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) Parser nie mógł rozpoznać (błąd składni): {\displaystyle \equiv \not</mant>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) <math>\equiv \not</mant>MaPodzielnik(n), zatem aby spełnić warunek końcowy należy wprowadzić negację zmiennej Answer (zmienna typu bool – wartości 0,1). </div> </div> ---- ===Ćwiczenie 4 – Technika wizualizacji i afirmacji=== 4.1. Poniżej opisano 5 sytuacji, w każdej z nich została sformułowana afirmacja. Przy użyciu [[media:io-2-lab-z4_1.rtf|formularza odpowiedzi]] proszę zweryfikować, czy afirmacje te mają 5 podstawowych cech omówionych na wykładzie. Jeśli nie proszę je odpowiednio przeredagować. #Marek studiuje na IV roku informatyki. Jego praca inżynierska została wyróżniona. Na jej podstawie, pod okiem swojego promotora, napisał swój pierwszy artykuł i został zaproszony do jego prezentacji na konferencji naukowej. Jako, że wcześniej Marek nie miał okazji występować publicznie postanowił zastosować technikę wizualizacji i afirmacji, które poznał na studiach. Wyobrażając sobie salę konferencyjną, licznych słuchaczy oraz siebie, prezentującego przed audytorium referat Marek używał następującej afirmacji: „Mój referat na pewno wypadnie dobrze, w końcu długo się przygotowywałem do wystąpienia.” #Janek, student II roku informatyki, miał problemy ze zmobilizowaniem się do nauki na pierwszym roku, czego efektem były 4 egzaminy poprawkowe w sesji letniej. Aby uniknąć takiej sytuacji w tym roku postanowił jeszcze w trakcie wakacji wykorzystać technikę wizualizacji i afirmacji. Na początek przypominał sobie, jak to było na pierwszym roku, jak po zajęciach zamiast pracować nad projektami i zadaniami siadał do gry komputerowej, jakie miał wtedy myśli, emocje. W drugim kroku wyobrażał sobie, jak będzie na drugim roku, jak po powrocie z zajęć zamiast od razu siadać do gry będzie zabierał się do nauki, tak na 2-3 godziny. Jaki będzie zadowolony, że odrobił wszystkie zadania i z czystym sumieniem, może usiąść do zasłużonego relaksu – gry komputerowej. Janek sformułował następującą afirmację: „Byłoby miło, gdybym potrafił znaleźć czas i na naukę i rozrywkę.” #Marta trenuje pływanie w Akademickim Związku Sportowym (AZS). Jej najmocniejszą konkurencją jest 50m stylem klasycznym. Jest uzdolnionym sportowcem, jednak podczas zawodów zawsze bardzo się denerwuje, czego skutkiem jest często, zbyt późne (w stosunku do innych zawodniczek) odbicie się od słupka startowego i utracenie już na początku dystansu do najlepszej czołówki. Trener zaproponował Marcie zastosowanie techniki wizualizacji i afirmacji. Marta, w wolnych chwilach wyobraża sobie, że stoi na słupku tuż przed startem. Przypomina sobie jakie emocje towarzyszą jej zazwyczaj podczas zawodów pływackich. Jej afirmacja polega na wyobrażeniu sobie, jak w tej sytuacji się rozluźnia i koncentruje na dobrym starcie. Można ją wyrazić następującym zdaniem: „Potrafię rozluźnić się tuż przed startem i skoncentrować się na dobrym rozpoczęciu wyścigu.” #Pan Andrzej, właściciel firmy Super-soft, planuje wdrożyć w firmie innowacyjne narzędzie ułatwiające zbieranie wymagań od klientów i ich specyfikację. Zdaje sobie sprawę z tego, że podstawą efektywnego wdrożenia jest pozytywne nastawienie do zmiany wszystkich pracowników firmy, którzy z natury sceptycznie podchodzą do rozwiązań zaburzających ich dotychczasowy tryb pracy. Dotychczas przekonywanie do zmian pracowników sprawiało mu sporo trudności. Dlatego tym razem przed przystąpieniem do działań Pan Andrzej postanowił przeprowadzić wizualizację i afirmację. Wyobraził sobie jak organizuje spotkanie w firmie i przedstawia wyniki ekspertyzy oraz propozycję zmian w zakresie zbierania wymagań, jak rozwija się dyskusja, pracownicy wyrażają swoje obawy i uwagi, wysłuchują kontrargumentów. To, jak czują się docenieni, że szef informuje ich o sytuacji firmy i konsultuje z nimi kwestie zmian. Pan Andrzej sformułował następującą afirmację: „To świetnie, że w firmie wszyscy pracownicy są dobrze poinformowani i potrafią konstruktywnie dyskutować nad propozycją zmian.” #Tomek właśnie rozpoczął swoją pierwszą pracę w firmie Super-soft. Już po tygodniu dostał pierwsze, bardzo samodzielne zadanie, dotyczące przebudowy strony internetowej. Wie, że potrafi je wykonać, ponieważ podczas studiów dorabiał sobie wykonując różne strony. Denerwuje się jednak trochę, bo zależy mu, żeby wypaść jak najlepiej przed szefem. Postanowił dodać sobie otuchy przy użyciu afirmacji: „Bardzo się cieszę, że dostałem samodzielne zadanie, które potrafię bardzo dobrze wykonać i dzięki któremu zdobędę uznanie szefa” <div class="mw-collapsible mw-made=collapsible mw-collapsed"> <span style="font-variant:small-caps">Rozwiązanie </span> <div class="mw-collapsible-content" style="display:none"> Plik z rozwiązaniem ([[media:io-2-lab-z4_1-ans.rtf|rtf]]) </div> </div> 4.2. Proszę napisać 3 afirmacje związane z wybranymi w ćwiczeniu 3.1 praktykami zarządzania czasem ([[media:io-2-lab-z4_2.rtf|formularz]]). <div class="mw-collapsible mw-made=collapsible mw-collapsed"> <span style="font-variant:small-caps">Rozwiązanie </span> <div class="mw-collapsible-content" style="display:none"> Plik z rozwiązaniem ([[media:io-2-lab-z4_2-ans.rtf|rtf]]) </div> </div> ==Pytania do dyskusji== #Jak mogłoby wyglądać stosowanie zasady „ostrz piłę” w firmie informatycznej? #W jaki sposób zasada win-win może funkcjonować w relacjach kierownik projektu – programista?}