Io-1-lab

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

Ć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ź

Rozwiązanie


Ć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:  */
while ( k != n){
   k = k + 1;
   Instrukcja2; /* prawdziwy Invariant – nie zmienia ani k ani n*/
   /* INV:  */    
};

We wzorcu występuje niezmiennik :

Aby, wykazać poprawność programu wystarczy udowodnić, że 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ź

Rozwiązanie


Ć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:

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

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

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

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

Podpowiedź

Rozwiązanie

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?