SW wykład 12 - Slajd14
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
Ostatnia uwaga do poprzedniego slajdu wskazuje metodę dowodzenia całkowitej poprawności programów względem warunków wstępnego i końcowego. Formalnie, łatwo pokazać, że instrukcja języka TINY jest całkowicie poprawna względem zadanych warunków wstępnego i końcowego wtedy i tylko wtedy, gdy instrukcja ta jest częściowo poprawna względem tych warunków, oraz gdy obliczenia tej instrukcji rozpoczynające się w stanach spełniających warunek wstępny są skończone. Własność ta przenosi się także na dowolne programy deterministyczne, w których nie może następować sytuacja błędna (blokowanie obliczenia przed zakończeniem programu).
Z tego już wynika, że aby pokazać całkowitą poprawność instrukcji pętli względem zadanego niezmiennika jako warunku wstępnego i tegoż niezmiennika wzmocnionego o negację warunku wejścia do ciała pętli jako warunku końcowego, wystarczy pokazać, że zachodzą dwa warunki. Po pierwsze: ciało pętli jest całkowicie poprawne względem warunku wstępnego, którym jest niezmiennik pętli wzmocniony o warunek wejścia do ciała pętli, i warunku końcowego, którym jest niezmiennik pętli. Pokazuje to częściową poprawność instrukcji pętli względem rozważanych warunków wstępnego i końcowego, oraz brak nieskończonych obliczeń ciała pętli rozpoczynających się w interesujących nas stanach. Po drugie: wskazujemy zbiór wartości z relacją dobrze ufundowaną oraz funkcję, która przyporządkowuje stanom wartości w tym zbiorze tak, że dla każdego stanu spełniającego niezmiennik pętli i warunek wejścia do ciała pętli, wartość tej funkcji dla tego stanu jest w relacji z wartością tej funkcji dla stanu po zakończeniu obliczenia ciała pętli rozpoczętego w tym stanie. Uwaga: można dopuścić wykorzystanie tu funkcji częściowej, o ile jest ona określona na wszystkich stanach spełniających niezmiennik pętli. Zgodnie z uwagami przy poprzednim slajdzie, pokazuje to brak nieskończonych obliczeń instrukcji pętli rozpoczynających się w stanach spełniających niezmiennik.
