SW wykład 10 - Slajd7: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 2: | Linia 2: | ||
[[Grafika:sw1006.png|frame|center|]] | [[Grafika:sw1006.png|frame|center|]] | ||
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. | |||
Aktualna wersja na dzień 17:06, 10 paź 2006
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.
