How do I use the loop invariant to show that this code correctly computes $\sum_{k=0}^{n-1} 2k$?

Question

I am supposed to use the loop invariant (I) to show that the code below correctly computes $$\sum_{k=0}^{n-1} 2k$$

evenSum(int n){
   p = 2(n-1)
   i = n-1
   while i>0 do{
      //(I)  $p=\sum_{k=i}^{n-1} 2k$
      i--
      p = p+2i
      }
   return p
}

For clarity, (I) in the code above is $$p = \sum_{k=i}^{n-1} 2k$$ Here's my work so far:

1. Proving the base case of the loop invariant (I): $$p=2(n-1);$$ $$ i = n-1; $$ $$\sum_{k=i}^{n-1}2k = \sum_{k=n-1}^{n-1}2k= 2(n-1) \Rightarrow \sum_{k=i}^{n-1}2k = p$$
2. Inductive step: Assume (I) is true before an iteration $$p_{old}= \sum_{k=i_{old}}^{n-1}2k$$ We need to prove (I) is true after an iteration $$p_{new}= \sum_{k=i_{new}}^{n-1}2k$$

So, I'm stuck on completing the proof. I know that I need to utilize $p = p + 2i$ from the code, perhaps setting it up as $p_{new} = p_{old} + 2(i_{old}-1)$? I'm uncertain as to how to complete my proof, any help or input would be appreciated!

Answer 1

evenSum(int n){
   p = 2(n-1)
   i = n-1
   while i>0 do{
      //(I)  $p=\sum_{k=i}^{n-1} 2k$
      i--
      p = p+2i
      }
   return p
}

For the inductive step,

assume (A) $p=\sum_{k=i}^{n-1} 2k$ holds.

next iteration i and p have changed.

So we will need to prove (B) $p+2(i-1)=\sum_{k=i-1}^{n-1} 2k$ and we have the assumption i-1>0 available too, otherwise the loop would have ended.

Subtract $2(i-1)$ from both sides of (A) to prove (B).