Hoare logic - partial/total correctnes and strength invariant

Question

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?

Answer 1

You're misunderstanding. It's not that when you try to prove total correctness, Hoare logic somehow magically finds a stronger invariant for you. Hoare logic doesn't find the invariant for you -- either way, you have to find the invariant yourself and then prove it.

Rather, it's that you need to prove a stronger invariant if you want to prove total correctness. A weaker invariant can suffice to show partial correctness. Therefore, total correctness can often be harder to prove than partial correctness (proving total correctness requires more work, because you have to prove a stronger, more detailed invariant).