Proof of correctness (loop invariant) for Fibonacci numbers

Question

I'm an absolute beginner in programming. I'm trying to write a proof of correctness for the iterative programme of Fibonacci numbers, by specifying a pre-condition, post-condition and loop invariant.

int fib(int k)
{
    //fib(0)=0 and fib(1)=1
    if (k==0 || k==1) 
        return k;
    else
    {       
        int i = 1;
        int prev = 0;
        int last = 1;
        //Pre-condition: prev=0 and last=1 and i=>1
        //invariant: last=last+prev and prev=last-prev and 1<=i<=k
        while (i<k)
        {
            //last=last+prev=fib(i)+fib(i-1)
            last += prev;
            //prev=last-prev=fib(i)-fib(i-1)
            prev = last - prev;
            //i=i+1
            i++;
        }
        return last; //when the loop ends i=k and last=fib(k)
        //Post-condition: last=last+prev and prev=last-prev and i=k, i.e. last=fib(i), prev=fib(i-1) and i=k
    }
}

I understand that my invariant last=last+prev is true when prev=0 but prev=last-prev is not true. Would it be any better if I write it in terms of inductive function, i.e. last=fib(i)+fib(i-1) and prev=fib(i)-fib(i-1) and 1<=i<=k?

I have already made many attempts and I cannot progress further. Thanks for your help.

Answer 1

First off, you're going to have trouble using any invariant or similar analysis to prove that this program is correct, because it's not correct. If you had a working program, I could explain how to do the invariants to prove correctness; if you understood invariants I could explain how to use them to prove that the program you have is incorrect and how to fix it. But you seem to be trying to learn two things at once and since you don't have either of them yet, you have nothing solid to hold onto. You need to use a simpler example. Instead of trying to use this new technique to analyze a program that you don't have, you should use the technique to analyze a program you do have.

You seem to have a mistaken idea that preconditions, postconditions, and invariants are pieces of program code. They are not. They are claims, assertions, or statements that express our desire about what we hope the program will do. They say what we want done, not how it is done.

The conditions are often, but not always, in mathematical language. They can be in English, or in mathematics, or in a combination. They should be things like “The first $i$ elements of the array are in increasing order” or “$v$ is a power of 2”: things we would like to be true, or things that we know are true.

The meaning of the = symbol in programming languages is quite misleading, not what you are used to, and is a frequent cause of confusion for beginners. It is not the same as the $=$ sign in mathematical statements. In mathematics, $a=b$ is an assertion or claim that the values of $a$ and $b$ are equal. This is completely different from the computer code a=b, which is not an assertion of anything. Instead, = is an instruction to the computer to perform an assignment, which is the action of copying the value of $b$ into the memory cell designated by $a$. Note that in mathematics, $a=4$ means the same as $4=a$, but the computer programming = symbol is not like this: a=4 means one thing, and 4=a means nothing at all because 4 does not designate a memory cell. For this reason many programming languages like to represent the assignment operation with an asymmetric symbol. Some use a := b or a ← b instead of a = b.

You suggested that one of the function's postconditions is “last = last + prev”. This doesn't make sense, because postconditions are supposed to be assertions, and as an assertion of equality, this means that the value of $last$ is equal to the value of $last + prev$. This can obviously only occur when $prev = 0$, so if this were really the postcondition you meant, you would just say “$prev = 0$” and leave it at that. Needless to say, this is not the condition you want.

I don't want to just dump the fibonacci answer on you, because it is a very instructive example and you deserve the chance to get the benefit from it. So I am going to do a different and simpler example that I hope will explain the idea. I will write a function which, given $k$, calculates $2^k$.

---

The function will look like this:

int pow2(int k) {
  int p = ???;     # this will hold the result
  ... ??? ...
  # precondition: p = 2^k
  return p;
}

The last thing the function does is to return the value of $p$, so for the function is to be correct, this return action has the precondition that $p$ must be equal to $2^k$. If this condition doesn't hold, the function is returning the wrong value!

How can we achieve this? We might have the idea of using a while loop:

int pow2(int k) {
  int p;     # this will hold the result
  while (???) {
    ???
  }
  # precondition: p = 2^k
  return p;
}

Our precondition for the return is now also a postcondition for the loop.
At this point we need to introduce a new element. (Otherwise the only possible while condition would be while (p ≠ 2^k), which is not helpful.) We might like to try to calculate $2^k$ iteratively, so we will introduce a loop index variable $i$ to count the number of iterations the loop has performed. Since we want to run the loop exactly $k$ times, we want $k=i$ as a postcondition for the loop. A while (C) loop always guarantees as a postcondition that that $C$ is false (this is the whole point of a while loop) which suggests that we should take the condition of the loop here to be $k≠i$:

