SW wykład 13 - Slajd14

[ <<powrót do strony wykładu

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 $n-rt$ 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ć.