Hoare Logic - Exactitude totale des boucles

Question

Considérez une boucle de la forme:

$ texttt {while (c) {s}} $

avec $ texttt {c} $ la condition et $ texttt {s} $ le corps de la boucle.

Soit $ texttt {i} $ et $ texttt {v} $ respectivement être un invariant et une variante de cette boucle. La règle pour l'exactitude totale de While Loops est donnée dans mon manuel par:

Si $ texttt {i} rightarrow texttt {v} geq 0 $

Et $ [ texttt {i} land texttt {c} land texttt {v} = v_0] , texttt {s} , [ texttt {i} land texttt {v} <v_0] $

Alors $ [ texttt {i}] , texttt {while (c) {s}} , [ texttt {i} land neg texttt {c}] $

D'après ce que je pense que je comprends, pour que la boucle se termine, la variante $ texttt {v} $ doit être striquement diminuée et qu'elle doit également être bornée par zéro. Cependant, lorsque je traduis cela mathématiquement, j'obtiens une proposition différente de celle de mon manuel:

$$ [ texttt {v} geq 0 land texttt {v} = v_0] , texttt {s} , [ texttt {v} geq 0 land texttt {v} <v_0] $ $

Ma question : Cette dernière proposition et la règle de mon manuel disent-elles la même chose sur ce qui doit être prouvé pour que la boucle se termine? En d'autres termes: est

$ [ 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] $

le même que

$ texttt {i} rightarrow texttt {v} geq 0 $ avec $ [ texttt {i} land texttt {c} land texttt {v} = v_0] , texttt {s} , [ texttt {i} land texttt {v} <v_0] $

Pourquoi ou pourquoi pas?