1. Operational Semantics: big-step semantics, small-step semantics and abstract machine semantics for the simple imperative language IMP.
2. Analysing IMP programs: state space exploration, termination, equivalence. Determinism of IMP.
3. Denotational Semantics for IMP. Fixed Point Theory. Relation with big-step operational semantics.
4. Axiomatic Semantics for IMP. Program Verification. Computing weakest preconditions.
5. Operational and denotational semantics for the simple declarative language REC. Domain Theory.
The overall aim of the course is to study the main semantic styles used for capturing the meaning of programs in a formal way, compare their strengths and weaknesses, and analyze how they can be used for establishing important properties of programming languages, concrete programs, and transformations on programs. A secondary goal is to learn the theories and proof techniques on which such semantic investigations are based.
After the course, the successful student will be able to perform the following constructions:
- construct the state space of a program as a basis for program behaviour analysis through state space exploration;
- compute the denotation of a program;
- extend a programming language with new constructs, and extend its semantics accordingly;
- specify and verify programs in Hoare logic,
- formally relate different semantic styles;
- prove language properties such as determinism and termination;
- show correctness of a given program transformation by proving equivalence of the original and the transformed program.
For passing the course, a student has to demonstrate proficiency with problems of type 1-4; for the highest grade he/she has to be equally proficient at the remaining types of problems.
