SW wykład 12 - Slajd4: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 2: | Linia 2: | ||
[[Grafika:sw1203.png|frame|center|]] | [[Grafika:sw1203.png|frame|center|]] | ||
Oczywistym rozwiązaniem dla wskazanej słabości pojęcia częściowej | |||
poprawności jest wprowadzenie mocniejszej jego wersji, wymagającej | |||
także własności terminacji programu. Wprowadzamy więc "całkowitą | |||
poprawność" programu względem warunków wstępnego i końcowego --- | |||
zapisując odpowiednie stwierdzenia całkowitej poprawności jak w | |||
pierwszej ramce na slajdzie, a (na razie nieformalnie) rozumiejąc je | |||
jak przedstawiamy w ramce na dole. | |||
Aktualna wersja na dzień 22:05, 16 paź 2006
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
Oczywistym rozwiązaniem dla wskazanej słabości pojęcia częściowej poprawności jest wprowadzenie mocniejszej jego wersji, wymagającej także własności terminacji programu. Wprowadzamy więc "całkowitą poprawność" programu względem warunków wstępnego i końcowego --- zapisując odpowiednie stwierdzenia całkowitej poprawności jak w pierwszej ramce na slajdzie, a (na razie nieformalnie) rozumiejąc je jak przedstawiamy w ramce na dole.
