Io-1-lab

Ćwiczenia – Wprowadzenie do przedmiotu

Wprowadzenie

Podczas wykładu „Wprowadzenie do przedmiotu”, była mowa o wielu aspektach Inżynierii oprogramowania. Większość przedstawionych zagadnień będzie przedstawiona szerzej przy okazji kolejnych wykładów (także podczas kursu „Zaawansowana inżynieria oprogramowania”). W ramach tych ćwiczeń chcielibyśmy zwrócić uwagę na jedno zagadnienie, które nie będzie już dalej omawiane – dowodzeniu poprawności programów.

---

Ćwiczenie 1 – Dowodzenie programu obliczającego n-ty wyraz ciągu Fibonacciego.

W ramach wykładu „Wprowadzenie do przedmiotu”, przedstawiony został przykład dowodzenia programu z wykorzystaniem niezmienników (ang. Invariants), na przykładzie programu obliczającego wartość wyrażenia n!.

Zadanie polega na udowodnieniu w analogiczny sposób programu obliczającego n-ty wyraz ciągu Fibonacciego.

Ciąg Fibonacciego jest zdefiniowany w następujący sposób:

Parser nie mógł rozpoznać (nieznana funkcja „\begin{cases}”): {\displaystyle Fib(n) = \begin{cases} 0, \mbox{dla n=0,} \\ 1, \mbox{dla n=1,} \\ F(n-1) + F(n-2) \mbox{, dla n > 1.} \end{cases} }

Badany program w języku C ma następującą postać:

int Fib(int n){
 int k, f0, f1, f2;
 k = 0; f0 = 1; f1 = 1;
 while (k != n){
   k = k + 1;
   f2 =  f0 + f1;
   f0 = f1;
   f1 = f2;
 };
 return f0;
};

Podpowiedź

Staraj się postępować według następującego schematu:

1. Określ warunek wstępny (ang. Precondition).
2. Określ warunek końcowy (ang. Postcondition).
3. Znajdź odpowiedni niezmiennik $\alpha$ (ang. Invariant).
4. Udowodnij, że $\alpha$ jest niezmiennikiem.
5. Udowodnij prawdziwość warunku końcowego.

Rozwiązanie

Będziemy postępować zgodnie z przedstawionym jako podpowiedź schematem postępowania.

1. Określ warunek wstępny (ang. Precondition).

W przypadku ciągu Fibonacciego warunek wstępny może wyglądać następująco:

• Precondition: n >= 0

int Fib(int n){  /* PRE: n >= 0 */
 int k, f0, f1, f2;
 k = 0; f0 = 1; f1 = 1;
 while (k != n){
   k = k + 1; 	
   f2 =  f0 + f1;  
   f0 = f1;		
   f1 = f2;		
 };
 return f0;
};

2. Określ warunek końcowy (ang. Postcondition).

• Postcondition: f0 == Fib(n)

int Fib(int n){  /* PRE: n >= 0 */
 int k, f0, f1, f2;
 k = 0; f0 = 1; f1 = 1;
 while (k != n){
   k = k + 1; 	
   f2 =  f0 + f1;  
   f0 = f1;		
   f1 = f2;		
 };
 return f0; /* POST: f0 = Fib(n) */
};

3. Znajdź odpowiedni niezmiennik $\alpha$ (ang. Invariant).

Niezmiennik można by zdefiniować jako:

• f0 == Fib(k) $\wedge$ f1 == Fib(k + 1)

int Fib(int n){  /* PRE: n >= 0 */
 int k, f0, f1, f2;
 k = 0; f0 = 1; f1 = 1;
 /* INV: f0 == Fib(k) and f1 == Fib(k + 1) */
 while (k != n){ 
   k = k + 1; 	
   f2 =  f0 + f1;  
   f0 = f1;		
   f1 = f2;		
 };
 return f0; /* POST: f0 = Fib(n) */
};

4. Udowodnij, że $\alpha$ jest niezmiennikiem.

