SW wykład 12 - Slajd5
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
Dla formalnego zdefiniowania znaczenia stwierdzeń całkowitej poprawności, wprowadźmy jeszcze oznaczenie dualne do obrazu zbioru stanów względem (znaczenia) instrukcji: przeciwobraz zbioru stanów względem (znaczenia) instrukcji --- patrz pojedyncza ramka.
Teraz: instrukcja języka TINY jest całkowicie poprawna względem warunków wstępnego i końcowego, gdy zbiór stanów spełniających warunek wstępny jest zawarty w przeciwobrazie zbioru stanów spełniających warunek końcowy względem (znaczenia) tej instrukcji. Innymi słowy, dla każdego stanu, jeśli ten stan spełnia warunek wstępny to znaczenia instrukcji jako funkcja częściowa ma określoną wartość na tym stanie i zadany jako ta wartość stan końcowy spełnia warunek końcowy.
UWAGA: sformułowanie to nie budzi wątpliwości dla języków deterministycznych, takich jak TINY, gdzie znaczeniem instrukcji są funkcje częściowe. Rozpatrzymy jednak przez chwilę języki niedeterministyczne (jak rozszerzenie języka TINY szkicowane na wykładzie 3, slajd 16) z naturalną semantyką denotacyjną, gdzie znaczeniami instrukcji są binarne relacje na stanach, w oczywisty sposób powiązane z obliczeniami instrukcji. Wprowadźmy też oczekiwane pojęcie przeciwobrazu zbioru stanów względem (relacyjnego znaczenia) instrukcji. Wówczas powyższa definicja całkowitej poprawności mówi: dla każdego stanu, jeśli ten stan spełnia warunek wstępny to istnieje obliczenie tej instrukcji prowadzące do stanu końcowego, który spełnia warunek końcowy. Nieformalnie mówi się tu o "anielskim niedeterminizmie": skoro istnieje obliczeni prowadzące do sukcesu, to właśnie takie obliczenie zostaje rozpatrzone. Jest to wymaganie słabsze niż być może bardziej oczekiwana wersja: dla każdego stanu, jeśli ten stan spełnia warunek wstępny to istnieje obliczenie tej instrukcji prowadzące do stanu końcowego i każdy możliwy stan końcowy spełnia warunek końcowy. To zaś z kolei jest wymaganiem słabszym niż być może najbardziej oczekiwane: dla każdego stanu, jeśli ten stan spełnia warunek wstępny to każde obliczenie tej instrukcji prowadzi do stanu końcowego, który spełnia warunek końcowy. Tu z kolei mówi się o "diabelskim niedeterminizmie": musimy rozpatrzyć wszystkie możliwe obliczenia, bo jeśli istnieje obliczenie złe, to ono właśnie może się przydarzyć. Warto też zauważyć, że to ostanie pojęcie całkowitej poprawności dla programów niedeterministycznych nie może być wyrażone w terminach semantyki denotacyjnej określającej znaczenia instrukcji jako relacje między stanami początkowymi i końcowymi. Tak rozumiana całkowita poprawność odróżnia bowiem program, który dla każdego stanu początkowego ma jedno deterministyczne obliczenie. od programu, który dla każdego stanu początkowego niedeterministycznie wybiera obliczenie pętlące się lub obliczenie pierwszego programu.
