After this course participants are able to:
- Define the semantics of imperative language constructs using inductive methods.
- Explain the consequences of design choices.
- Analyze computations in imperative languages like termination behavior and semantic equivalence.
- Prove properties of programs using inference systems for correctness.
- Determine whether inference systems are sound and/or complete.
|
|
|
In this course, you will learn formalisms to define the operational semantics of imperative programming languages. These methods are important for designing new languages and extending existing languages. In addition, these formalisms are used for analyzing the behavior of programs. In the field of computing science, you will not only have to apply these formalisms, but you will also have to evaluate, expand or design these formalisms as well.
|
|
|
| You have programming experience with imperative programming languages. In addition, you are able to:
- use the language of predicate logic to formulate statements; distinguish the elementary steps within argumentation and present proofs in a suitable inference system;
- specify (programming) languages and extensions using regular expressions and context-free grammars;
- formulate clearly, both in motivating solutions as well as in proofs in natural language.
You can obtain these prerequisites by doing the courses in the programming line, the course Languages and Automata, and the course Logic and Applications. In addition, it helps if you have done the course Computability, but that is not a formal requirement. |
|
| The course is finalized with a written exam. |
|
|