Synopsis

• Introduce specifications semantically as pair of state sets.
• Show examples of programs that fulfill simple specifications.
• Introduce assertions as propositional formula that represents sets of states and can be used to formulate specifications by pre- and post-conditions.
• Define specifications syntactically pre- and post-conditions and solve the technical problem of compatible variables.
• Introduce total and partial correctness and the syntax of Hoare triples.
• Discuss weakening of post-conditions and strengthening of pre-conditions.
• Introduce failures, discuss difficulties in detecting failures in C due to undefined behavior.
• Introduce assertions practically as a means to check if an assertion holds during program execution.
• Briefly discuss “defensive programming”, i.e. making programs fail as early as possible by documenting pre- and post-conditions using assertions.

Sections Covered