# Loop Invariant summation

So I am stuck:

I have this algorithm from which I need to find a loop invariant but I just can't get my head around it :

main_f = x
follow_up = x
while (follow_up < y):
follow_up = follow_up + 1
main_f = main_f + follow_up

return main_f


So basically I have a list of values of this function(main_f):

Initialisation : i = 0 , main_f = x

Iteration 1: i = 1 , main_f = 2x+1

Iteration 2: i = 2 , main_f = 3x+3

Iteration 3: i = 3 , main_f = 4x+6

Iteration 4: i = 4 , main_f = 5x+10

Iteration 5: i = 5 , main_f = 6x+15

And basically it goes on and on like this in a while (main_f < y) loop;

The loop invariant is certainly a sigma from i=x to y with the "x" part: (i+1)x but i can't find the formula that fits the integer part I got after the iterations.

• Why did you delete (again) the algorithm? – Yuval Filmus Oct 3 '18 at 5:33
• Sorry I was just editing with the old version – Sami Oct 3 '18 at 5:34

From your table, the following is apparent: at iteration $$i$$, $$\text{main_f} = (i+1)x + \binom{i+1}{2}.$$ You should be able to prove this formula by induction.