SW wykład 12 - Slajd24
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
Nie będziemy tu podawać pełnego systemu dowodzenia dla logiki naszkicowanej na po przednim slajdzie --- nie jest to zadanie trywialne. System taki zawiera oczywiście zwykłe reguły dla spójników i kwantyfikatorów logiki pierwszego rzędu. Do tego dodać należy szereg reguł (lub aksjomatów) wiążących modalności i spójniki zdaniowe --- jak pierwsze trzy aksjomaty podane na slajdzie. I w końcu, niezbędne są reguły (lub aksjomaty) mówiące o semantyce instrukcji wyznaczających rozważane modalności --- jak ostatni z podanych aksjomatów, ujmujący niejako semantykę instrukcji złożonej. Najtrudniejsze, jak zwykle, są reguły dla modalności wyznaczonych przez instrukcje pętli: na ogół wymagają one nieskończonej liczby przesłanek, i dopiero system z takimi nieskończonymi regułami może okazać się pełny.
