Skip to main content
Logo image

Section C.14 S3: Correctness


  • 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.