Semantics Of Programming Languages. Ediz. Italiana

We first define the formal semantics of some imperative programming languages. In particular, we define the operational semantics of a simple imperative language with assignments, concatenation, conditional and iterative commands, and we present the axiomatic semantics of that language by using the calculus of Hoare triples for proving partial correctness of programs. We also consider imperative languages which have nondeterministic and parallel commands. Then we present the operational and the denotational semantics of some first–order and higher–order functional languages, under both the eager semantics (call by value) and the lazy semantics (call by name). For that purpose, we introduce the theory of the complete partial orders and the fixpoint theory of continuous functions. We also study the abstraction property of the denotational semantics of those functional languages. We then present various induction principles for proving properties of recursive, functional programs. We introduce the Calculus for Communicating Systems (CCS) by Robin Milner, and the modal mu–calculus, and we present a local model checker for verifying properties of parallel processes. Finally, we present the Prolog implementations of: (i) the operational semantics of a simple imperative language and some functional languages, and (ii) a local model checker for the modal mu–calculus.