[Algorytmy] Poprawność semantyczna - Fibonacci

[Modery]

Witam. Zrobiłam częściowo zadanie o poprawności semantycznej n-tego ciągu Fibonacciego. Wygląda ono następująco:

algorytm:

Kod: Zaznacz cały

fibonacci (int n)
{  int fibb=0;
    int i =2;
    int w0=0;
    int w1=1;
    int n;
    if ( n==0 )
    { fibb = 1;}
    if ( n==1 )
    { fibb = 1;}
    if ( n>1 )
    { while ( i<n )
       { w1 = w0 + w1;
          w0 = w1 - w0;
          i++;
         }
       fibb=w1;
       }
    }

\(\displaystyle{ { \alpha : n \ge 0 }\\
{ \beta : fibb: fibonacci _{(n)} \\
{ \gamma : ................................ ;}\)brakuje mi warunku gamma dla pętli while i jego dowódu

1) Dla n=0,1 poprawność wynika z własności ciągu fibonacciego, bo\(\displaystyle{ F_{0} = F_{1} = 1}\)
2) Dla n>1 przeprowadzimy indukcję względem \(\displaystyle{ F_{(k)}}\)
k=n-1

Założenie:
\(\displaystyle{ F_{(k)} = F_{(k-1)} + F_{(k-2)} \wedge 1<k<n\\
F_{(0)} = F_{(1)} = 1}\)

Teza:
Dla każdego n, algorytm jest prawdziwy

Dowód:

\(\displaystyle{ F _{(n)} = F_{(n-1)} + F_{(n-2)}\\
F _{(n-1)} = F_{(n-2)} + F_{(n-3)}}\)

\(\displaystyle{ F _{(n)}}\) jest wywołane rekurencyjnie dla n-1, n-2, n-3, ... więc jesli zgodnie z założeniem indukcyjnym \(\displaystyle{ F _{(n-1)}}\) jest prawdziwe, to \(\displaystyle{ F _{(n)}}\) również.



Jak ma wyglądać warunek gamma i jego dowód ? Z góry dziekuje