SW wykład 12 - Slajd22

<<powrót do strony wykładu

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

Prosty przykład: dobrą specyfikacją znanego nam programu obliczającego całkowity pierwiastek kwadratowy liczby naturalnej jest wymaganie, by był on poprawny względem zwykłego warunku wstępnego ($n$ jest liczbą naturalną) i binarnego warunku końcowego, który mówi, że zmienna $rt$ w stanie końcowym ma wartość całkowitego pierwiastka kwadratowego wartości zmiennej $n$ w stanie początkowym. Oczywiście, uniemożliwia to akceptację "rozwiązania" zmieniającego wartość zmiennej $n$ i określającego wartość $rt$ jako całkowity pierwiastek kwadratowy z nowej wartości zmiennej $n$.