# Wrong Invariant?

• Sep 14th 2012, 08:43 PM
gomdohri
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
• Sep 14th 2012, 09:29 PM
chiro
Re: Wrong Invariant?
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)?
• Sep 14th 2012, 11:25 PM
gomdohri
Re: Wrong Invariant?
Extremely simple invariant - something that never changes so here I am looking for the good loop invariant
• Sep 14th 2012, 11:47 PM
chiro
Re: Wrong 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)?
• Sep 15th 2012, 05:55 AM
emakarov
Re: Wrong Invariant?
Quote:

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).
• Sep 15th 2012, 01:28 PM
gomdohri
Re: Wrong Invariant?
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
• Sep 15th 2012, 02:05 PM
emakarov
Re: Wrong Invariant?
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?