7
$\begingroup$

Consider a while loop of the form :

$\texttt{while (C) {S}}$

with $\texttt{C}$ the condition and $\texttt{S}$ the body of the loop.

Let $\texttt{I}$ and $\texttt{V}$ respectively be an invariant and a variant of this loop. The rule for total correctness of while loops is given in my textbook by:

If $\texttt{I} \Rightarrow \texttt{V} \geq 0$

And $[\texttt{I} \land \texttt{C} \land \texttt{V} = v_0] \,\texttt{S} \, [\texttt{I} \land \texttt{V} < v_0]$

Then $[\texttt{I}] \, \texttt{while (C) {S}} \, [\texttt{I} \land \neg \texttt{C}]$

From what I think I understand, in order for the loop to terminate, the variant $\texttt{V}$ must stricly decrease and that it must also be bounded by zero. However, when I translate that mathematically, I obtain a different proposition from that of my textbook :

$$[\texttt{V} \geq 0 \land \texttt{V} = v_0] \, \texttt{S} \, [\texttt{V} \geq 0 \land \texttt{V} < v_0]$$

My question : Are this last proposition and my textbook's rule saying the same thing about what needs to be proven in order for the loop to terminate? In other words : is

$[\texttt{I} \land \texttt{C} \land \texttt{V} \geq 0 \land \texttt{V} = v_0] \, \texttt{S} \, [\texttt{I} \land \texttt{V} \geq 0 \land \texttt{V} < v_0]$

the same as

$\texttt{I} \Rightarrow \texttt{V} \geq 0$ together with $[\texttt{I} \land \texttt{C} \land \texttt{V} = v_0] \,\texttt{S} \, [\texttt{I} \land \texttt{V} < v_0]$

Why or why not?

$\endgroup$
  • $\begingroup$ The claim that "𝚅 must stricly decrease and that it must also be bounded by zero" is sufficient is misleading. You also need that 𝚅 is a function with a well-founded range. Just imagine using the non-negative rational numbers instead and construct a counter-example. $\endgroup$ – Kai Sep 22 '17 at 13:47
5
$\begingroup$

They are equivalent, in the sense that every time you can apply the textbook rule you can also apply your own rule, and vice versa. The invariant for the two rules is similar, but not the same.

Converting a textbook rule instance into an instance of your rule

Suppose we have an application or your textbook rule. I.e., we have found some $\texttt{I}$ for which:

$\texttt{I} \Rightarrow \texttt{V} \geq 0$ together with $[\texttt{I} \land \texttt{C} \land \texttt{V} = v_0] \,\texttt{S} \, [\texttt{I} \land \texttt{V} < v_0]$

Then, thanks to the implication above, we also have $\texttt{I} \iff \texttt{I} \land \texttt{V} \geq 0$. Using rule PrePost, we can rewrite the invariant into its equivalent, and we get an application of your rule:

$[\texttt{I} \land \texttt{C} \land \texttt{V} \geq 0 \land \texttt{V} = v_0] \, \texttt{S} \, [\texttt{I} \land \texttt{V} \geq 0 \land \texttt{V} < v_0]$

Here, we use the same invariant as in the textbook rule.

Converting an instance of your rule into a textbook rule instance

Now, for the converse direction. Suppose we have found $\texttt{I}$ for your rule:

$[\texttt{I} \land \texttt{C} \land \texttt{V} \geq 0 \land \texttt{V} = v_0] \, \texttt{S} \, [\texttt{I} \land \texttt{V} \geq 0 \land \texttt{V} < v_0]$

Now, we can't assume $\texttt{I} \Rightarrow \texttt{V} \geq 0$, so we can't use $\texttt{I}$ for the textbook rule. However, we can use as a new invariant $\texttt{I}' := \texttt{I} \land \texttt{V} \geq 0$. We trivially have $\texttt{I}' \Rightarrow \texttt{V} \geq 0$ by construction (*). Further, from the hypothesis

$[\texttt{I} \land \texttt{C} \land \texttt{V} \geq 0 \land \texttt{V} = v_0] \, \texttt{S} \, [\texttt{I} \land \texttt{V} \geq 0 \land \texttt{V} < v_0]$

we can obtain (by PrePost)

$[\texttt{I}' \land \texttt{C} \land \texttt{V} = v_0] \, \texttt{S} \, [\texttt{I}' \land \texttt{V} < v_0]$ (**)

Properties (*) and (**) are exactly what we need to apply the textbook rule.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.