Assertions con’t

Think of A as the set of states where assertion A is true

  • $ A \supset B$ means A is a subset of B
  • A and B is the intersection of A and B
  • A or B is the union of A and B

While loop

After the loop, we know that not B must be the case. We have:

while B do S = 
if B then {S; while B do S} else skip

Doesn’t tell us that the loop terminates!

This becomes

{P}
if B then {S; while B do S} else skip
{~B and Q}

Using rule for if-statement, this is

{P and B} S; while B do S {~B and Q}, P and ~B $\supset$ ~B and Q
---
{P} while B do S {~B and Q}

Loop invariants $\rightarrow$ true before and after executing loops. Solution to a fixed point equation.

For assignment and if-statements, given a postcondition, we can always calculate the weakest precondition by starting with the postcondition and applying axioms. Can’t do this with loop invariants.

Termination

Partial correctness: nontermination allowed. Total correctness: termination required. Old-fashioned perspective.

Well founded set: A set with a partial order is well founded if there are no infinitely decreasing sequences of distinct elements from the set. E.g., the Natural numbers (no negatives).

To prove a loop terminates (i.e., proving total correctness), define a variant function which takes values from a well founded set. Show that each loop iteration decreases the value of the variant function or establishes $\neg B$. Since the variant function can’t decrease forever, the loop must terminate.

Let I be a loop invariant.

While loop with loop

While loop with loop

Often times, will need to come up with a loop invariant when trying to prove termination. How to do this? Guess! Take the guard of the loop, (e.g., while guard do S), delete the conjuct in the post-condition that represents the negation of the guard. What’s left is the loop invariant.