SW wykład 13 - Slajd13
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ę
Musimy zatem teraz określić warunek wejścia do ciała pętli, instrukcję ciała pętli, jej niezmiennik, oraz zbiór z relacją dobrze ufundowaną i wyrażenie o wartościach w tym zbiorze tak, aby zostały spełnione cztery wymienione na slajdzie wymagania. Zauważmy, że wymagania te są wystarczające do pokazania całkowitej poprawności pętli względem podanych warunków wstępnego i końcowego.
