One of the questions in the problem sets that I'm struggling in is this specific number that asks me to prove an iterative Fibonacci algorithm. The algorithm is written below:
if n = 0 then
a = 0; b = 1; i = 2;
while i <= n do
c = a + b
a = b
b = c
i = i + 1
The way too prove correctness, according to my professor was to make sure that there are these three steps:
- Initialization - the loop invariant must hold true prior to the first iteration
- Maintenance - the loop invariant must hold true after an iteration
- Termination - the loop invariant must hold true when the loop terminates
The loop invariant I've chosen is
a <= b since I find this to be true for steps 1 through 3. First of all, I'm not sure if this is a valid loop invariant and this is the only observation I saw since
i <= n isn't always true for inputs
n that are natural numbers.
Assuming that I've chosen the correct loop invariant, I need to answer the proof by doing three steps so for this number I plan to answer it this way
- Initialization - before the start of the loop
ais assigned a value of 0 while
bis assigned a value of 1 which starts the Fibonacci sequence.
a <= bholds true prior to the start of the loop
- Maintenance - during the loop, another variable
cis added such that it is equal to the sum of
b. After which,
bis assigned to variable
cis assigned to
bthus making the invariant
a <= btrue during the iteration.
- Termination - the loop ends when
i > n. Before
iis incremented, the procedures in the maintenance step is still done, thus the loop invariant still holds true
For my questions, is my loop invariant
a <= b correct? And are the three statements I mentioned above sufficient to prove the correctness of an iterative Fibonacci algorithm?