Skip to main content

Section C.14 S3: Correctness

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.

Section 7.1