unction fib$($n: nat$)$: nat

$2\{$

$3$ if n$==0$ then $0$

$4$ else if n$==1$ then $1$

$5$ else fib$($n $-1)+$fib$($n $-2)$

$6\}$

$7$

$8$ method ComputeFib$1($n:nat$)$ returns $($a:nat$)$

$9$ ensures a$==$ fib$($n$)$

$10\{$

$11$ if n$==0\{$ return $0$;$\}$

$12$ var i: int :$=1$;

$13$ a :$=1$;

$14$ var b:$=1$;

$15$ var c :$=2$;

$16$

$17$ while i $<$ n

$18//$ TODO: fill in invariants here

$19\{$

$20$ a:$=$b;

$21$ b:$=$c;

$22$ c:$=$a$+$b;

$23$ i :$=$ i $+1$;

$24\}$

$25$ return a;

$26\}$

$27$

$28$ method ComputeFib$2($n:nat$)$ returns $($b:nat$)$

$29$ ensures b$==$ fib$($n$)$

$30\{$

$31$ var i: int :$=0$;

$32$ var a :$=1$;

$33$ b :$=0$;

$34$

$35$ while i $<$ n

$36//$ TODO: fill in invariants here

$37\{$

$38$ a$,$ b :$=$ b$,$ a $+$ b;

$39$ i :$=$ i $+1$;

$40\}$

$41$ return b;

$42\}$

$1$