SW wykład 10 - Slajd8

<<powrót do strony wykładu

Poprawność programów i weryfikacja Poprawność programów Dowodzenie poprawności Wyspecyfikowany program Logika Hoare'a Definicje formalne Definicje formalne, c.d. Semantyka logiki Hoare'a Reguły wnioskowania Przykład dowodu Przykład dowodu, c.d. Niezmiennik pętli Przykład dowodu, c.d. W pełni wyspecyfikowany program Teorie pierwszego rzędu

Wykorzystując wprowadzone przed chwilą oznaczenia, łatwo już teraz formalnie zapisać znaczenie stwierdzeń o częściowej poprawności instrukcji. Mianowicie, stwierdzenie, że dana instrukcja jeżyka TINY jest częściowo poprawna względem warunków wstępnego i końcowego danych formułami pierwszego rzędu, zachodzi wtedy i tylko wtedy, gdy obraz zbioru stanów spełniających warunek wstępny po wykonaniu tej instrukcji jest zawarty w zbiorze stanów spełniających warunek końcowy. Innymi słowy, gdy dla każdego stanu, jeśli ten stan spełnia warunek wstępny i wynik (znaczenia) instrukcji w tym stanie jest określony, to wynik ten jest stanem spełniającym warunek końcowy.

Mamy nadzieję, że zgodność tego sformułowania z wcześniejszą, nieformalną prezentacją pojęcia częściowej formalności jest zupełnie oczywista.