For (1):
if you expand $(i+1)^2$ you get $i^2+2i+1$.
You should know that, so I'm not sure if I interpreted your question correctly.
For 2):
Since $i_{new}=i+1$, $\;\;i^2_{new}=(i+1)^2$
What is a loop-invariant?
A loop-invariant is a statement that you can make about variables in a program that will be true at the end of each iteration of a loop.
For example, $i\in N$, $i\leq n$ and $s=i^2$ are all loop-invariants.
The purpose of a loop-invariant is to help you prove that a program is correct.
For example, suppose it is claimed that sum($n$) produces $n^2$ for all positive integers $n$.
First, you prove that $s=i^2$ is a loop-invariant using induction.
Next, you note that at the end of the $k^{th}$ iteration of the loop, we have $i=1+k$ and that the loop terminates after the $(n-1)^{th}$ iteration.
This means that when the loop terminates after $k = (n-1)$ iterations we have:
$s=i^2=(1+k)^2=(1+(n-1))^2= n^2$
Hope this helped.
First of all, yes, the loop invariant must be true before we start the loop, after each iteration, and after the loop completes.
See https://en.wikipedia.org/wiki/Loop_invariant, http://www.cs.miami.edu/home/burt/learning/Math120.1/Notes/LoopInvar.html, any of several other pages from university course notes that you'll find if you search for "loop invariant", or (presumably) your textbook.
In the most general sense, finding a loop invariant is about constructing
a mathematical proof, and there is not a simple set of instructions that will
give a good invariant whenever one exists. But if you have an inductive definition of the result of the algorithm, as you do here, your invariant might
also look like an inductive definition.
In this case you have that for all $i>1$, $F(i) = F(i-1) + F(i-2)$.
You also know the values of $F(0)$ and $F(1)$.
This suggests an algorithm in which before the first iteration of a loop,
you store the values $F(0)$ and $F(1)$ in two variables, $A$ and $B$, respectively, and you maintain the invariant that $A=F(k)$ and $B=F(k+1)$
where $k$ is the number of iterations of the loop that have completed.
You can prove that the invariant is maintained by showing that at the end of
each loop, the value in $A$ is the value that previously was in $B$,
and the value in $B$ is the previous value of $A+B$.
That is, if at the end of $k$ iterations you had $F(k)$ stored in $A$ and
$F(k+1)$ stored in $B$, at the end of the next iteration
(that is, after $k+1$ iterations) you will have $F(k+1)$ stored in $A$
and $F(k+2) = F(k+1) + F(k)$ stored in $B$.
My $A$ and $B$ look suspiciously like your r
and l
, respectively.
But note that in the algorithm I described, $B$ will store $F(n)$ after only
$n-1$ iterations, while your algorithm is written to do $n$ iterations,
and to return the larger number at the end of the $n$th iteration.
Your algorithm resolves this by doing an extra iteration at the beginning,
that is, it starts by setting l
to $F(0)$ and r
to $F(-1)$,
respectively, where $F(-1)=1$ in order that $F(1) = F(0) + F(-1)$.
So after $k$ iterations, where $k\geq 0$,
your algorithm always has $F(k-1)$ stored in r
and $F(k)$ stored in l
.
Alternatively, rather than defining $F(-1) = 1$, you can write a special
case into your loop invariant for the case when you have completed $0$ iterations. That is what your proposed invariant does, which is fine.
One of the potential difficulties of writing loop invariants is notational.
The invariant as I stated it depends on knowing how many iterations of the
loop have been completed. You have a variable i
whose value during each
loop is clearly defined, but whose values at the beginning and end of each loop are not clear to me. At the end of the first loop, does i
store the value $0$
or the value $1$? You should have a clearly defined convention for some
kind of variable associated with a loop control such as for i in [0,n)
,
with clearly-defined values of this variable before the first iteration
of the loop and at the end of each iteration of the loop.
Your notes or textbook should have established a convention for how you
construct such a variable for such a loop.
Without a clearly established convention, I'm not sure whether l
at the
end of the last iteration is $f_n$ (which it is if $i$ in your invariant has
the value $k-1$ at the end of $k$ iterations)
or $f_{n+1}$ (which is what you get if $i$ denotes the number of iterations
that have been completed).
EDIT: "How I would have done it," not necessarily how you should do it:
If I were writing this for a formal methods course (or possibly even
in an ordinary program), I probably would have started by laying out the
base cases in code like this (using =
for an equality test, not assignment):
if n=0
return 0
else if n=1
return 1
else if n>1
... do loop ...
return result
Note that the return value is undefined if $n<0$. For $n>1$,
the loop would do $n-1$ iterations of the $A,B$ algorithm I described above,
and the result would be the last value of $B$.
I might then notice that the outcomes would be the same if I wrote
if n=0
return 0
else if n>0
... do loop ...
return result
That is, one of the "if" conditions was superfluous. But I cannot get rid of
the special handling of the case $n=0$ with the loop as written,
because the loop depends on doing $n-1$ iterations to produce $F(0)$,
and you can't do $-1$ iterations of a loop.
Best Answer
Let $f(n)$ be the $n^{th}$ term of the Fibonacci sequence.
A correct invariant would be, for example: " At the end of an iteration , $y=f(i-1)$ and $x=f(i)$ " It is true for the first iteration ($i=2, y=1, x=1$), and stays true during the loop due to the definition of $f$ ($f(n)=f(n-1)+f(n-2)$ for $n > 1$).
Hence, at the end of the loop, $x=f(i)=f(n)$, so the function returns the correct value.