Exercise 9 from Microsoft's Dafny on Rise4Fun.com

dafny-exercise9

/*
 * The ComputeFib method above is more complicated than necessary. Write
 * a simpler program by not introducing a as the Fibonacci number that
 * precedes b, but instead introducing a variable c that succeeds b.
 * Verify your program is correct according to the mathematical definition
 * of Fibonacci.
 */
function fib(n: nat): nat
{
   if n == 0 then 0 else
   if n == 1 then 1 else
                  fib(n - 1) + fib(n - 2)
}

method ComputeFib(n: nat) returns (b: nat)
   ensures b == fib(n); // Do not change this postcondition
{
   var i: int := 0;
       b := 0;
   var c := 1;
   while (i < n)
      invariant 0 <= i <= n;
      invariant b == fib(i);
      invariant c == fib(i + 1);
   {
      b, c := c, b + c;
      i := i + 1;
   }
}