PLP: Lecture 33
Assertions con’t
Think of A
as the set of states where assertion A
is true
- $ A \supset B$ means
A
is a subset ofB
A and B
is the intersection of A and BA 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.
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.