Finding a loop invariant - Hoare Triple

Question

From the following code, I need to deduce/choose a loop invariant.

(|true|)
x = 0 ;
s = 0 ;
while ( x <= n ) {
    s = s + x ;
    x = x + 1 ;
}
(|s = n(n + 1)/2|)

Solution given was

• s = (x-1)*x/2 ∧ (x ≤ n +1)

I don't quite understand how it has reached the solution above.

Please, help me with how to derive such solution or other loop invariant from the code.

Answer 1

Given the invariant, you can easily check that it is true before, within, and after the loop (yes, adding up integers from 1 to n inclusive gives you (n+1)*n/2 - see triangular numbers ). Since it covers all relevant variables in the loop (x and s), and cannot be further refined (well, you could add ^ x >= 0), it is indeed the invariant.

To deduce it by yourself, I am afraid that you need to know about triangular numbers (or the half-the-square) formula beforehand. You can of course write out that s = sum of integers from 1 to x for that part, and I for one would take it as a valid invariant. The part where x <= n+1 is comparatively easy.

A layman's way of finding invariants is to try to write out what the variables of the loop do during their lifetime inside the loop:

• s always holds the sum of integers up to x
• x goes through the integers from 0 to n, inclusive

And then writing it out in math.