Proof Loop Invariant

Question

I want to get the loop invariant of the following code snippet:

$(0 \le n)$ (precondition)

sign = 1;
res = 0;
i = 0;

while (i < n) {
   res = -(res + sign);
   sign = - sign;
   i = i +1;
}

$(res = (-1)^n*n)$ (postcondition)

My invariant: $i = sign * res$

I have done a few iteration steps to make clear that the invariant could be correct:

\begin{array}{|c|c|c|} \hline sign& res & i \\ \hline 1 & 0 & 0 \\ \hline -1 & -1 & 1\\ \hline 1 & 2 & 2\\ \hline -1 & -3 & 3 \\ \hline 1 & 4 & 4 \\ \hline \end{array}

Now I need to prove the loop variant via induction.

So I have started like that:

$res' = -(res + sign') $ and $ sign' = -sign$

$\Rightarrow res' = -(res + (-sign)) = -res-sign \Rightarrow -res = sign$

My induction step:

$ i' = i+ 1 $

$ res' = \frac{i + 1}{sign}$

Question: How can I go on ? My main problem is, that there are three variables in the equation and I do not know how to simplify the equation.

Answer 1

For convenient, let $res$ that corresponds to number $i$ be $r_i$ and $sign$ that corresponds to $i$ be $s_i$.

We want to prove that $i=s_ir_i$

where $r_{i+1}=-(r_i+s_i)$ and $s_{i+1}=-s_i$ and $r_0=0$ and $s_0=1$.

Notice that from iterations to iterations, $s_i$ just alternatives between $1$ and $-1$. (You might want to prove this)

Base case: since, $r_0=0$, we have $r_0s_0=0$.

Suppose that $i=r_is_i$.

Notice that $r_{i+1}s_{i+1}=(-(r_i+s_i))(-s_i)=(r_i+s_i)s_i=r_is_i+s_i^2=i+1.$

Remark: Your mistake was a typo at the very first line of your proof.

$res'=-(res+sign)$