SW wykład 12 - Slajd21
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
Reguła dla instrukcji warunkowej jest dość standardowa: wykorzystanie binarnych warunków końcowych nie wprowadza tu nic nowego.
Ważna i ciekawa, jak zwykle, jest reguła dla pętli. Po pierwsze, mamy tu do czynienia z dwoma niezmiennikami: zwykłym niezmiennikiem, takim jak poprzednio, oraz niezmiennikiem binarnym, opisującym dowolną niezerową liczbę kolejnych wykonań ciała pętli. Przesłanki reguły zapewniają, że rzeczywiście i są takimi niezmiennikami. Po drugie, warunek z metody dowodzenia własności stopu dla pętli przez funkcje (określone wyrażeniami) w zbiór z relacją dobrze ufundowaną, który wymaga, by funkcja ta zmniejszała swą wartość przy każdym wykonaniu ciała pętli, może tu zostać wyrażony w stwierdzeniu o poprawności ciała pętli względem odpowiedniego binarnego warunku końcowego.
W końcu, tym razem warto podać dwie reguły wynikania. Jedna, jak dotychczas, pozwala na dowolne wzmocnienie warunku wstępnego i osłabienie warunku końcowego. Druga zaś pozwala na wzmocnienie warunku końcowego o informację o stanie początkowym zawartą w warunku wstępnym.
Oczywiście, reguły te można podać w wielu wersjach, niekiedy wartych dalszego doszlifowania.
