# How to prove that this while loop calculates n^2

I'm studying for my exam of logic later this week and I have to prove that this while loop:

``````i := 0
s := 0
while i < n do
i := i + 1
s := s + (2*i -1)
``````

calculates n^2. This question is made up of 2 subquestions. We have to prove that 0 ≤ i ≤ n ∧ s = i^2 is a loop invariant for this while loop. I managed to prove that, but the second subquestion is that I have to prove that this loop calculates n^2, but I don't really know how to start. The course is a bit confusing about this part of the question.

The loop calculates 1 + 3 + 5 + 7 + ... + (2n-1). The easiest way to visualise that this sums to n^2 is • This is by far the best answer one could give for this answer. @PieterVerschaffelt you should accept the answer. – Silviu Burcea Jan 13 '15 at 9:48

Using the formula of arithmetic progression we can derive it directly:

number of elements is `n`, first element is `1` last element is `2*n-1`

``````n*(1 + 2*n-1)/2 = n*(2*n) /2 = n*n
``````

Existing answers have missed an important point: the OP has already proved some things, and the practice exam question asked him to prove these things first. Presumably, this is because the things he's already proved are meant to be handy stepping stones towards finishing the proof.

We want to prove that the program outputs n^2. Since there are no output statements, presumably one of the variables is the output, and it isn't `i`, so it must be `s`.

We already have s=i^2, so we're actually really close; wouldn't it be nice if i=n at the end of the loop? Turns out, i=n is true at the end of the loop. And we're done.

When proving things, it's very often helpful to look at other things we've already proved and what we're trying to prove. Similarities between what we have and what we want can be suggestive of things to try.

• Thank you! That's indeed very useful. Turns out it wasn't very difficult to prove it from what I had when I see you're answer :) – Pieter Verschaffelt Jan 14 '15 at 18:12

You could also prove this by a method called 'mathematical induction', which works for positive integers.

To put it simply: You assume that you statement about the loop is true for a arbitrary 'n' and so it's also true for 'n+1' and therefore for every integer bigger than your lower border (which normally is 1, but in your case, 0 works as well).

It's a way more mathematical approach and so you may like it or you hate it. But here we go: If you're not familiar with the sigma operator in mathematics, this is how it works. It's simply a 'for' loop, with 'a' being the starting value and 'b' being the included upper limit. It increases 'a' every 'iteration' by one and sums the values together.

So mathematically, your problem could be written like this: Now, for mathematical induction to work, we first have to prove that this statement is true for the lowest value of 'n' (this would normally be 1, but 0 works here as well): Which definitely is true. And thats true as well.

Great, so let's move on to the 'exciting' part... Proving this statement for any (positive integer) 'n' by replacing 'n' with 'n + 1': Now, this looks quite complicated, but let's analyse it step by step. The first part is exactly the same as in the second picture, but now every 'n' is replaced by 'n + 1'. The second part (after the '->' and there especially the left side of the equation) may not be obvious at the first glance. But from a programmers point of view it might be a bit easier to understand, because

``````for(int i = 0; i <= n; i++)
{
...Do sth here.
}
``````

is exactly the same as

``````for(int i = 0; i <= l; i++)
{
...Do sth here (part 1)
}

for(int i = l + 1; i <= n; i++)
{
...Do sth here (part 2)
}
``````

On the right side of the equation I simply expanded '(n + 1)^2' to 'n^2 + 2n + 1'. Now the final spurt: Since for our second 'loop' (=sigma operator) the upper value equals the lower value, we don't need it at all. There's only one iteration with this particular value, so we simply can replace 'k' with 'n + 1', which then gives us '2*(n + 1) - 1'. So we now have still the same sigma left, which we had in the beginning and we wanted to prove being 'n' squared. So to get rid of it, we simply can replace it by 'n^2' in the second part (after the '->'), because if our assumption is true, there is no difference between them. We now have 'n^2' on both sides, so we can simply subtract it to get rid of it as well. So whats now left we can simply out multiply and eventually get an equation, which is true as well. Therefore we have proven that a loop summing up all odd numbers (starting from 1 up to '2n - 1') equals 'n^2'.