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?

  • $\begingroup$ 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. $\endgroup$ – D.W. Feb 23 '15 at 19:42

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).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.