SW wykład 10 - Slajd7
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
Rozwijając dalej wprowadzone notacje i wykorzystując wprowadzone funkcje semantyczne, wprowadzamy dwa nowe oznaczenia.
Pierwsze to zbiór stanów, w których spełniona jest dana formuła pierwszego rzędu --- tj., w terminach naszej semantyki, zbiór tych stanów, dla których znaczenie tej formuły (jako funkcja ze stanów w wartości logiczne) daje wartość prawda.
Drugie to obraz zbioru stanów początkowych po wykonaniu instrukcji --- tj., w terminach naszej semantyki, obraz zbioru stanów względem funkcji ze stanów w stany, która jest znaczeniem tej instrukcji.
