function fib(n: nat): nat
{
   if n == 0 then 0 else
   if n == 1 then 1 else
                  fib(n - 1) + fib(n - 2)
}

method fibo(n: nat) returns (b: nat)
   ensures b == fib(n);
{
   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;
   }
}