SW wykład 10 - Slajd14

<<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

Warto zauważyć, że w zasadzie konstrukcja dowodu w powyższym przykładzie przebiega zgodnie ze strukturą instrukcji, o której częściowej poprawności mówi dowodzone stwierdzenie (wyjątkiem jest tu "wtrącane" stosowanie reguły wynikania). Istotę dowodu stanowi zatem podanie odpowiednich warunków wykorzystywanych jako warunki wstępne i końcowe dla stwierdzeń o częściowej poprawności poszczególnych instrukcji występujących w naszym programie. Na powyższym slajdzie proponujemy sposób zapisu tych wszystkich warunków, przez odpowiednie ich wplecenie w składnię programu, którego częściową poprawność pokazujemy. Z tak podanych asercji, mówiących o własnościach stanów, które mogą się pojawić w obliczeniach w danych punktach programu, można łatwo zrekonstruować dowód, posługując się strukturą programu i formalnie odwołując się do podanych reguł dowodzenia.

Wygodnie nam będzie w przyszłości w taki właśnie skrócony sposób zapisywać argumenty pokazujące częściową poprawność programów. Warto przy tym zwrócić uwagę, że poza pierwszym warunkiem wstępnym i ostatnim warunkiem końcowym dla całego programu, najistotniejsze jest tu podanie niezmienników pętli. Jeśli zostały one określone prawidłowo, to pozostałe asercje można uzyskać "mechanicznie", jak wskazywaliśmy powyżej.

Uwaga jednak: nie wystarcza tu wymaganie, by asercje podane dla poszczególnych punktów programu były spełnione we wszystkich stanach, które w danym punkcie mogą się pojawić w trakcie obliczeń programu. Muszą one być wystarczające dla pokazania, że zachodzą odpowiednie stwierdzenia o częściowej poprawności, wymagane dla stosowania reguł dowodzenia częściowej poprawności. Podawane asercje muszą więc ze sobą współgrać (i współgrać z pierwszym warunkiem wstępnym i ostatnim warunkiem końcowym dla całego programu).

Tak wpisane w program asercje stanowią wspaniałą dokumentację programu: nie tylko mówią, jakich własności należy oczekiwać w danym punkcie programu, ale podają te własności w sposób spójny i pełny, gwarantujący możliwość dowodu poprawności programu względem danych warunków wstępnego i końcowego. Co więcej, podają pełne wymagania lokalne wobec różnych fragmentów programu. Ważne jest przy tym, że bez naruszenia poprawności całego programu, każdą jego instrukcję składową można zastąpić inną, o ile tylko i ta nowa instrukcja jest częściowo poprawna względem podanych w jej bezpośrednim sąsiedztwie asercji.