SW wykład 12 - Slajd8

<<powrót do strony wykładu

Zadanie programistyczne Przykład Problemy z logiką Hoare'a Poprawność całkowita Poprawność całkowita, c.d. Poprawność całkowita, c.d. Reguła dla pętli Poprawność systemu dowodzenia dla Tiny Pełność systemu dowodzenia dla Tiny Przykład Uogólnienie Poprawność i pełność Relacje dobrze ufundowane Dowodzenie poprawności całkowitej Przykład Przykład Kolejny problem Binarne warunki końcowe Warunki poprawności Reguły dowodzenia Reguły dowodzenia, c.d. Przykład Logika algorytmiczna System dowodzenia

Poprawność systemu dowodzenia stwierdzeń o całkowitej poprawności instrukcji języka TINY względem warunków wstępnego i końcowego można łatwo pokazać przez indukcję po strukturze dowodu. Przypadki reguł innych niż reguła dla instrukcji pętli są łatwe i w gruncie rzeczy bardzo podobne do dowodu dla odpowiednich przypadków w dowodzie poprawności systemu dowodzenia logiki Hoare'a (dla stwierdzeń częściowej poprawności) --- patrz wykład 11, slajd 2. Przypadek dla instrukcji przypisania wykorzystuje fakt, że każde podwyrażenie w formule można zastąpić zmienną o wartości równej wartości tego podwyrażenia --- a dalej dowód jest łatwy. Przypadek dla instrukcji pustej jest oczywisty. Przypadek dla instrukcji złożonej wymaga argumentacji podobnej, jak dla częściowej poprawności, ale korzystającej z monotoniczności przeciwobrazu (równie oczywistej jak monotoniczność obrazu). Poprawność reguły dla instrukcji warunkowej znów przebiega jak dla poprawności częściowej. Podobnie przypadek dla reguły wynikania (choć znów korzystamy z monotoniczności przeciwobrazu).

Zajmijmy się więc przypadkiem dla instrukcji pętli. Załóżmy, że zachodzą wszystkie trzy przesłanki tej reguły. Rozpatrzymy dowolny stan początkowy, spełniający niezmiennik przy dowolnej naturalnej wartości licznika $l$. Przez prostą indukcję indukcję względem wartości tej zmiennej w stanie początkowym (ta wartość to liczba naturalna, wykorzystujemy najbardziej standardową zasadę indukcji), korzystając z warunków wyrażonych przesłankami reguły, łatwo pokazać, że wartością znaczenia instrukcji pętli w tym stanie początkowym jest pewien stan końcowy, spełniający niezmiennik pętli z licznikiem zastąpionym stałą zero. To już prawie koniec dowodu: rozpatrzmy bowiem dowolny stan początkowy spełniający podany w konkluzji reguły warunek początkowy. Z definicji semantyki kwantyfikatora egzystencjalnego, istnieje stan różniący się od tego stanu początkowego co najwyżej wartością zmiennej $l$, który spełnia niezmiennik pętli przy pewnej naturalnej wartości tej zmiennej. Na mocy poprzedniego argumentu, wartość znaczenia instrukcji pętli w tym stanie jest określona i jest stanem końcowym spełniającym niezmiennik ze stałą zero wstawioną za zmienną $l$. Ale: zmienna $l$ w ogóle nie występuje w samej instrukcji pętli (jest to nowa zmienna); jej wartość w stanie początkowym nie może wpływać na przebieg obliczeń instrukcji pętli. Zatem także dla naszego stanu początkowego, znaczenie instrukcji pętli jest określone i daje stan końcowy także spełniający niezmiennik ze stałą zero wstawioną za zmienną $l$ (bo różniący się od wskazanego powyżej stanu końcowego co najwyżej wartością zmiennej $l$, która w tym ostatnim warunku nie występuje).

To kończy dowód dla tego przypadku i dowód poprawności całego systemu podanych reguł dowodzenia całkowitej poprawności instrukcji języka TINY względem warunków początkowego i końcowego.