SW wykład 12 - Slajd17
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
Uporawszy się z problemem zapewnienia własności stopu, zmierzmy się z kolejną słabością częściowej (i całkowitej) poprawności. Mianowicie, pojęcie to nie oferuje żadnego formalnego mechanizmu opisania związku pomiędzy stanem początkowym a stanem końcowym programu.
Na przykład, "dobrym" rozwiązaniem zadania programistycznego mówiącego o obliczeniu całkowitego pierwiastka kwadratowego z wartości pewnej zmiennej jest przypisanie tej zmiennej zera i określenie zera jako jej całkowitego pierwiastka kwadratowego.
Zapobiegać takim i podobnym "rozwiązaniom" można co najmniej na kilka sposobów.
Chyba najprostszy z nich polega na podaniu listy zmiennych, które mogą być wykorzystywane w warunkach wstępnym i końcowym, ale nie mogą pojawić się w programie (a przynajmniej, nie mogą być przez ten program zmieniane). Często przy tym praktycznie ważniejszy jest wariant tej metody, gdy określamy listę zmiennych, których wartości program może zmieniać (zmiennych zmienianych przez program jest zawsze skończenie wiele; zmiennych, których on nie wykorzystuje, jest potencjalnie nieskończenie wiele).
Inne podejście podejmuje ten problem szerzej, przez wprowadzenie mechanizmów wiązania wartości zmiennych w stanie przed wykonaniem instrukcji i w stanie po jej wykonaniu, albo przez rozszerzenie pojęcia poprawności do warunków końcowych opisujących relację między stanem początkowym i końcowym obliczeń specyfikowanego programu. Inne jeszcze podejście to budowa bardziej złożonych systemów logicznych opartych o związane z programami modalności.
