CSC 208-01 (Spring 2023)

Reading: Hoare Logic

So far, we have employed a substitutive model of computation for Python 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.

Definition (side-effect) : a side-effect of an expression is any observable effect of evaluating that expression beyond producing a value.

Definition (purity): an expression is considered pure if it does not produce any side-effects.

Examples of side-effects include:

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 Python, 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.

Definition (precondition): a precondition of a program fragment is a property that must be true for that program fragment to behave as expected.

Definition (postcondition): a postcondition of a program fragment is a property that is guaranteed to be true if that fragment’s precondition is true.

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:

Claim: for the example program, if 0 ≤ x ≤ 5, then y ≥ 0.

Proof. We use following Hoare logic derivation to derive a precondition suitable to achieve the desired postcondition, y ≥ 0:

# {{ 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 can simplify our derived precondition as follows:

\[\begin{align*} &\; x + 5 - (x × 2) \geq 0 \\ \rightarrow &\; 5 - x \geq 0 \\ \rightarrow &\; 5 \geq x \end{align*}\]

\(5 \geq x\) (i.e., \(x \leq 5\)) if \(0 \leq x \leq 5\). Thus, our postcondition holds given our precondition.

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:

Rule (Assignment): Let x = e be an assignment statement of expression e to variable x. If the statement has postcondition \(P\), then it has precondition \([e \mapsto x] P\), i.e.

# {{ [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 \(e_2\) becomes the precondition of \(s_1\).

Rule (Sequence): Let \(s_1\) and \(s_2\) be statements. If \(P\) and \(Q\) are the pre- and postconditions of \(s_1\) and \(Q\) and \(R\) are the pre- and postconditions of \(s_2\), then we derive:

# {{ 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.

In general, when working backwards from precondition to postcondition we can always strengthen our precondition as needed to meet our original assumptions:

Rule (Consequence, precondition): If:

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

For some statement \(s\) and its precondition \(P'\) and postcondition \(Q\), and we can show that \(P\) implies \(P'\), written \(P \rightarrow P'\), for some other logical proposition \(P'\), then we can conclude:

# {{ 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 strengthen preconditions because they represent assumptions about the state of our program, it is always safe to weaken postconditions because they represent guarantees about the outputs of our program. To put it another way, we can always weaken our expectations about a program and still be safe!

Rule (Consequence, precondition): If:

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

