Hoare logic - total correctness of loops
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} &lt; 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} &lt; 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} &lt; 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} &lt; v_0]$

we can obtain (by PrePost) 

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

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