Logics preserve truth. If you start with premises that are true and transform them using logical rules, then your conclusions are also true. Algorithms do things. If you start with an input, following the steps of an algorithm will transform it to an output. There’s a fab way to apply logic to actions that was developed in Belfast by computer scientist Tony Hoare (1969), building on work by Robert Floyd (1967). I learned about this in Belfast, 2000; here’s an attempt to explain it.
A recipe is a kind of algorithm. Its inputs are ingredients and the steps involve peeling, chopping, heating, stirring. The output is a particular dish. But there’s no guarantee what the resulting dish will be if you start from the wrong ingredients, even if you follow the steps.
Hoare formalises this intuition for computer algorithms in what is now known as a Floyd-Hoare triple:
\(P \{Q\} R\)
\(P\) is the precondition (you have the right ingredients), \(Q\) is the sequence of steps of the algorithm (or recipe), and \(R\) is the postcondition (the resulting dish).
So \(P\) and \(R\) are statements that could be either true or false (logic as usual) and \(Q\) is sequence of actions (something different). The triple, \(P \{Q\} R\), as a whole is a statement that is true or false – that’s the key innovation. The triple lifts actions into the world of truths.
Here is how to read the triple (Hoare, 1969, p. 577):
“If the assertion \(P\) is true before initiation of a program \(Q\), then the assertion \(R\) will be true on its completion.”
We need axioms and rules of inference to reason about all the different kinds of program, for instance, doing one thing after another; choosing what to do, depending on whether some condition is true; and repeating things until a condition is met. These are the main ingredients of any program.
Assignment
Things quickly get complicated. Let’s start with a simple assignment statement. I’ll use an R-ish notation:
\(y \leftarrow x + 42\)
If you run this program, then \(y\) will be set to whatever \(x\) is plus 42.
The axiom for thinking about assignment statements (the axiom of assignment) is as follows:
\(P_0 \{ x \leftarrow f \} P\),
where \(P_0\) is the result of taking \(P\) and replacing all occurrences of \(x\) with \(f\). That’s how Hoare writes it. We could also write:
\(P[f/x] \{ x \leftarrow f \} P\),
where \(P[f/x]\) is another way to express the replacement in symbols. (I remember what it means because “/” is a forward slash, so it’s “\(f\) for \(x\)”.)
Now let’s suppose, for our one-liner program above, we want our postcondition to be that \(y\) is strictly positive. We have the following triple from the axiom of substitution:
\((y > 0)[x + 42 / y]\ \{ y \leftarrow x + 42\}\ y > 0\).
We can calculate \((y > 0)[x + 42 / y]\) by examining \(y > 0\) and replacing all occurrences of \(y\) (there’s one) with \(x + 42\). So we get:
\(x + 42 > 0\ \{ y \leftarrow x + 42\}\ y > 0\).
Equivalently,
\(x > -42\ \{ y \leftarrow x + 42\}\ y > 0\).
Let’s give this a go with an example. Suppose \(x = -41.9\). Then if we run \(y \leftarrow x + 42\), the result is \(-41.9 + 42 = 0.1\) and \(0.1 > 0\). It worked, the postcondition is true!
Suppose we try the program with \(x = -42\). Now the precondition doesn’t hold (the ingredients are wrong). If we run \(y \leftarrow x + 42\), the result is \(-42 + 42 = 0\) and so the postcondition doesn’t hold either.
If-else
That’s not a particularly impressive program. Let’s try something requiring an if-else: a program for finding the maximum of \(x\) and \(y\) and saving the answer in \(m\). Here’s a first go at the postcondition:
\(m \ge x \land m \ge y\).
In words, \(m\) should be greater than or equal to both \(x\) and \(y\). We would also probably like \(m\) to be one of \(x\) or \(y\), but let’s begin with this weaker postcondition.
Here’s a program:
if \((x \ge y)\) then
\(m \leftarrow x\)
else
\(m \leftarrow y\)
There is no apparent precondition (well, we could explicitly require that the inputs are valid values on which there is an ordering). The if-else gives us preconditions on the two routes through the code for free, as per the annotations below in square brackets:
if \((x \ge y)\) then
\([x \ge y]\)
\(m \leftarrow x\)
else
\([x < y]\)
\(m \leftarrow y\)
That is, in the arm of the if-else that only runs when \(x \ge y\), we can assume that \(x \ge y\). (We are assuming that the program which runs R programs is correct. Proving this is definitely somebody else’s problem.)
We can now reduce the program to two triples about assignment statements, one for each arm of the if-else:
\(x \ge y\ \{m \leftarrow x \}\ m \ge x \land m \ge y\)
\(x < y\ \{m \leftarrow y \}\ m \ge x \land m \ge y\)
Take the first. If we carry out the substitution on the postcondition as per the axiom of assignment, the resulting precondition is \(x \ge x \land x \ge y\). So we have now proved:
\(x \ge x \land x \ge y\ \{m \leftarrow x \}\ m \ge x \land m \ge y\)
But the triple we want to prove is:
\(x \ge y\ \{m \leftarrow x \}\ m \ge x \land m \ge y\)
We need some way to link the derived precondition, \(x \ge x \land x \ge y\), onto the one we have on this arm of the if-else, \(x \ge y\).
The way to do so is using Hoare’s rules of consequence. There are two such rules. The one we need is:
If \(P\{Q\}R\) and \(S \Rightarrow P\), then \(S\{Q\}R\).
We got \(P\) from the rule of assignment and \(S\) is the precondition we have from the if-else, so next we need to prove \(S \Rightarrow P\):
\(x \ge y\ \Rightarrow\ x \ge x \land x \ge y\).
It’s easy to see that this holds. It is indeed true that \(x \ge x\) and we get \(x \ge y\) for free from the antecedent. So by the rule of consequence, we have proved
\(x \ge y\ \{m \leftarrow x \}\ m \ge x \land m \ge y\)
Take the second arm of the if-else. If we carry out the substitution on the postcondition as per the axiom of assignment and apply the rule of consequence, we have to prove:
\(x < y\ \Rightarrow\ y \ge x \land y \ge y\).
Which is equivalent to
\(x < y\ \Rightarrow\ x \le y \land y \ge y\).
Again it is easy to see that this holds. If \(x < y\), then clearly \(x \le y\). And \(y \ge y\) holds too.
We have now proved that both routes through the program satisfy the postcondition, so we are done.
Now let’s try again and check that by the end of program \(m = x\) or \(m = y\). Here are the two triples we need to prove (\(\lor\) is the symbol for “or”):
\(x \ge y\ \{m \leftarrow x \}\ m = x \lor m = y\)
\(x < y\ \{m \leftarrow y \}\ m = x \lor m = y\)
Apply the axiom of assignment to them both:
\(x = x \lor x = y\ \{m \leftarrow x \}\ m = x \lor m = y\)
\(y = x \lor y = y\ \{m \leftarrow y \}\ m = x \lor m = y\)
So we need to prove the following two propositions, via the rule of consequence:
\(x \ge y \Rightarrow (x = x \lor x = y)\)
\(x < y \Rightarrow (y = x \lor y = y)\)
which are equal to
\(x \ge y \Rightarrow \mathbf{true}\)
\(x < y \Rightarrow \mathbf{true}\)
Both reduce to \(\mathbf{true}\). We’re done!
Loops
Now the fun begins. Hoare (1969, p. 578) provides the following rule of iteration, mildly translated into R as follows:
If \(P \land B\ \{S\}\ P\), then \(P\) {while (\(B\)) \(S\) } \(\neg B \land P\).
Note how \(P\) appears in both the precondition and postcondition of the loop. In later papers, this became known as the loop invariant.
Something else to note: there are two ways for \(B\) to be false. One is that, given some inputs and code before the loop, we already have the answer so there’s no need to run the loop. The other is that the loop has run at least once and now finished looping.
I want to find a program to illustrate how this works using the smallest number of assignment statements in the loop. The smallest I can think of, with one statement, counts down from (nonnegative) \(n\) to \(0\) and doesn’t do anything else:
\(i \leftarrow n\)
while (\(i > 0\))
\(i \leftarrow i\ – 1\)
The problem with this is that there’s no interesting loop invariant.
So we will need more than one statement in the while loop. This means we need Hoare’s rule of composition (again mildly translated to R):
If \(P\{Q_1\}R_1\) and \(R_1 \{Q_2\} R\), then
\(P\)
\(\{Q_1\)
\(Q_2\}\)
\(R\)
(Hoare used an explicit composition operator, \(;\). R allows a newline to compose statements. It does have the \(;\) too – often used when you want to squeeze multiple statements onto one line.)
The simplest program I can think of that actually does something requires two statements in the while loop: it multiplies a number, \(x\), by a natural number, \(n\), using repeated addition. Let’s save the result in \(r\). So the postcondition of the program is \(r = xn\).
I’m going to use the rule of iteration to help write the program. The easiest case is when \(n = 0\): \(x0 = 0\). Let’s suppose the loop doesn’t run when \(n = 0\) The program for this case is then simply:
\(r \leftarrow 0\)
Let’s use \(i\) as the loop variable. We need to find a suitable loop invariant – something that is true on each iteration of the loop. Let’s try \(r = xi\). So, a mild addition to the program above leads to:
\(r \leftarrow 0\)
\(i \leftarrow 0\)
This suggests that \(i\) needs to iterate from \(0\) up to \(n\) (without having to look after the loop invariant, I probably would have looped down from \(n\)). Here’s a first try for the whole program:
\(r \leftarrow 0\)
\(i \leftarrow 0\)
while (\(i \ne n\)) {
\(r \leftarrow r + x\)
\(i \leftarrow i + 1\)
}
Back to the rule of iteration, we need to prove:
\(r = xi \land i \ne n\ \{r \leftarrow r + x; i \leftarrow i + 1\}\ r = xi\)
Let’s begin with the last assignment statement. Using the axiom of assignment we get:
\(r = x(i+1)\ \{ i \leftarrow i + 1 \}\ r = xi\)
Your first thought on looking at that precondition might be, er, what?
But glance at the line above, \(r \leftarrow r + x\). If this has worked, then \(r\) has incremented by \(x\) and we just need to increment \(i\) too so that the invariant still holds. I’m going to take this precondition and feed it through the previous line to calculate a postcondition using the axiom of assignment:
\(r + x = x(i+1)\ \{ r \leftarrow r + x \}\ r = x(i+1)\)
Before we think about what’s going on in the precondition on the left, we can glue both statements together by the rule of composition. Call the two liner in the while loop, \(T\). Now we have:
\(r + x = x(i+1)\ \{ T \}\ r = xi\)
We want to prove:
\(r = xi \land i \ne n \ \{T\}\ r = xi\)
This looks like another case for the rule of consequence we used above. Let’s fill in the variables with the information we have:
If both of these conditions hold:
(1) \(r + x = x(i+1)\ \{ T \}\ r = xi\)
(2) \(r = xi \land i \ne n\ \Rightarrow\ r + x = x(i+1)\),
then \(r = xi \land i \ne n \ \{T\}\ r = xi\).
We just need to prove the second conditional. We get \(r = xi\) from the antecedent. Adding \(x\) to both sides gives us
\(r + x = xi + x\)
\(\equiv\)
\(r + x = x(i + 1)\)
We’re done!
Strictly speaking, we need to drag the axiom of assignment and rule of composition up the program to check that running
\(r \leftarrow 0\)
\(i \leftarrow 0\)
establishes the invariant before the loop. Without using the formal axioms, I think it’s easy to see that they do and we did think about this when writing the program.
Additionally, we really need to show that the program establishes \(r = xn\). By the end of the loop, we know that \(i = n\) (otherwise the loop hasn’t terminated – also it’s part of the rule of iteration) and \(r = xi\) (by the loop invariant). So \(r = xn\) does indeed hold.
References
Floyd, R. W. (1967). Assigning meanings to programs. In J. T. Schwartz (Ed.), Proceedings of Symposium on Applied Mathematics (pp. 19–32).
Hoare, C. A. R. (1969). An axiomatic basis for computer programming. Communications of the ACM, 12(10), 576–583.
