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:

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

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

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

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.

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

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

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

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

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

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

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.

# n is predefined

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

We start our proof by formally naming our loop invariant (in terms of the variable(s) that drive the loop’s execution):

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

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

result = 0
for i in range(n+1):
    result = result + i