Guarded Commands, Nondeterminacy and Formal Derivation of Programs
This is the paper that introduced predicate transformer semantics.
Dijkstra begins by defining an imperative language of “guarded commands”, which has the following syntax (slightly modified):
The intended semantics is nondeterministic: a conditional should nondeterministically execute some branch whose guard expression evaluates to truth (failing in case there is no such guard), and a loop should repeatedly do the same as long as at least one guard expression evaluates to truth (proceeding as a no-op in case there is never any such guard).
Building off of Hoare's work, Dijkstra defines the semantics of this language in terms of “predicate transformers”: a program is interpreted as a function that maps a postcondition to the weakest precondition such that . This weakest precondition is often written as .
The way in which we use predicates (as a tool for defining sets of initial or final states) for the definition of the semantics of programming language constructs has been directly inspired by Hoare, the main difference being that we have tightened things up a bit: while Hoare introduces sufficient pre-conditions such that the mechanisms will not produce the wrong result (but may fail to terminate), we shall introduce necessary and sufficient—/i.e./ so-called “weakest”—pre-conditions such that the mechanisms are guaranteed to produce the right result.
To see the difference, let us consider a few constructs.
1. conditionals
First, recall Hoare's rule for conditionals:
Define . Let's work out . Both and have their own weakest preconditions, so should be some composition of these. We reason: if executed and left true, then either was true and was true, or was false and was true. Thus: Note that this is logically equivalent to
Now, a conditional in Dijkstra's language looks like Our reasoning for is very similar to our reasoning for . Instead of a single conjunction, we use an existential: To obtain something more like to the second form, it is tempting to use But this is not quite right, since it does not guarantee that some is true. (We did not need to worry about this for , since it was effectively equivalent to a with guard conditions and , of which at least one is always true.) So we need to add a side-condition: This is the formulation that Dijkstra uses.
2. loops
Hoare's rule looks like this:
Let ; let's derive . Note that must always hold after executing , so we are really looking for . We can analyze the situation into cases depending on how many times ran.
- Suppose never ran. Then running changed nothing, so the weakest precondition is exactly the postcondition. In this case, the weakest precondition is .
- Suppose ran just once. Then, before executing , both and must have been true. In this case, the weakest precondition is . Note that is the weakest precondition in the case of zero iterations.
- Suppose ran twice. Before the second iteration, both and must have been true. Then, before the first iteration, both and must have been true. In this case, the weakest precondition is . Note that is the weakest precondition in the case of one iteration.
Generalizing, we define
- , and
- ;
Then
Now, a loop in Dijkstra's language looks like Following similar reasoning, we define
- , and
- ;
then Again, Dijkstra's formulation is slightly different: he defines
- , and
- .
I believe that this formulation is logically equivalent to the former one, but I have not bothered to prove it.