# Hoare logic - partial/total correctnes and strength invariant

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?

• What specifically are you confused about? Are you aware of the definition of total correctness and of partial correctness? Did you try proving total correctness using the simpler invariant? (whatever it is; I think it must have gotten scrambled somehow) What did you get? Where did you go wrong? Work through this step-by-step: you should be able to either figure it out on your own, or show us your work.
– D.W.
Feb 23, 2015 at 19:42