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
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.
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:
And then writing it out in math.