SW wykład 11 - Slajd3
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
Poprawność reguły dla instrukcji pętli jest nieco trudniejsza.
Znaczenie instrukcji pętli definiujemy jako najmniejszy punkt stały odpowiedniego operatora na funkcjach częściowych ze stanów w stany. Zakładając, że prawdziwa jest przesłanka reguły (tzn., zakładając częściową poprawność ciała pętli względem warunku wstępnego, który jest koniunkcją niezmiennika pętli i warunku wejście do ciała pętli, i warunku końcowego, którym jest niezmiennik pętli), przez indukcję stałopunktową (patrz wykład 8, slajd 8) pokażemy, że prawdziwa jest też konkluzja reguły, tj., instrukcja pętli jest częściowo poprawna względem warunku wstępnego, którym jest niezmiennik pętli, i warunku końcowego, który jest koniunkcją niezmiennika pętli i negacji warunku wejścia do pętli.
Rozpatrzmy własność funkcji częściowych ze stanów w stany, która mówi, że obraz względem danej funkcji zbioru stanów spełniających niezmiennik pętli jest zawarty w zbiorze stanów spełniających ten niezmiennik i negację warunku wejścia do pętli. Zauważmy najpierw, że ponieważ obraz względem sumy łańcucha funkcji częściowych jest sumą obrazów względem funkcji w tym łańcuchu (zachodzi to też dla łańcucha pustego --- zatem nasza własność jest prawdziwa dla funkcji pustej), jest to własność dopuszczalna. Możemy więc dla niej stosować indukcję stałopunktową.
Załóżmy zatem, że jakaś funkcja częściowa ze stanów w stany tę własność spełnia. Pokażemy, że spełnia ją także wynik aplikacji do tej funkcji operatora, które najmniejszym punktem stałym jest znaczenie instrukcji pętli. Rozpatrzmy dowolny stan początkowy spełniający niezmiennik pętli. Jeśli warunek wejścia do pętli w tym stanie ma wartość fałsz, to obrazem tego stanu początkowego względem aplikacji operatora do naszej funkcji na stanach jest on sam, i co więcej, należy on do zbioru stanów spełniających niezmiennik pętli i negację warunku wejścia do pętli. Przypuśćmy zatem, że warunek wejścia do pętli ma w tym stanie początkowym wartość prawda. Wówczas, jeśli obraz tego stanu względem aplikacji operatora do naszej funkcji na stanach jest określony, to jest on obrazem względem naszej funkcji na stanach stanu pośredniego, który jest z kolei obrazem stanu początkowego względem znaczenia ciała pętli. Z założenia o prawdziwości przesłanki reguły, ten stan pośredni spełnia niezmiennik pętli. Zatem, ponieważ nasza funkcja ma analizowaną własność, otrzymany stan końcowy spełnia niezmiennik pętli i negację warunku wejścia do pętli. Pokazuje to, że obraz naszej funkcji względem tego operatora spełnia analizowaną własność. Zatem, na mocy indukcji stałopunktowej, najmniejszy punkt stały tego operatora (będący znaczeniem instrukcji pętli) także tę własność spełnia. Rzeczywiście więc, rozważana instrukcja pętli jest częściowo poprawna względem niezmiennik pętli jako warunkiem wstępnym i koniunkcji tego niezmiennika z negacją warunku wejścia do pętli jako warunkiem końcowym --- czyli konkluzja reguły jest prawdziwa.
