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łę.