program Fibonacci; {versione fatta in classe e in laboratorio}

{pre: n >= 0, intero} 
{post: fib = f(n), dove f e` la funzione:
f(0) = 0  (caso base);
f(1) = 1  (caso base);
f(n+2) = f(n+1) + f(n) (caso induttivo).}

var a,b,c,i,n,fib:integer;

begin
 a:=0; b:=1; c:=1;    {a=f(0);b=f(1);c=f(1)}
 readln(n);
 if n=0 then fib:=0   {fib=0=fib(0)}
  else if n=1 then fib:=1   {fib=1=fib(1)}
   else
    begin
     for i:=1 to n-1 do 
      begin
       c:=a+b;        
       a:=b;          
       b:=c;          {INVARIANTE di CICLO: a=f(i-1);c=b=f(i)}
     end;
    fib:=c;           {i=n, dunque fib=c=f(i)=f(n)}
   end;
 writeln(fib);
 readln;
end.

NOTA 1: il caso induttivo si puo` scrivere anche come:
	f(n) = f(n-1)+f(n-2), se n diverso da 0, 1.

NOTA 2: l'inizializzazione c:=1 serve solo a rendere l'invariante vero
        anche per i = 1.  L'algoritmo funziona anche con l'inizializzazione
	c:=0. Confrontate questa versione del programma con la soluzione 
	a vostra disposizione qui sotto.