SW wykład 12 - Slajd24

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

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 logiki pierwszego rzędu dla spójników i kwantyfikatorów. 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.