int Fib(int n){ /* PRE: n >= 0 */
 int k, f0, f1, f2;
 k = 0; f0 = 1; f1 = 1;
 /* INV: f0 == Fib(k) and f1 == Fib(k + 1) */
 while (k != n){
   k = k + 1;		<-  f0 == Fib(k) $\wedge$ f1 == Fib(k + 1) (k = k – 1) 
   f2 =  f0 + f1;	<-- f2 == Fib(k - 1) + Fib(k) == Fib(k + 1)  
   f0 = f1;		<-- f0 == Fib(k)  (f1 == Fib(k + 1) == Fib(k))
   f1 = f2;		<-- f1 == Fib(k + 1) (patrz f2)
 };
 return f0; /* POST: f0 = Fib(n) */
};

Jak można zaobserwować zaproponowany przez nas niezmiennik w postaci:

• f0 == Fib(k) $\wedge$ f1 == Fib(k + 1),

faktycznie pozostaje prawdziwy w ramach pętli while, zatem jest niezmiennikiem.

5. Udowodnij prawdziwość warunku końcowego.

W punkcie 4. udało się udowodnić, że wyrażenie

• f0 == Fib(k) $\wedge$ f1 == Fib(k + 1),

jest inwariantem. Zatem po wykonaniu pętli while zmienna f0 będzie miała wartość:

• f0 == Fib(k).

Jeśli została zakończona pętla while z warunkiem:

• k != n,

Oznacza to, że prawdziwe jest zaprzeczenie tego warunku, czyli na tym etapie wykonywania programu prawdziwe jest stwierdzenie:

• n == k,

Zatem warunek końcowy

• Postcondition: f0 == Fib(n)

jest spełniony, ponieważ:

• f0 == Fib(k), gdzie k == n, zatem f0 == Fib(n)

Tym samym udowodniliśmy poprawność programu.

---

Ćwiczenie 2 – Schematy programów, których poprawność udowodnić można wykorzystując podobnie jak w przypadku programów obliczających n! i n-ty wyraz ciągu Fibonacciego.

Analizując przykłady dowodów na poprawność programu obliczającego wyrażenie n! (przedstawionego na wykładzie) oraz programu obliczającego n-ty wyraz ciągu Fibonacciego, możemy zauważyć, że przeprowadzane dowody poprawności są dość zbliżone.

Można zatem spróbować stworzyć pewne schematy (wzorce) programów, dla których jesteśmy w stanie udowodnić pewne własności, które mogą okazać się bardzo pomocne podczas dowodzenia.

Przyjrzyjmy się poniższemu schematowi (SP1):

k = p; 
Instrukcja1;     /* prawdziwy Invariant – nie zmienia ani k ani n*/
/* INV: $\alpha$ */
while ( k != n){
   k = k + 1;
   Instrukcja2; /* prawdziwy Invariant – nie zmienia ani k ani n*/
   /* INV: $\alpha$ */    
};

We wzorcu występuje niezmiennik $\alpha$:

• ${\mathrm{\forall }}_{n>=p}\alpha$

Aby, wykazać poprawność programu wystarczy udowodnić, że $\alpha$ jest niezmiennikiem.

Tego typu wzorce mogą ułatwić dowodzenie poprawności dłuższych programów. Jeśli potrafimy udowodnić pewne właściwości wzorca, nie musimy dowodzić ich dla konkretnego przykładu tego wzorca (w postaci konkretnego programu).

Przeanalizuj jeszcze raz program na obliczanie n-tego wyrazu ciągu Fibonacciego pod kątem przedstawionego schematu i spróbuj dopasować wzorzec SP1 do tego programu.

Podpowiedź

a) dokonaj modyfikacji programu z ćwiczenia 1 jeśli to konieczne,

b) określ niezmiennik,

c) znając właściwości wynikające z SP1, spróbuj dowieść poprawności programu (wykaż, że zdefiniowane $\alpha$, jest niezmiennikiem)

Korzystając ze schematu napisz program obliczający wartość wyrażenia $a^n$.

Rozwiązanie

Program obliczający wartość wyrażenia $a^n$, który odpowiada schematowi SP1:

int aton(int a, int n){ /* PRE: n >= 0 */
 int res = 1, k = 0;
 /* INV: res = a^k */
 while (k != n){
   k = k + 1;
   res = res * a;
 };
 return res; /* POST: res == a^n */
};

Jak można zauważyć program aton, odpowiada schematowi SP1. Aby dowieść jego poprawności musimy udowodnić, że wybrany przez nas niezmiennik:

