Hoare logic - total correctness of loops
-
04-11-2019 - |
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