Preamble This post, although involving unusual notions for most, is meant to be very basic and I expect most computer scientists, computer science students to be able to understand it. If you don't please let me know, I'll arrange to put enough background in it.
End of preamble
For some time, Prof. Jonathan Ostroff has been trying to convince me of the elegance of Hehner's method of refinement. Recently, I was giving examples of Dijkstra's program calculus. Among these was the derivation of the program for computing the maximum of two numbers and its proof. I eventually came around to consider this example terms of Hehner's method and I was struck with at how simple his formulation is. For example, the semantics of the following conditional statement is given in Hehner's formulation and in Dijkstra's (and Morgan's, for that matter).
if b -> x := E [] c -> x := F fi
Hehner (x' denotes the value of the variable x after execution whereas x denotes its initial value):
(b /\ x' = E) \/ (c /\ x' = F)
Dijkstra (it is defined as a function of the predicate p and it represents the weakest precondition that will allow the statement to enforce the postcondition p):
(b ==> (x := E).p) /\ (c ==> (x := F).p) /\ (b \/ c)
Just here, we have a factor of a little bit less than two. It is a bit of an unfair comparison, though since the two formulae are not used in the same way. It is interesting to note, however, that Dijkstra's formulation includes a term (b \/ c) which he calls "the law of excluded miracle" (as a pun referring to "the law of excluded middle"). Its purpose is to make sure that one of the branches of the conditional applies whenever we get ready to execute the statement. On the other hand, Hehner's formulation implies (b \/ c) and it does not have to be included in the term. Unfortunately, it is necessary with Hehner's method to mention every variable that do not change which, as it appears to me, an amateur when it comes to Hehner's method, can be quite inconvenient.
Here is the development of the mentioned program with both methods. We start by stating the postulates that we have.
(0) x max y >= x
(1) x max y >= x
(2) x max y = x \/ x max y = y
(3) x max y = y max x
(4) x = x max y == x >= y
(5) y = x max y == y >= x
(6) x >= y \/ y >= x
Now, here is the postcondition that we want to implement:
P: z = x max y
because of the form of (2) we could presume that the appropriate execution of either of:
Q: z := x
and
R: z := y
We must therefore investigate when it is appropriate to execute each. For that, we calculate the weakest precondition that allows each of them to establish the postcondition. We can do that by applying the statements Q and R as a subtitution over the postcondition P.
Q.P
== { Subtitution }
x = x max y
== { (4) }
x >= y
(with == being the logical equivalence) Using a similar calculation, we get
R.P == y >= x
We can conclude that the following code establishes the postcondition:
if x >= y -> z := x
[] y >= x -> z := y
fi
The only thing left to do is to apply the law of excluded miracle and make sure that there is always a branch which is executable.
(x >= y) \/ (y >= x)
== { (6) }
true
If we try the same derivation with Hehner's method, we can start by saying that the postcondition is trivially established by
P: z := x max y
which, unfortunately, is not executable. For simplicity, we will assume that x is the only assignable variable. We have the following statement representing the semantics of P.
Q: z' = x max y
We can now start calculating:
z' = x max y
== { Identity of /\ }
z' = x max y /\ true
== { (2) }
z' = x max y /\ (x = x max y \/ y = x max y)
== { /\ distributes over \/ }
(z' = x max y /\ x = x max y) \/ (z' = x max y /\ y = x max y)
== { Leibniz, twice }
(z' = x /\ x = x max y) \/ (z' = y /\ y = x max y)
== { (4) and (5) }
(z' = x /\ x >= y) \/ (z' = y /\ y >= x)
The final stage of the calculation represents the semantics of the following conditional:
if x >= y -> z := x
[] y >= x -> z := y
fi
What I like about the previous derivation is that it is very straight forward. There is a small invention involved which is to introduce true at the beginning and transform it into (2). It seems reasonable since it gives a simple expression for any possible value of x max y. Also, the proof contains a little too much detail. For instance, the first and the second steps could have been merged and explained simply by referring to assumption (2).
On a more personal side, I must admit that, for at least one year, I was very enthusiastic about Ralph Back's lattice theoretic interpretation of programs: it's just so elegant! In practice however, I can't help but being struck with awe at how straightforward the program derivation is with Hehner. Like Dijkstra said so often: we must not become enamored with our tools especially if they show how clever we have been. Back's interpretation introduced me to lattice theory which I still like and find pretty useful but using it for program calculus does not seem necessary and I should probably turn over to Hehner's program calculus even though it does not yell "I know lattice theory!"
Simon
September 18th 2009
Zürich
