Question

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?

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top