SW wykład 10 - Slajd12

<<powrót do strony wykładu

Poprawność programów i weryfikacja Poprawność programów Dowodzenie poprawności Wyspecyfikowany program Logika Hoare'a Definicje formalne Definicje formalne, c.d. Semantyka logiki Hoare'a Reguły wnioskowania Przykład dowodu Przykład dowodu, c.d. Niezmiennik pętli Przykład dowodu, c.d. W pełni wyspecyfikowany program Teorie pierwszego rzędu

Pokażemy teraz, że wprowadzony w poprzednim kroku dowodu warunek końcowy dla złożenia dwóch przypisań rozpoczynających nasz program jest niezmiennikiem następującej po tym złożeniu pętli.

Po pierwsze, pokazujemy poprawność pierwszego z przypisań w ciele pętli względem warunku wstępnego, który jest rozważanym niezmiennikiem wzmocnionym o warunek wejścia do ciała pętli, i względem odpowiedniego warunku końcowego (który znów można wyznaczyć jako najmocniejszy warunek końcowy, zapewniający częściową poprawność tego przypisania względem zadanego warunku wstępnego). To stwierdzenie o częściowej poprawności znów wynika wprost z reguły dla instrukcji przypisania.

Po drugie, pokazujemy poprawność drugiego z przypisań w ciele pętli względem warunku wstępnego, którym jest warunek końcowy dla poprzedniego przypisania, i warunku końcowego, którym jest rozważany niezmiennik pętli. To stwierdzenie również wynika wprost z reguły dla instrukcji przypisania (i z przekształcenia otrzymanej przez odpowiednie podstawienie formuły, oczywistego wobec znanego wzoru na kwadrat sumy liczb).

Stosując teraz regułę dla instrukcji złożonej, otrzymujemy stwierdzenie o częściowej poprawności ciała pętli względem warunku wstępnego, którym jest rozważany niezmiennik wzmocniony o warunek wejścia do pętli, i warunku końcowego, którym jest ów niezmiennik pętli.

Reguła dla instrukcji pętli prowadzi teraz wprost do stwierdzenia częściowej poprawności pętli względem warunku wstępnego, którym jest podany niezmiennik tej pętli, i warunku końcowego, którym jest niezmiennik pętli wzmocniony o negację warunku wejścia do pętli.