Thread: Wrong Invariant?

Hi, I am working through Hoare Logic problem, I think my invariant is wrong but I cannot think of the good invariant.. please help me with this.

The program:

{n >= 0}

x := 0;
t := 0;
while ( x < n ) do
x := x+1;
t := t+x;
{t = (n^2 + n) / 2}

My invariant was (t = (x^2 +x ) / 2) but it seems that it is wrong

Hey gomdohri.

Can you explain in simple terms what the invariant corresponds to (for someone that is not familiar with the terminology in Hoare logic)?

Extremely simple invariant - something that never changes so here I am looking for the good loop invariant

Are you talking about in the loop (where you want t to be a function of x explicitly) for each iteration of t?

If that is the case then I agree with you on the formula you have. Did you try and test it within your code (by using a print statement)?

Originally Posted by gomdohri

My invariant was (t = (x^2 +x ) / 2) but it seems that it is wrong

I think the invariant is correct. Why do you think it is wrong? The only problem is that it does not allow proving that t = (n^2 + n) / 2 after the loop. The Hoare logic rule for while is

Code:

       {P /\ B} S {P}
-------------------------------
{P} while B do S done {~B /\ P}

So, with the invariant t = (x^2 + x) / 2 we can only conclude that x >= n /\ t = (x^2 + x) / 2; we can't conclude that x = n. Can you think of how to change the invariant to be able to deduce x = n after the loop?

By the way, you should indicate somehow that the body of the loop consists of two assignments (e.g., by placing "done" or "end" after the body of the loop).

Sorry for the confusion here yes, the problem with my invariant is that I cannot prove that t = (n^2 + n) /2 after the loop so that is why I had to change the invariant. However, since I am not really familiar with Hoare logic, I could not think of the invariant that also proves t = (n^2 + n) / 2

The part of the invariant you are missing is not related to t. Basically, you need to deduce the following.

Code:

{x <= n}

while (x < n) do
  x := x+1;
done;

{x = n}

The rule for while allows you to conclude that the loop guard (i.e., x < n) is false after the end of the loop, so you know that x >= n after the loop. You also need to know that x <= n. What should the invariant for the program above be?