SW wykład 13 - Slajd9
Zadanie programistyczne Pierwsze podejście Przykład Weryfikacja Przykład Możliwe przyczyny porażki Poprawiony program Przykład dowodu Drugie podejście Wyprowadzanie programu Wyprowadzanie programu, c.d. Wyprowadzanie programu, c.d. Wyprowadzanie programu, c.d. Wyprowadzanie programu, c.d. Wyprowadzanie programu, c.d. Własność stopu Własność stopu, c.d. Poprawność przez konstrukcję
Przedstawimy teraz alternatywne podejście, gdzie program konstruujemy krok po kroku, systematycznie podejmując decyzje programistyczne i budując uzasadnienie ich poprawności. Zakończenie budowania programu w ten sposób nie będzie już wymagało przeprowadzenie dowodu poprawności wyniku: dowód ten powstanie wraz z programem, w czasie jego systematycznej konstrukcji.
Jak poprzednio, posłużymy sie tym samym prostym przykładem: naszym punktem wyjścia jest specyfikacja programu liczącego całkowity pierwiastek kwadratowy liczby naturalnej --- co zadajemy, jak dotychczas, w postaci warunków wstępnego i końcowego, względem których zbudowany program ma być całkowicie poprawny. Przynajmniej niektóre z omawianych kroków konstrukcji będą dość trywialne, a ich analiza może wydać się Państwu nadmiernie szczegółowa, czy wręcz zbędna. Pamiętajmy jednak, że to tylko z konieczności bardzo uproszczony przykład, pełniący rolę ilustracji rzeczywistych, często nietrywialnych decyzji programistycznych, które są niezbędne w konstruowaniu bardziej złożonych programów.
Aby powiązać wartości zmiennych w stanie końcowym z wartościami w stanie początkowym, wymagać też będziemy, by zmienna niosąca liczbę całkowitą, której pierwiastek chcemy policzyć, nie była zmieniana w konstruowanym programie (patrz wykład 12, slajd 17). Ponieważ jest on łatwy do zapewnienia i sprawdzenia, warunkiem tym nie będziemy się dalej zajmować w naszej analizie.