int pow2(int k) {
  int p;     # this will hold the result
  int i;     # number of times the loop has run
  while (i≠k) {
    ???
  }
  # postcondition: i = k
  # precondition: p = 2^k
  return p;
}

Since we want $i$ to be the number of times the body of the loop has run, we can state a precondition for starting the while loop: $i=0$. And we can state a condition for the body of the while loop: it must increase $i$ by exactly 1. This motivates the following additions:

int pow2(int k) {
  int p;     # this will hold the result
  int i = 0; # number of times the loop has run
  while (i≠k) {
    i += 1; # invariant: the body of the loop has run exactly i times
    ???
  }
  # postcondition: i = k
  # precondition: p = 2^k
  return p;
}

Now we are going to tackle $p$, which is the real point of the program. At the end, we want to have $p=2^k$ and $i=k$, so if we can arrange that $p=2^i$ each time through the loop, then when the loop exits we will have $p=2^i = 2^k$ and we will win. Since $i$ is 0 before the loop starts, we must have $p=2^0 = 1$ at that point:

int pow2(int k) {
  int p = 1; # this will hold the result
  int i = 0; # number of times the loop has run
  while (i≠k) {
    i += 1; # invariant: the body of the loop has run exactly i times
    ???
  }
  # postcondition: i = k
  # precondition: p = 2^k
  return p;
}

Now we have $p=2^i$ before the loop and we want $p=2^i$ also after the loop. A while loop with body $B$ guarantees that if some loop invariant condition holds before the loop starts, and if it is preserved by $B$, then it will hold after the loop completes. The loop invariant condition we want here is $p=2^i$. We did arrange for this to be true before the loop starts. If we can arrange that the body of the loop maintains this invariant, then the semantics of while guarantees that we will still have $p=2^i$ at the end, and we win.

But right now the loop body does not preserve the invariant that $p=2^i$. It has i+=1. If we want $p=2^i$ to continue to hold, we must update the value of $p$ to match the change in $i$. Since we had $i$ changing to $i+1$, we need $p$ to change from $2^i$ to $2^{i+1}$:

# If p=2^i before this executes...
{
  i += 1;
  p *= 2;
}
# ... then still p = 2^i afterward

This is the correct body for the while loop, so let's put it in:

int pow2(int k) {
  int p = 1; # this will hold the result
  int i = 0; # number of times the loop has run
  # precondition: p = 2^i
  while (i≠k) {
    i += 1; # invariant: the body of the loop has run exactly i times
    p *= 2; # invariant: p = 2^i
  }
  # postcondition: p = 2^i
  # postcondition: i = k
  # precondition: p = 2^k
  return p;
}

This program works, and the proof is in the invariants and conditions: The body of the while loop preserves the invariant $p=2^i$. This condition holds before the loop begins executing, so it must still hold when the loop finishes. Also the semantics of the while loop guarantees that the condition $i≠k$ will be false when the loop finishes—so that means we will also have $i=k$. From $p=2^i$ and $i=k$ we can conclude that $p=2^k$. This is the precondition we wanted for the return statement. We win!

---

That was really long, but I hope it was helpful.

I have a couple of suggestions for how you should proceed from here.

Start with a program that actually works, and try to analyze it in terms of invariants and pre/postconditions. If you don't know how to write a working fibonacci number function, start instead with something you do know how to write.

Or start with a problem that you already know how to solve, and try to understand what the conditions and invariants are, and then use that to synthesize the program code.

But don't try to do both things at the same time.

Hint: A fibonacci function always needs three variables. Two is not enough.

Sorry this was so long.

---

Addendum: I thought of a good exercise for you to do that will be easier than the fibonacci one. Redo the pow2 function I wrote above so that it counts down to 0 instead of up from 0:

int pow2(int k) {
  int p = 1; # this will hold the result
  int i = k; # number of times the loop has left to run
  # precondition: p * 2^i = 2^k
  while (???) {
     ???       # Invariant: p * 2^i = 2^k
  }
  # postcondition: p * 2^i = 2^k
  #    ???
  # precondition: p = 2^k
  return p;
}

The loop invariant is now $p·2^i = 2^k$. This is correctly established by the initialization $p=1; i=k$.

1. What must you put into the body of the while loop to maintain this invariant?
2. What additional condition is required after the while loop completes in order for us to conclude that $p=2^k$ as we desire?
3. What can we put into the condition of the while loop to guarantee that this additional condition will hold when the while loop finishes running?