I'm studying Hoare logic and I can't understand the relation between partial and total correctness regarding loop invariant. Suppose for example that I have the following program:
{X ≥ 0}
Y := 0;
Z := 0;
{Y =2Z}
while (Z ̸= X) do (
Z := Z + 1;
Y := Y + 2 )
{Y =2X}
The solutions says that for partial correctness I can use the invariant Inv = 2Z. But when I have to prove total correctness the invariant must be strengthened with X - Z >= 0. Which is the hoare logic property that let me strength the invariant, adding the condition to it, only for total correctness?