So far, we have employed a substitutive model of computation for Racket programs to reason about their correctness. This model made a significant assumption about their behavior: our programs are pure. In other words, our programs do not produce any side-effects.

Examples of side-effects include:

• Mutating (i.e., changing) the contents of a variable.
• Printing a string to the console, e.g, print('hello world!').
• Receiving input from the user, e.g., keyboard input via the input function.
• Raising an exception or throwing an error.

You can tell from this list that side-effects are integral to most programs that we write. So it stands to reason that our model of computation should account for them. However, mere substitution is insufficient to properly capture the behavior of an impure program!

To see this, consider the following code snippet involving variable mutation:

x = 1
y = x + 1
x = 5
z = x + 5

How might we evaluate this sequence of four statements, program fragments whose purpose are to produce side-effects? The first line is a simple initialization of the variable x to 1. One thought might be to evaluate this initialization statement by replacing any subsequent occurrence of x with 1. This results in the following updated program:

y = 1 + 1
x = 5
z = 1 + 5

On the next line, we initialize y to 2 which makes sense since x is initialized to 1. However, on the line after this, we reassign x to store a new value, 5. This clearly will cause issues because on the final line, we had already substituted away the occurrence of x with its old value, 1!

Introduction to Hoare Logic

To fix this, we might observe that we should have simply substituted only for the first occurrence of x since the second occurrence of x is shadowed by the reassignment of x to 5. However, in general, we may not know which assignment is active for a given use of a variable! Consider the following example:

x = 0
if ... :
    x = 5
print(x)

Here, let’s assume for the sake of argument that x can either be 0 from line one or 5 from line three. With our substitutive model, after executing line one, we must decide whether the occurrence of x in the print(x) call will come from this initialization. However, we won’t know this fact until we evaluate the guard of the conditional which could consist of arbitrary code, e.g., checking to see if the user presses a certain key.

From this example, we can see that substitution simply won’t cut it; we need a new model that accounts for impure code! This model, Hoare Logic, named after British computer scientist, Sir Tony Hoare allows us to reason about an impure program in terms of pre- and postconditions of the various parts of the program.

Previously, you studied pre- and postconditions as they related to functions. We specified preconditions on the parameters of our function and postconditions on the function’s output. Now we’ll extend this idea to whole programs, i.e., collections of statements.

Let’s look at this with an example. Consider the following program:

# x is previous defined
y = x + 5   # Line (a)
x = x * 2   # Line (b)
y = y - x   # Line (c)

Suppose that we assume as a precondition to the program that 0 ≤ x ≤ 5, i.e., x is a natural number and that we want to show that as a postcondition to this program that y ≥ 0. How can we reason about the behavior of our impure program to prove that our postcondition holds under the assumption that our precondition holds?

Hoare logic gives us a framework for proving claims of this sort in a compositional manner. In other words, we reason about our program in terms of its individual parts. To do so, let’s work backwards from the postcondition through the program and see if our precondition is sufficient to guarantee that the postcondition holds. Working backwards from our goal back to our original assumptions is akin to our substitutive proofs in that we had our goal and transformed it via symbolic evaluation into an obviously provable fact. Here, we’ll work backwards but with a different aim: to arrive at a set of preconditions that are definitely true according to the assumptions we make initially.

After line (c), it must be the postcondition holds, i.e., that y ≥ 0. What must be true before the assignment on line (c) for this to hold? The assignment has the effect of making y the right-hand side of the assignment y - x. If we were expecting y ≥ 0 to hold, then we must also expect that this inequality holds of the right-hand side before we perform the assignment, i.e., y - x ≥ 0.

We’ll write this information in a particular way:

# ...

# {{ y - x ≥ 0 }}
y = y - x   # Line (c)
# {{ y ≥ 0 }}

Below each line, we write the postcondition that ought to hold after execution of that line. Above each line, we write the precondition that ought to hold before execution of that line. We call this combination of a precondition, program statement, and postcondition:

# {{ <precondition> }}
<statement>
# {{ <postcondition> }}

A Hoare triple in Hoare logic. In our proofs of this style, we will annotate our code using these triples, interspersing the annotations between lines under the assumption that the postcondition of the previous line becomes the subsequent precondition of the next line. This makes sense because of the sequential manner in which we execute statements.

Continuing the proof, for line (b), we mutate to contain the value x * 2, i.e., the old value of x multiplied by 2. Similar to the logic of the previous line (c), this means that whenever our postcondition (i.e., precondition of line (c)) mentions x, the assignment implies that we really meant x * 2. This gives us the following updated precondition for line (b)

# ...

# {{ y - (x * 2) ≥ 0 }}
x = x * 2   # Line (b)
# {{ y - x ≥ 0 }}
y = y - x   # Line (c)
# {{ y ≥ 0 }}

