SW wykład 12 - Slajd4
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.
