CS 245 — Lecture 21

While Loops and Total Correctness

While Loops

Let's define the inference rule in our proof system for while loops.

Definition 21.1. $$\frac{\llparenthesis \eta \wedge B \rrparenthesis C \llparenthesis \eta \rrparenthesis}{\llparenthesis \eta \rrparenthesis \text{ while $B$ $\{C\}$ } \llparenthesis \eta \wedge (\neg B) \rrparenthesis } \text{(partial-while)}$$

The formula $B$ is called the loop guard and this rule is called partial-while. The reason it is called partial-while is because this rule is only sufficient to prove partial correctness. Generally, a proof involving a while loop with precondition $\varphi$ and postcondition $\psi$ will look like

Like all of the rules we've seen, it looks like the application of the inference rule for partial-while follows our strategy of pushing the postcondition up through each block. However, the partial-while gives us our first new challenge.

The formula $\eta$ is called the loop invariant. It is called as such because it needs to hold:

• before entering the loop,
• before each iteration of loop execution,
• after each iteration of loop execution,
• after exiting the loop.

Since it remains the same by the end of each iteration of the loop, it is invariant (the adjective). In essence, the loop invariant describes the behaviour of the loop.

Determining what the loop invariant should be is not as mechanical as applying our other rules. The invariant must be weak enough to be implied by our precondition and strong enough to imply our postcondition. Unfortunately, there is no algorithm that will tell us what loop invariant we should use. One way to do this is to consider a candidate invariant and run a few iterations of the loop to see if it works.

Example 21.2. We will consider the following proof of a program for computing $y = x!$.

First, we need some intuition about how the loop should work. Let's examine a particular run of the program.

From this, we have some possible loop invariants: $y = z!$, $y \geq z$, $x \geq 0$. The only one that will be useful is the first. Remember that we need our invariant to be able to prove the postcondition at the end.

Now, we will prove each of the implications.

1. We have $(x \geq 0) \vdash (1 = 0!)$ by definition of $0!$.
2. To see $((y = z!) \wedge \neg(z = x)) \vdash (y \cdot (z+1) = (z+1)!)$, we observe that \begin{align*} y &= z! \\ y \cdot (z+1) &= z! \cdot (z+1) \\ y \cdot (z+1) &= (z+1)! \end{align*}
3. To see that $((y = z!) \wedge (z = x)) \vdash (y = x!)$, we simply apply transitivity of equality.

Thus, we have proved that this Hoare triple is satisfied under partial correctness.

Total Correctness

So far, partial correctness has been enough to get us by, since the termination of the programs we've looked at so far is not really in question. That changes with the introduction of loops. So it is time to properly define total correctness.

Definition 21.3. A Hoare triple $\llparenthesis \varphi \rrparenthesis P \llparenthesis \psi \rrparenthesis$ is satisfied under total correctness if it is satisfied under partial correctness and, whenever $P$ starts in a state satisfying the precondition $\varphi$, it follows that $P$ terminates.

The difference that total correctness adds is that we must now show that our programs terminate as well. For everything that we've been doing so far, this is not really necessary, since there is no way for our programs to not terminate. However, with loops, we now have a way to shoot ourselves in the foot if we're not careful.

Thus, in order to prove that a program will terminate, we have to say something about the loop guard. A general strategy is to identify an integer expression which is always non-negative and whose value decreases every time through the while loop. Then, we can identify when the loop will eventually cause our expression to reach zero and cause the program to terminate. Such an expression is called a variant.

Example 21.4. Let's revisit Example 21.3. To show that this Hoare triple is satisfied under total correctness, we need to argue that the program will halt. To do this, we examine the loop guard, $z \neq x$. We observe that this is just $x - z \neq 0$ and we will choose $x-z$ to be our loop variant. If we examine the code, we see that at the beginning of the loop, we have $x-z = x \geq 0$. Then within each iteration of the loop, $x-z$ decreases by one. This means that the value of $x-z$ eventually reaches 0 and since $x-z$ is finite, this will occur in a finite number of steps. Thus, the loop will eventually exit and the program will terminate.

Therefore, there is a two step process to proving that a Hoare triple $\llparenthesis \varphi \rrparenthesis P \llparenthesis \psi \rrparenthesis$ is satisfied under total correctness.

1. Show that $\llparenthesis \varphi \rrparenthesis P \llparenthesis \psi \rrparenthesis$ is satisfied under partial correctness by providing a valid proof tableau/code annotation.
2. Argue that $P$ will terminate.

Obviously if $P$ doesn't contain any loops, arguing step 2 is trivial.

Example 21.5. In this offering of the course, we have chosen to prove total correctness by proving partial correctness and then proving termination separately. However, one can redefine the partial-while inference rule into a total-while inference rule that incorporates the notion of the loop variant. Please note that this is for illustrative purposes only. Do not do this on assignments and the exam.

Such a rule would look like $$\frac{\llparenthesis (\eta \wedge B) \wedge (0 \leq E = E_0) \rrparenthesis C \llparenthesis (\eta \wedge (0 \leq E \lt E_0)) \rrparenthesis}{\llparenthesis \eta \wedge (0 \leq E) \rrparenthesis \text{while $B \{C\}$} \llparenthesis \eta \wedge (\neg B) \rrparenthesis}\text{(total-while)}.$$

In this case, $E$ is the loop variant. The rule now has an additional condition for the loop variant: by the time an iteration of the loop ends, it must have decreased. This is reflected by the condition that $E = E_0$ before running $C$ and $E \lt E_0$ after running $C$.

Furthremore, in order to guarantee that only a finite number of iterations is ever run, we also have the condition that $E$ is bounded from below by 0. Since our previous conditions have that $E$ is always decreasing with each iteration, if we have everything set up properly, $E$ should reach 0 coinciding with exiting the loop.

A proof using this rule would look like the following, taking $E = x$ as our loop variant.

Since the total-while rule has the additional condition on the loop variant $E$, we can guarantee that our loop is appropriately set up (otherwise, we wouldn't be able to come up with a valid proof) and there's no need to prove termination separately.

Ideally, we want our proof system to be able to prove total correctness without having to prove termination separately and this rule allows us to do that. In addition to being very tidy theoretically, this has practical purposes like allowing the automation of the construction of the proof. However, this complicates proofs when humans are constructing them by hand, which is why we opted not to go this route for this course.