When we process line (a), we apply the same logic to the initialization of y: whenever we see y in our postcondition, we really mean the value it is assigned to, x + 5, in its precondition:

# {{ x + 5 - (x * 2) ≥ 0 }}
y = x + 5   # Line (a)
# {{ y - x * 2 ≥ 0 }}
x = x * 2   # Line (b)
# {{ y - x ≥ 0 }}
y = y - x   # Line (c)
# {{ y ≥ 0 }}

We have completed pushing our postcondition back through the program to arrive at an initial precondition to the function. The precondition that we derived, x + 5 - (x * 2) ≥ 0, does not look like our initial assumption, 0 ≤ x ≤ 5. However, we don’t need for the preconditions to line up exactly! It is sufficient if our assumed precondition implies that our derived precondition is true. In other words, if 0 ≤ x ≤ 5 then does x + 5 - (x * 2) ≥ 0? A little bit of arithmetic demonstrates this fact! Below, we include a complete description of our first proof using Hoare logic:

# {{ x + 5 - (x * 2) ≥ 0 }}
y = x + 5   # Line (a)
# {{ y - x * 2 ≥ 0 }}
x = x * 2   # Line (b)
# {{ y - x ≥ 0 }}
y = y - x   # Line (c)
# {{ y ≥ 0 }}

The Rules of Hoare Logic

Like symbolic evaluation, Hoare logic provides a collection of rules for reasoning about the different constructs of our programs, here, statements. Our previous example consisted exclusively of variable initialization/assignment statements, so let’s try to generalize this rule. Let’s reexamine our reasoning for the final line of the program:

# {{ y - x ≥ 0 }}
y = y - x   # Line (c)
# {{ y ≥ 0 }}

We know that the effect of an assignment statement is to store the value that right-hand side expression evaluates to in the variable on the left-hand side of the equals sign. Thus, at this point in our program, the left-hand side variable is equivalent to the right-hand expression. With this in mind, it is safe to capture this information in our updated precondition by substituting the right-hand expression for the left-hand variable everywhere in occurs in the postcondition. In our above example, to obtain the precondition, we replace y with y - x everywhere y occurs in the postcondition y ≥ 0. Likewise, on line (b):

# {{ y - x * 2 ≥ 0 }}
x = x * 2   # Line (b)
# {{ y - x ≥ 0 }}

We replace x with x * 2 everywhere x occurs inside of the postcondition y - x ≥ 0. This notion of substituting into the postcondition to arrive at the necessary precondition gives us the following rule for reasoning about assignment:

# {{ [e ↦ x] P }}
x = e
# {{ P }}

The notation \([e \mapsto x] P\) means that the precondition is \(P\) but with every occurrence of \(x\) replaced with \(e\). We can pronounce this substitution notation pithily as:

\(e\) for \(x\) everywhere inside of \(P\).

Implicitly, we used another key rule of Hoare logic: sequencing. If we have consecutive statements \(s_1\) and \(s_2\), the precondition of \(s_2\) becomes the postcondition of \(s_1\).

# {{ P }}
s1
# {{ Q }}
s2
# {{ R }}

Finally, in our example, we observe that our derived precondition x + 5 - (x * 2) ≥ 0 was not identical to our assumed precondition 0 ≤ x ≤ 5. However, we showed that the assumed precondition implied our derived precondition. Another way to look at this is that we strengthened the derived precondition so that it was identical to the assumed precondition. This is safe because the stronger statement 0 ≤ x ≤ 5 which puts more constraints on x certainly implies the truth of the weaker statement x ≤ 5 since it places fewer constraints on x (i.e. our derived precondition is good enough to proof the program correctness).

In general, when computing precondition and postcondition for program correctness proof, we can always weaken our precondition as needed to meet our original assumptions (a stricter one):

# {{ P' }}
s
# {{ Q }}

# {{ P }}
s
# {{ Q }}

In our example, \(P'\) is x ≤ 5 and \(P\) is 0 ≤ x ≤ 5. This “implies” relationship between the two propositions \(P\) and \(P'\) is called logical implication. A logical implication \(P \rightarrow P'\) is true if whenever \(P\) is true that \(P'\) is true as well.

We can also apply similar, but reversed logic, to the postconditions of a Hoare triple. Whereas it is always safe to weaken preconditions because they represent assumptions about the state of our program (more “input”), it is always safe to strengthen postconditions because they represent guarantees about the outputs of our program. To put it another way, we can always strengthen our expectations about a program and still be safe!

# {{ P }}
s
# {{ Q' }}

# {{ P }}
s
# {{ Q }}

Exercises

# w is already defined
x = w - 1
y = w + 1
z = x * y