For some statement \(s\) and its precondition \(P\) and postcondition \(Q\), and we can show that \(Q\) implies \(Q'\), written \(Q \rightarrow Q'\), for some other logical proposition \(Q'\), then we can conclude:

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

Loops and Conditionals

So far, we have covered straight-line code. Because there is only one path through the program, reasoning is relatively easy. However, once we introduce branching via conditionals and loops, our reasoning becomes more difficult.

First let’s consider a conditional with some guard e and if- and else-branches s1 and s2:

if e:
    s1
else:
    s2

Suppose that we want to show some postcondition Q holds off this conditional. What preconditions must be true at the start of the conditional to guarantee that Q holds?

We can derive a reasoning principle directly from our understanding of how the conditional executes. Regardless of how e evaluates (modulo non-termination), control flows into either s1 or s2 and then out of the conditional. Thus, whether postcondition Q holds depends on whether Q holds for both s1 and s2 which we can check independently of each other. We also know that when executing s1, it must be the case that e evaluates to True so that control flows into the if-branch. Likewise, when executing s2, it must be the case that e evaluates to False so that control flows into the else-branch.

Combining these facts gives us the following rule for reasoning about conditionals:

Rule (Conditional): If:

# {{ P ∧ e -->* True }}
s1
# {{ Q }}

And:

# {{ P ∧ e -->* False }}
s2
# {{ Q }}

Then:

# {{ P }}
if e:
    s1
else:
    s2
# {{ Q }}

In other words, to show that Q holds of a conditional, it is sufficient to show that Q holds under preconditions P in both s1 and s2 with the additional assumption that e = True when checking s1 and e = False when checking s2. Note that because

Let’s try this rule on an example. Consider the following Python code:

# x, y, and z have been previously defined

if x > y:
    z = x
else:
    z = y

We can then prove the following claim about this code using our conditional rule:

Claim: after execution of the code snippet, \(z \geq y\) and \(z \geq x\).

To prove this, it is sufficient to show that the proposition is a postcondition of this code without any required preconditions. Our conditional rule tells us that we must reason about each of the branches of the conditional independently.

First, let’s reason about execution of the if-branch. Using our assignment rule in conjunction with the additional assumption given yields the following annotated program:

# {{ x ≥ y ∧ x ≥ x ∧ x > y }}
z = x
# {{ z ≥ y ∧ z ≥ x }}

The final inequality x > y comes from the fact that we are in the if-branch of the conditional so that the guard must be true. \(x \geq x\) is always true and if we know that \(x > y\), then we also know that \(x \geq y\), so we can rewrite the preconditions to just \(x > y\) which is just the additional assumption gained by virtue of the if-branch. Thus, there are no preconditions in this case we need to assume if execution flows into the if-branch.

Now let’s reason about the else-branch. Again, using the assignment rule yields the following annotated program:

# {{ y ≥ y ∧ y ≥ x ∧ x ≤ y }}
z = y
# {{ z ≥ y ∧ z ≥ x }}

Again, the last condition of the precondition is due the fact that we’re in the else-branch of the conditional. If \(x > y\) does not hold, then \(x \leq y\) does hold. Simplification of calculated required preconditions yields that the required precondition is simply \(x \leq y\) which is the precondition we assume going into the branch. Thus we require no additional preconditions in this case, too, and our original claim holds.

Now, let’s reasoning about loops. A while-loop of the following form:

while e:
    s

Proceeds by first evaluating e. If e evaluates to True, then statement s is executed, i.e., we “go into the loop.” We then go back to the top of the while-loop, reevaluate e to see if it is still True, and if so, we reevaluate s. This process continues until e evaluates to False in which case execution proceeds to the statement immediately after the while loop.

Suppose that we wish to prove a postcondition Q holds of this loop. What must we do? Like a conditional, we get some additional assumptions as a consequence of how while-loops execute:

However, because of the nature of the loop, it is not clear what preconditions that might be required since every iteration may mutate variables in a way that drastically changes the behavior of later iterations.

Our insight here is that we will be conservative in our reasoning about a loop. In particular, we will require that the post-condition holds before execution of the loop, i.e., the precondition is precisely the postcondition. This makes the postcondition/precondition an invariant of the loop.

Definition (Invariant): an invariant of a piece of code, e.g., is a property that holds before and after execution of the code.

With this in mind, we can derive the following rule for reasoning about loops:

Rule (While): If:

# {{ P ∧ e = True }}
s
# {{ P }}

For some proposition P, expression e, and statement s, then:

# {{ P }}
while e:
    s
# {{ P ∧ e = False }}

Let’s apply this rule to reason about the following code:

# n is predefined

result = 0
i = 0
while i <= n:
    result = result + i
    i = i + 1

And the following postcondition:

Claim: as long as \(n \geq 0\), after execution of the code, result = 0 + ... + n.

In other words, result contains the sum of the numbers from 0 to n inclusive. If we were to naively apply our rule, we would arrive at the following annotated code the loop body:

# {{ result + i = 0 + ... + n }}
result = result + i
# {{ result = 0 + ... + n }}
i = i + 1
# {{ result = 0 + ... + n }}

What does this precondition say? It says that we require that result = 0 + ... + n - i when we start the loop. However, this clearly does not hold beforehand! Taking this precondition backwards through our initialization of result and i with sequential reasoning yields:

# {{ 0 = 0 + ... + n }}
result = 0
# {{ result + 0 = 0 + ... + n }}
i = 0
# {{ result + i = 0 + ... + n }}

And this precondition—the sum of the numbers from \(0\) to \(n\) is \(0\)—is clearly not satisfiable!

What went wrong? Observe that it isn’t the case that result = 0 + ... + n holds before and after loop execution! Indeed, the point of the loop is for result to eventually contain this value! But this won’t be true until after the last iteration of the loop.

Instead of using our postcondition directly, we need to express the postcondition in terms of the variable(s) that drive the loop’s execution. This new postcondition should imply our desired postcondition once the loop finishes execution.

For the above example, we can use the following refined proposition instead:

# {{ result = 0 + ... + i-1 }}

In other words, result is the sum of the first i numbers we have encountered so far in the loop. Clearly, once we finish the loop, i = n + 1 and so result = 0 + ... + n as desired. So this new postcondition certainly implies our desired postcondition is true. However, is it an invariant of the loop? Analyzing the loop body shows this is the case:

# {{ result + i = 0 + ... + i }}
result = result + i
# {{ result = 0 + ... + (i + 1) - 1 }}
i = i + 1
# {{ result = 0 + ... + i - 1 }}

By subtracting i from both sides, we see that the final precondition can be rewritten as result = 0 + ... + i - 1 (keeping in mind that the term before i in the repeated addition is i - 1). Thus, we know that result = 0 + ... + i - 1 is an invariant of the loop. We work backwards from here to ensure that our original precondition, \(n \geq 0\), sufficiently covers the precondition we generate with our reasoning:

# {{ 0 = 0 }}
result = 0
# {{ result = 0 }}
i = 0
# {{ result = 0 + ... + i - 1 }}

We obtain the precondition to i = 0 by observing that the repeated sum ranges from 0 to 0 in this case.

Exercises

Exercise (Assignment Chain, ‡): Consider the following program:

# x is already defined
y = x * 2
z = x - 3

Prove the following claim about this program using Hoare logic:

Claim: if \(-2 \leq x \leq 0\) then \(y > z\).