SW wykład 12 - Slajd19

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

Wprowadzamy teraz stwierdzenia (całkowitej) poprawności instrukcji języka TINY względem zwykłego warunku wstępnego i binarnego warunku końcowego, zapisywane jak na slajdzie.

Stwierdzenie takie zachodzi, gdy dla każdego stanu początkowego spełniającego warunek wstępny, znaczenie instrukcji jest określone i daje stan końcowy, który razem z tym stanem początkowym spełnia binarny warunek końcowy. Zauważmy, że jeśli warunek końcowy jest zwykłą formułą (nie wykorzystuje zmiennych ze znacznikiem stanu początkowego) to stwierdzenie to jest tożsame ze stwierdzeniem o całkowitej poprawności tej instrukcji względem tych samych warunków wstępnego i końcowego. Dodatkowo jednak zyskujemy tu możliwość mówienia w warunku końcowym o początkowych wartościach zmiennych.