SW wykład 12 - Slajd23

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

I jeszcze jeden pomysł, w pewnym sensie najdalej idący: zamiast mówić bezpośrednio o poprawności programów, rozbudujemy system logiczny i zbiór formuł tak, by zawierały one w sobie programy. Dla każdej instrukcji języka TINY wprowadzamy nową "modalność", która mając daną formulę logiczną, buduje z niej (i z danej instrukcji) nową formułę, odpowiadającą najsłabszemu warunkowi wstępnemu, takiemu że dana instrukcja jest całkowicie poprawna względem tego warunku wstę>pnego i warunku końcowego będącego daną formułą. Dokładniej: powstała formuła jest spełniona dokładnie dla tych stanów, dla których instrukcja kończy swoje działanie w stanie końcowym spełniającym daną początkowo formułę.

Zwróćmy uwagę, że tak powstałe formuły traktujemy w zwykły sposób. Może być ona wykorzystana jak wcześniej zbudowane formuły, na przykład jako składowa formuł budowanych przez spójniki logiczne czy kwantyfikatory, a także przez użycie dalszych modalności. Możemy więc dowolnie zagnieżdżać i mieszać wykorzystanie spójników logicznych, kwantyfikatorów i modalności zadanych instrukcjami języka TINY.

Powstają w ten sposób bardzo ciekawe systemy logiczne; jeden z pierwszych takich systemów zaproponowany został przez Andrzeja Salwickiego w końcu lat 60. pod nazwą logika algorytmiczna, choć w świecie większą popularność zyskała wprowadzona później tzw. logika dynamiczna.

Warto się przekonać, że wprowadzone wcześniej pojęcia częściowej i całkowitej poprawności instrukcji języka TINY względem warunków wstępnego i końcowego danych formułami pierwszego rzędu łatwo wyrazić jako formuły tak zbudowanej logiki. Logiki tego typu pozwalają jednak także na opis bardziej złożonych własności programów.