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.
Loops
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 thate = 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. Since \(i-1<0\), we do not
include that last value in the sum. This is common notation with
summations: we don’t allow subsequent values to be less than the
original value when writing it generally. You can think of the statement
‘result = 0 + ... + i-1
’ as actually saying
‘result = 0 + ... + i-1
for \(i>0\) and result=0
for
\(i\leq0\)’.
Inductive Reasoning about Loops
Now that we have worked through our rule for while loops, let’s take a moment to tease out the details of the formal proof technique that we have used: induction.
To formally prove the truth of our invariant P
, we need
to reason in three major steps:
- Initialization. We need to show that
P
is true before the loop begins. - Maintenance. We need to show that the invariant remains true during execution of the loop.
- Termination. We need to show that the loop actually terminates.
If all three of these steps hold, then we can conclude that the invariant holds before and after execution of the loop, as desired.
The first step of this process, initialization, is essentially the base case of our proof, and will need to be proved using only the assumptions of our original claim, the preconditions we have received from earlier in our code, and any mathematical axioms we made need to cite.
The second step of this process, maintenance, is the heart of the inductive proof. We want to show that the invariant remains true during execution of the loop. Well actually, that is a lazy way to phrase what we need to prove. We don’t need the invariant to be true at every moment of execution, but rather, we need the invariant to be true at the end of each iteration. If we return to our definition of an invariant, it is a property that is true before and after execution of a piece of code. The definition does not require that the invariant hold true at every moment during the execution of the code, merely that it is a precondition and postcondition of the code.
Consider the following loop. We can easily see the that the claim \(n \equiv i\) is an invariant of this loop.
= 0
i = 0
n while i < 5:
+= 1
i += 1 n
However, there are a few moments during execution when \(n\) and \(i\) have different values. During the first
iteration of the loop, both \(n\) and
\(i\) are \(0\). However, after we execute the line
i += 1
, we have \(i=1\)
while \(n=0\) still! But this isn’t a
problem, because we immediately execute n += 1
and restore
our invariant. The main takeaway from this example: our invariant only
needs to hold at the end of each iteration. That way we can safely claim
that it holds when the loop terminates. Technically, we must be a bit
careful of things like break
statements in the body of our
loop. If we terminate an iteration early, we will have some extra work
to do to prove that the invariant does properly hold at termination.
So let’s redefine our maintenance step’s goal with this new
understanding. We are not trying to show that the invariant holds during
execution of the loop. Instead, the maintenance step
requires us to prove that the invariant is true at the end of
each iteration of the loop (even if that iteration ends early due to the
presence of a continue
or break
statement).
But how do we show that the invariant is true at the end of ‘every iteration of the loop’? That’s where our inductive reasoning comes in! Let’s assume that the invariant is true at the end of the \(n-1\) iteration of the loop (our inductive hypothesis), and use that fact to help prove that the invariant is true at the end of the \(n\)th iteration. In other words, we are assuming that the invariant is a precondition of the current iteration, and using that fact to prove that it is also a postcondition of the current invariant. Recall that this is exactly what was required in our Hoare Logic Rule:
# {{ P ∧ e = True }}
s# {{ P }}
P
had to be both a precondition and postcondition of
s
, the statement executed within the loop!
The initialization step was our base case, and proved that the invariant was true at the start of the first iteration. Our maintenance step then tells us that if it is true at the end of the previous iteration (which is also the start of the current iteration), then it is true at the end of the current iteration. Putting these together works just like an inductive proof: we can conclude that the invariant is true at the end of the first iteration, and that it is therefore true at the end of the second iteration, and that it is therefore true at the end of the third iteration, etc.
The third step of this process, termination, is
where these loop invariant proofs differ from our regular inductive
outline. In an inductive proof, we are not concerned with if or when the
process will end. After all, we are typically trying to prove that the
claim is true ‘for all n
’. But for a loop invariant, our
goal is to be able to reason about the relationship of the preconditions
before the loop and the postconditions after the loop. Which of course,
requires that the loop actually terminates. So as a final step of the
proof process for invariants, we must prove that the loop terminates to
conclude that the invariant is true after the loop’s execution. This
step is fairly trivial for a for
loop, but can be a bit
more complicated for a while
loop.
Using this ‘initialization, maintenance, termination’ outline for proving loop invariants, let’s revisit the claim from earlier.
Claim: as long as \(n \geq
0\), after execution of the code,
result = 0 + ... + n
.
# n is predefined
= 0
result = 0
i while i <= n:
= result + i
result = i + 1 i
We start our proof by formally naming our loop invariant (in terms of the variable(s) that drive the loop’s execution):
Loop Invariant: at the end of each iteration of the
loop, result = 0 + ... + i-1
.
Initialization: When the loop begins execution, we
know that result=0
and i=0
. Recalling that we
don’t include the i-1
term in the summation when \(i\leq0\), we can indeed conclude that
result = 0 = 0 + ... + i-1
as desired.
Maintenance: Assume that
result = 0 + ... + i-1
was true at the end of the previous
iteration. In other words, result = 0 + ... + i-1
is a
precondition of our current iteration of the loop! We now desired to
show that result = 0 + ... + i-1
is true at the end of the
current iteration, i.e., it is a postcondition of the current iteration.
We can see this through the following logic:
# {{ result = 0 + ... + i - 1 }}
# {{ result + i = 0 + ... + i }}
= result + i
result # {{ result = 0 + ... + (i + 1) - 1 }}
= i + 1
i # {{ result = 0 + ... + i - 1 }}
Termination: We must now show that the loop
terminates, and reason about our invariant once termination occurs. To
see that the loop terminates, consider the condition
i <= n
. We can see that if i
ever exceeds
the value of n
, then the loop will terminate. We note that
i = 0
at the start of the loop, and always increases in
value due to the i = i + 1
statement. Therefore we can
conclude that eventually it will be true that i > n
and
the loop will terminate. Moreover, we can reason that at termination,
not only will i > n
, but actually
i = n + 1
. This is because at the previous iteration, we
knew that i <= n
, and after executing the statement
i = i + 1
, now i > n
. This can only happen
if i = n + 1
when the loop terminates.
We now know that at termination, i = n + 1
and
result = 0 + ... + i-1
. Therefore
result = 0 + ... + n
, proving our claim!
As a final note here: we got a bit lazy in the termination step of this process, and used a bit of mathematical reasoning to get us to the desired result. After all, our current rule only tells us:
# {{ P }}
while e:
s# {{ P ∧ e = False }}
So we can really only conclude that at termination,
i > n
, which is insufficient for our proof. We needed to
know that i = n + 1
specifically.
We could, however, prove this formally within the Hoare Logic
framework, though it would require a bit more effort. We properly should
augment our loop invariant to also reason about the value of
i
as the loop progresses. In a way that both lets us
conclude that the loop will eventually terminate, and that tells us that
i = n + 1
at termination.
Had we been reasoning about the following (equivalent)
for
loop instead, this termination process would have been
trivialized due to the nature of for
loops: we know that it
will terminate, and we precisely know the value of i
at
each iteration of the loop (and at termination).
# n is predefined
= 0
result for i in range(n+1):
= result + i result