SW wykład 12 - Slajd3
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
Istnieją także inne rozwiązania przykładowego zadania programistycznego zadanego warunkami z poprzedniego slajdu. Niestety, niektóre z nich nie spełniają naszych intuicyjnych oczekiwań --- i tu pojawiają się problemy z wykorzystaniem częściowej poprawności w ten sposób.
Łatwo na przykład pokazać, że każdy program, który ma tylko nieskończone obliczenia, jest częściowo poprawny względem dowolnych warunków początkowego i końcowego, a więc także jest "dobrym" rozwiązaniem naszego przykładowego zadania.
Poprawność częściowa nie gwarantuje terminacji programu, zatem specyfikacje wykorzystywane tu jako sformułowanie zadania programistycznego nie wymagają zakończenia działania programów, będących dopuszczalnymi rozwiązaniami tak podanych zadań. Oczywiście, dopuszczalność takich trywialnych i, intuicyjnie, trywialnie niewłaściwych rozwiązań nie może być zadowalająca.
