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' }}
```

## 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:
s1else:
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:
s1else:
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:
= x
z else:
= y z
```

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 }}
= x
z # {{ 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 }}
= y
z # {{ 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:

- When executing
`s`

, we gain the assumption that`e = True`

. - As a postcondition of executing the loop, we know that
`e = False`

. Otherwise, we would still be in the loop.

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
= 0
result = 0
i while i <= n:
= result + i
result = i + 1 i
```

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 + i
result # {{ result = 0 + ... + n }}
= i + 1
i # {{ 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 }}
= 0
result # {{ result + 0 = 0 + ... + n }}
= 0
i # {{ 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 + i
result # {{ result = 0 + ... + (i + 1) - 1 }}
= i + 1
i # {{ 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 }}
= 0
result # {{ result = 0 }}
= 0
i # {{ 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
= x * 2
y = x - 3 z
```

Prove the following claim about this program using Hoare logic:

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