Let $n \in \mathbb{N}_0$ and $f: \mathbb{N}_0 \rightarrow \mathbb{N}_0$. The values of variables $y$ and $i$ are in $\mathbb{N}_0$.
Algorithm A:
$y \leftarrow f(0)$
$i \leftarrow 0$
while $i<n$ do
$\quad i \leftarrow i+1 \\ \quad y \leftarrow y + f(i)$
od
For $j \in \mathbb{N}_+$, $y_j$ and $i_j$ are the values after going through the loop $j$ times.
a)$f(x) = 2x$ and $n=4$. Calculate the values for $y_j$ and $i_j$.
$\begin{array} {|r|r|} \hline j & i_j & y_j \\ \hline - & 0 & 0 \\ \hline 1 & 1 & 2 \\ \hline 2 & 2 & 6 \\ \hline 3 & 3 & 12 \\ \hline 4 & 4 & 20 \\ \hline \end{array}$
b)How many times will the while loop be executed for any random $n$?
The while-loop will be executed n-times.
c)Which value will the variable y have after going through A, when $n \in \mathbb{N}_0$ is random and $f = I_{\mathbb{N}_0}$. (For a set M: $I_M = \{(x,x)|x\in M\}$)
$ \begin{equation} y(n) = \begin{cases} (0,0) & \text{if $n=0$}\\ (1,1) & \text{if $n=1$}\\ ([\sum^n_{i=0}i]-1,[\sum^n_{i=0}i]-1) & \text{otherwise} \end{cases} \end{equation} $
d)Prove the validity of the Hoare-Triple:
$\quad T: \{0=0\} A \{y= \sum ^n_{j=0} f(j)\}$
Find a loop invariant I for the while loop in A to prove the Hoare triple.
Prove in Hoare logic that I is a loop invariant.
Prove in Hoare logic that $\{0=0\} y \leftarrow f(0); i \leftarrow 0 \{I\}$ is a valid Hoare triple
Prove that $I \land \neg (i < n)$ implies the assertion $y = \sum^n_{j=0}f(j)$.
Hint: Make sure that "$\land i \leq n$" is part of your loop invariant I.
e)Find an arithmetic expression, which will become smaller after every execution of the while loop. Conclude that for any $n$ and any $f$ A will terminate.
How do I find the invariant and prove its validity?