SW wykład 12 - Slajd10

<<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

Spójrzmy na prosty, znany nam już świetnie przykład programu liczącego całkowity pierwiastek kwadratowy liczby naturalnej. Dla dowodu jego całkowitej poprawności względem tych samych co dotychczas warunków wstępnego i końcowego należy wzmocnić niezmiennik o określenie (formułą pierwszego rzędu) wartości licznika $l$ wskazującego liczbę wykonań ciała pętli do zakończenia jej obliczeń --- co w tym przypadku jest dość oczywiste. Łatwo już teraz sprawdzić, że przy tak zadanym niezmienniku można zastosować regułę dla pętli (to znaczy, pokazać wszystkie jej trzy przesłanki), otrzymując jako konkluzję stwierdzenie o całkowitej poprawności względem niezmiennika (dla egzystencjalnie skwantyfikowanej zmiennej $l$) jako warunku wstępnego i tegoż niezmiennika z zerem zastępującym zmienną $l$ jako warunkiem końcowym. Teraz już proste zastosowanie reguły wynikania daje dowodzone stwierdzenie całkowitej poprawności.