SW wykład 13 - Slajd14
Systematyczne konstruowanie programów Inżynieria wymagań Walidacja specyfikacji Strukturalne języki specyfikowania Zadanie programisty Uszczegóławianie Uszczegóławianie, c.d. Dekompozycja Wyzwanie
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ć.
