SW wykład 12 - Slajd20

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

Spójrzmy na typowe reguły dowodzenia poprawności instrukcji względem zwykłego warunku wstępnego i binarnego warunku końcowego. Dzięki wykorzystaniu warunków binarnych możemy tu bardzo dokładnie opisać w warunku końcowym znaczenie każdej instrukcji. Najlepiej widać to chyba w powyższej regule dla instrukcji przypisania: dla zadanego warunku wstępnego, jest ona poprawna względem tego warunku i binarnego warunku końcowego, który zawiera pełną informację o warunku zachodzącym w stanie początkowym, o wartości zmiennej, na którą jest wykonywane przypisanie, i o tym, że wartości każdej innej zmiennej nie zmieniają się. Podobnie w gruncie rzeczy skonstruowana jest reguła dla instrukcji pustej.

Reguła dla instrukcji złożonej wymaga dodatkowej operacji na binarnych formułach pierwszego rzędu odpowiadającej złożeniu opisywanych przez nie relacji binarnych: łatwo to wyrazić wykorzystując egzystencjalną kwantyfikację (po odpowiednim przemianowaniu zmiennych pośrednich, tak by zwykłe zmienne, mówiące o stanie końcowym pierwszej instrukcji składowej, utożsamić ze zmiennymi, mówiącymi o stanie początkowym dla drugiej składowej w jej binarnym warunku końcowym).