SW wykład 13 - Slajd14
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ę
Jak zwykle, kluczowy jest tu niezmiennik pętli: przedstawienie właściwego niezmiennika, który umożliwi potem konstrukcję pozostałych składowych instrukcji i dowodu jej wymaga poprawności, wymaga inwencji programisty.
W tym przypadku, proponujemy niezmiennik jak w ramce na górze slajdu.
Natychmiast zapewnia nam to spełnienie pierwszego z wymagań dotyczących konstrukcji pętli: niezmiennik ten jest konsekwencją warunku wstępnego.
Wybieramy też warunek wejścia do ciała pętli, jak w drugiej ramce na slajdzie. Wówczas też łatwo pokazać, że zachodzi drugie z wymagań dotyczących instrukcji pętli: niezmiennik wzmocniony o negację warunku wejścia do ciała pętli implikuje warunek końcowy.
Dalej, określamy zbiór z relacją dobrze ufundowaną (zbiór liczb naturalnych ze zwykłą "ostrą" nierównością). Zauważmy, że dla stanów spełniających niezmiennik pętli, wartość wybranego tu wyrażenia rzeczywiście jest liczbą naturalną.
W końcu, dwa ostatnie wymagania z poprzedniego slajdu tworzą specyfikację dla instrukcji ciała pętli, którą mamy jeszcze zbudować.
