caps_lock

Untitled

Mar 23rd, 2015
271
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. function fib(n: nat): nat
  2. {
  3.    if n == 0 then 0 else
  4.    if n == 1 then 1 else
  5.                   fib(n - 1) + fib(n - 2)
  6. }
  7.  
  8. method fibo(n: nat) returns (b: nat)
  9.    ensures b == fib(n);
  10. {
  11.    var i: int := 0;
  12.        b := 0;
  13.    var c := 1;
  14.    while (i < n)
  15.       invariant 0 <= i <= n;
  16.       invariant b == fib(i);
  17.       invariant c == fib(i + 1);
  18.    {
  19.       b, c := c, b + c;
  20.       i := i + 1;
  21.    }
  22. }
RAW Paste Data