Semantics of Imperative Features
Thérèse Hardin, Mathieu Jaume, François Pessaux, Véronique Viguié Donzeau-Gouge · 2021
This chapter presents the several classical semantic approaches to the most common imperative features of programming languages. It presents applications of the semantic definitions, along with a few classical proof techniques using these formalisms. As an operational semantics describes program behavior, it is possible to identify “equivalent” programs, that is, programs whose executions terminate and lead to the same memory state. Procedures are used to structure the code of a program, isolating certain parts and making them accessible from any point in the program. The chapter introduces the notion of a block, which confines definitions of variables and procedures in a portion of code. The call by reference mechanism transmits to the procedure a value, which is the reference of a mutable variable present in the current environment of the call. The axiomatic semantics is generally used to prove properties concerning the expected results of programs, rather than to describe their execution.