Synopsis

• Recap of correctness definition Section 7.1
• Correctness up to now was defined on the semantics, on executions of the program.
• We now develop a logic to reason about correctness without reasoning about executions.
• Note that the rules of the logic have to be proven correct but that is out of scope.
• Introduce basic rules of abort and assignment and informally reason about correctness.
• Block and sequence rules show how free assertions are determined by other rules (assignment).
• If-then-else example shows that sometimes assertions don’t “add up”.
• Introduce rule of consequence to strengthen preconditions and weaken postconditions.
• Note that non-matching assertions can be dealt with by the consequence rule which spins off verification conditions

Sections Covered