• res == $a^n$

rzeczywiście jest niezmiennikiem.

int aton(int a, int n){ /* PRE: n >= 0 */
 int res = 1, k = 0;
 /* INV: res = a^k */ 	<- res == a^0 == 1
 while (k != n){
   k = k + 1; 		<- res = a^k, gdzie k = k - 1
   res = res * a; 	<- res = a^k * a = a^k, gdzie k = k - 1
 };
 return res; /* POST: res == a^n */
};

Zatem res == $a^n$ jest niezmiennikiem. Zatem możemy stwierdzić, że program odpowiada wzorcowi SP1 i posiada jego właściwości. Wiemy, że wzorzec SP1 jest poprawny, zatem i program mu odpowiadający jest poprawny.

---

Ćwiczenie 3 – Opracowanie programu sprawdzającego czy dana liczba jest pierwsza w oparciu o schemat.

W zadaniu 2 udało się opracować schemat programu, który nazwaliśmy SP1. Jeśli dany program można uogólnić do postaci schematu SP1, możemy w łatwy sposób udowodnić jego poprawność.

Możemy zatem stwierdzić, że:

$\frac{SP1}{\alpha }$

Zaproponujmy schemat (SP2) dla innego typu problemów, w postaci:

Answer = False;
k = a;
while ( k < b){
   if ($\beta$(k)){
       Answer = True;
   }
   k = k + 1;
};

Możemy stwierdzić, że prawdziwa jest implikacja:

$\frac{SP2}{Answer\equiv {\mathrm{\exists }}_{a<=k<b}\beta (k)}$

Zaproponuj program sprawdzający czy dana liczba jest pierwsza, który da się uogólnić do postaci schematu SP2.

Podpowiedź

W pierwszej kolejności można stworzyć program sprawdzający czy dana liczba jest podzielna przez liczbę z przedziału <a,b). Wówczas warunek $\beta$ miałby postać:

• n % k == 0, dla (a <= k < b)

Rozwiązanie

Można uszczegółowić bardziej przedział <a, b). Dana liczba jest liczbą pierwszą jeśli dzieli się tylko przez siebie samą i liczbę 1. Zatem nie może być podzielna przez liczby z przedziału <2, n), gdzie n to badana liczba. Wykorzystując pomysł podany w podpowiedzi możemy zaproponować program sprawdzający, czy dana liczba jest podzielna przez liczbę z przedziału <a, b), a dokładniej z przedziału <2, n).

Można zatem określić, kiedy liczba n, jest podzielna przez liczbę z przedziału <2, n):

• MaPodzielnik(n) $⟺{\mathrm{\exists }}_{2<=k<n}$ n % k == 0

Program obliczający MaPodzielnik(n), może mieć postać:

bool MaPodzielnik(int n){
 bool Answer = False;
 int k = 2;
 while ( k < n){
   if (n % k = 0){
       Answer = True;
   }
   k = k + 1;
 }
 return Answer; 
};

Program ten jest instancją schematu SP2, zatem możemy stwierdzić, że jest on poprawny. Aby stworzyć program badający, czy liczba n jest liczbą pierwsza posłużymy się zależnością:

• Pierwsza(n) $\equiv \mathrm{\neg }$MaPodzielnik(n)

bool Pierwsza(int n){
 bool Answer = False;
 int k = 2;
 while ( k < n){
   if (n % k = 0){
       Answer = True;
   }
   k = k + 1;
 }
 Answer; 	<- tutaj kończył się program MaPodzielnik(n) 
 return !Answer; 
};

Wiemy, że program MaPodzielnik(n) jest poprawny, zatem możemy stwierdzić, że program Pierwsza(n) do linijki zaznaczonej w kodzie także jest poprawny. Jednak oba programy różnią się warunkiem końcowym. Wiemy, że Pierwsza(n) $\equiv \mathrm{\neg }$MaPodzielnik(n), zatem aby spełnić warunek końcowy należy wprowadzić negację zmiennej Answer (zmienna typu bool – wartości 0,1).

Pytania do dyskusji

1. W jakich typach programów dowodzenie poprawności ma szczególny sens i może być opłacalne?
2. Jakie są ograniczenia przemysłowe stosowania metod dowodzenia poprawności programów?