CSci 420/520: Proof of Maximum Algorithm

Here is the proof of the maximum algorithm in all its gory detail. I'm going to do it in reverse as you might work it out, then rewrite it so that it is more clear.

Prove:

{true}

if ( a >= b )
  m = a;
else
  m = b;

{m = max(a,b)}

"Work It Out" Proof

Working backwards in the proof, and outside-in in the code, we first want to derive the subgoals that will allow us to apply the "if" composition rule. These are:

{a >= b ∧ true}

m = a;

{m = max(a,b)}

{¬(a >= b) ∧ true}

m = b;

{m = max(a,b)}

The above two Hoare triples are the antecedents we need to apply the "if" composition rule. But we don't know if they are true, so we need to keep working backward. Let's work on the first one first. There's an assignment, which suggests that the assignment axiom would be useful. Unfortunately, the precondition doesn't actually say what the assignment axiom requires:

{a = max(a,b)}

m = a;

{m = max(a,b)}

We know the above to be true because of the axiom of assignment. (Recall that axioms are self-evident truths in our logic.) Now the question is whether we can get from this to the previous Hoare triple for m = a;. Since we're inferring the precondition, we need to employ the rule of consequence.

But to do this, we need to also prove the P ⇒ P' and Q' ⇒ Q verification conditions. In this case, P is "(a >= b) ∧ true" from our target triple, P' is "a = max(a,b)" from the axiom triple, Q' is "m = max(a,b)" from the axiom triple, and Q is "m = max(a,b)" from the target triple. So, we need to show that:

(a >= b) ∧ true ⇒ a = max(a,b)

and

m = max(a,b) ⇒ m = max(a,b)

The second implication is trivially true. For the first one, if a >= b then we know that max(a,b) will be a.

So, given these two implications and the axiom of assignment triple, we can deduce the first of our two previous assignment triples using the rule of consequence. We can do a similar proof for the second of the two previous assignment triples. i.e. Use the assignment axiom to get:

{b = max(a,b)}

m = b;

{m = max(a,b)}

Then try to prove the implications that we need for the rule of consequence:

¬(a >= b) ∧ true ⇒ b = max(a,b)

and

m = max(a,b) ⇒ m = max(a,b)

As before, this is easy given the definition of max(a,b)--if a is not less than or equal to b, then max(a,b) is b.

And as before, we can use these two implications and the axiom of assignment triple to derive the second target assignment triple using the rule of consequence.

This completes the "work it out" backward proof, since we started with the if-then, derived the two assignments in the antecedent, then proved the two antecedents back to the axioms. Now I'll rewrite this proof starting from the axioms in a more direct way.

Magical Forward Proof

Below is a step-by-step table for the proof. It seems magical when presented this way because we seem to pull the right "R" conditions from thin air.

m = a;

m = a;

m = b;

m = b;

if (a >= b)
  m = a;
else
  m = b;