Hoare Logic, while loop with '<= '

Question

I'm working on some Hoare logic and I am wondering whether my approach is the right one.

I have the following program P:

s = 0
i = 1
while (i <= n) {
    s = s + i
    i = i + 1
}

It should satisfy the hoare triple {n >= 0}P{s = n*(n+1)/2} (so it just takes the sum). Now, initially I had |s = i*(i-1)/2| as my invariant, which works fine. However, I had a problem from going to the end of my loop, to my desired postcondition. Because for the impliciation

|s = i*(i-1)/2 & i > n|
=>
| s = n * (n+1) / 2 |

to hold, I need to prove that i is n+1, and not just any i bigger than n. So what I thought of is to add a (i <= n + 1) to the invariant, so that it becomes :

|s = i * (i-1)/2 & i <= n+1|

Then I can prove the program so I think it should be correct.

Nonetheless, I find the invariant to be a bit, less "invariantly" :). And not like anything I've seen in the course or in the exercises so far, so I was wondering if there was a more elegant solution here?

Answer 1

There is another way to reason,given a more appropriate invariant (and other code)...searh n for final value of i...

I : s = i*(i+1)/2 and 0 <= i <=n

B : i < n

Now,evidently you have for post condition:

I and i >= n =>  s = i*(i+1)/2 and i=n => s = n*(n+1)/2

The code now becomes

s = 0
i = 0
while (i < n) {
    s = s + (i+1)
    i = i + 1
}

The invariant holds at init and keeps after each loop,since rewriting I as 2s=i*(i+1) we have to proof

 I and i<n => 2(s + (i+1)) = (i+1)*(i+2)


2(s + (i+1) )= 
2s + 2(i+1) =
i*(i+1) + 2(i+1)= (since I holds)
(i+1)(i+2)

Qed.

Answer 2

So what I thought of is to add a (i <= n + 1) to the invariant, so that it becomes :

|s = i * (i-1)/2 & i <= n+1|

Nonetheless, I find the invariant to be a bit, less "invariantly" :). And not like anything I've seen in the course or in the exercises so far, so I was wondering if there was a more elegant solution here?

Nope, given the way the code is written, that's exactly the way to go. (I can tell from experience since I've been teaching Hoare logic during several semesters in two different courses and since it's part of my graduate studies.)

Using i <= n is common practice when programming. In your particular program, you could just as well have written i != n+1 instead, in which case your first invariant (which indeed looks cleaner) would have sufficed since you get

| s=i*(i-1)/2 & i=n+1 |
=>
| s=n*(n+1)/2 |

which evidently holds.