SW wykład 12 - Slajd2
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
Rozpatrzmy prosty (znany nam już) przykład: zadanie programistyczne zbudowania programu obliczającego całkowity pierwiastek kwadratowy z dowolnej liczby naturalnej. Formułując to w terminach stwierdzeń logiki Hoare'a, mamy zbudować program, który jest częściowo poprawny względem warunku wstępnego " jest liczbą naturalną" i warunku końcowego " jest całkowitym pierwiastkiem kwadratowym liczby naturalnej ". Jak zwykle, warunki te zapisujemy formułami pierwszego rzędu w oczywisty sposób.
Przedstawiony na wykładzie 10 ("Logika Hoare'a. Poprawność częściowa") przykładowy dowód częściowej poprawności pokazuje, że podany tam (i powtórzony tu) program jest jednym z dobrych rozwiązań tego zadania.
