SW wykład 10 - Slajd13
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
Warunek końcowy w stwierdzeniu o częściowej poprawności instrukcji pętli na poprzednim slajdzie możemy teraz nieco osłabić, eliminując z niego informacje o wartości pomocniczej zmiennej --- otrzymujemy wówczas, na mocy reguły wynikania, pierwsze ze stwierdzeń częściowej poprawności na tym slajdzie.
Korzystając teraz z reguły dla instrukcji złożonej, z tego właśnie stwierdzenia o częściowej poprawności instrukcji pętli i z wyprowadzonego wcześniej stwierdzenia o częściowej poprawności poprzedzającego tę pętlę w naszym programie złożenia dwóch instrukcji przypisania wyprowadzamy stwierdzenie o częściowej poprawności programu względem podanych warunków wstępnego i końcowego dokładnie takiej postaci, jaką chcieliśmy od początku przykładu uzyskać.
Warto zwrócić uwagę, że powyższy dowód częściowej poprawności rozważanego programu konstruowaliśmy niejako "w przód", poczynając od warunku wstępnego i budując kolejne warunki występujące w dowodzie jako najmocniejsze warunki końcowe kolejnych instrukcji, zapewniające ich częściową poprawność względem wcześniej uzyskanych warunków wstępnych. Oczywiście, wyjątkiem było tu zaproponowanie odpowiedniego niezmiennika pętli, który na ogół nie może powstać w tak "mechaniczny" sposób. Alternatywną możliwością jest budowanie dowodu "w tył", poczynając od warunku końcowego. Znów, niezmienniki pętli muszą tu być efektem inwencji programisty (czy osoby prowadzącej dowód), ale w pozostałych przypadkach kolejne warunki występujące w dowodzie można budować jako najsłabsze warunki wstępne dla kolejnych ("od tyłu") instrukcji, które zapewniają ich częściową poprawność względem wcześniej uzyskanych warunków końcowych. Często okazuje się, że właśnie ta druga strategia, strategia budowania dowodu częściowej poprawności "od końca", okazuje się technicznie nieco prostsza: widać to choćby w regule przypisania, gdzie wprost w regule dany jest (jako wynik podstawienia w warunku końcowym) najsłabszy warunek wstępny, dla którego dana instrukcja przypisania jest częściowo poprawna względem zadanego warunku końcowego.
