SW wykład 11 - Slajd2
Poprawność systemu dowodzenia Hoare'a Dowód Dowód, c.d. Problem z pełnością Uogólnienie TINY TINY Ekspresywność Relatywna pełność logiki Hoare'a Rozszerzenia Ograniczenia
Dowód poprawności podanego systemu dowodzenia dla logiki Hoare'a przebiega przez indukcję po strukturze dowodu. Oznacza to, że musimy pokazać poprawność każdej z reguł dowodzenia w tym systemie: dla każdej reguły, jeśli semantycznie prawdziwe są wszystkie jej przesłanki, to semantycznie prawdziwa jest też jej konkluzja.
Reguła dla instrukcji przypisania: najpierw przez prostą indukcję po strukturze formuł pierwszego rzędu należy uogólnić znany już dla wyrażeń fakt, że każde podwyrażenie można zastąpić zmienną o wartości równej wartości tego podwyrażenia (wykład 2, slajd 18) --- potrzebne tu sformułowanie tego faktu dla formuł podajemy na slajdzie powyżej. Dalszy dowód jest już oczywisty przez odwołanie się do semantyki instrukcji przypisania.
Poprawność reguły dla instrukcji pustej jest oczywista.
Aby pokazać poprawność reguły dla instrukcji złożonej, załóżmy, że jej dwie przesłanki są prawdziwe, co oznacza, że obraz względem znaczenia instrukcji składowej zbioru stanów spełniających jej warunek wstępny jest zawarty w zbiorze stanów spełniających jej warunek końcowy. Ponieważ znaczeniem instrukcji złożonej jest złożenie znaczeń instrukcji składowych, więc obraz zbioru stanów spełniających warunek wstępny względem tego znaczenia jest obrazem względem znaczenia drugiej składowej obrazu względem znaczenia pierwszej składowej zbioru stanów spełniających warunek wstępny. Korzystając z monotoniczności obrazu względem danej funkcji i z założeń o prawdziwości przesłanek reguły, łatwo już pokazać, że także konkluzja reguły jest prawdziwa.
Poprawność reguły dla instrukcji warunkowej pokazujemy podobnie. Z założeń o prawdziwości przesłanek reguły, przez prostą analizę przez przypadki pokazujemy konkluzję: mając dany stan początkowy spełniający warunek wstępny instrukcji warunkowej, w zależności od tego, czy wyrażenie logiczne instrukcji warunkowej, czy też jego negacja ma wartość prawda w danym stanie początkowym, korzystamy z prawdziwości pierwszej lub drugiej przesłanki, pokazując, że obraz tego stanu względem semantyki instrukcji warunkowej (jeśli jest określony to) spełnia warunek końcowy. Zauważmy, że wykorzystujemy tu określoność wartości wyrażeń w każdym stanie: dla dowolnego stanu, albo wyrażenie logiczne, albo jego negacja ma wartość prawda.
Poprawność reguły wynikania można pokazać wykorzystując monotoniczność obrazu względem znaczenia instrukcji i oczywisty fakt, że implikacja dwóch formuł jest prawdziwa w naszym modelu liczb całkowitych wtedy i tylko wtedy, gdy zbiór stanów spełniających pierwszą z tych formuł jest zawarty w zbiorze stanów spełniających drugą z nich.
