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:
- 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:
= 1
x = x + 1
y = 5
x = x + 5 z
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:
= 1 + 1
y = 5
x = 1 + 5 z
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:
= 0
x if ... :
= 5
x 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
= x + 5 # Line (a)
y = x * 2 # Line (b)
x = y - x # Line (c) y
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 - x # Line (c)
y # {{ 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 * 2 # Line (b)
x # {{ y - x ≥ 0 }}
= y - x # Line (c)
y # {{ 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 }}
= x + 5 # Line (a)
y # {{ y - x * 2 ≥ 0 }}
= x * 2 # Line (b)
x # {{ y - x ≥ 0 }}
= y - x # Line (c)
y # {{ 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 }}
= x + 5 # Line (a)
y # {{ y - x * 2 ≥ 0 }}
= x * 2 # Line (b)
x # {{ y - x ≥ 0 }}
= y - x # Line (c)
y # {{ 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 - x # Line (c)
y # {{ 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 * 2 # Line (b)
x # {{ 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 }}
= e
x # {{ 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' }}
Exercises
Exercise (Finding Preconditions, ‡): Consider the following program:
# w is already defined
= w - 1
x = w + 1
y = x * y z
What precondition would be necessary to prove that at the end of execution, \(z>0\)?
What precondition would be necessary to prove that at the end of execution, \(z<0\)?
Remember that if the product of two numbers is positive, then the two numbers share a sign, i.e., they are either both positive or both negative.