SW wykład 11 - Slajd1
Poprawność systemu dowodzenia Hoare'a Dowód Dowód, c.d. Problem z pełnością Uogólnienie TINY TINY Ekspresywność Relatywna pełność logiki Hoare'a Rozszerzenia Ograniczenia
Jak wspominaliśmy już na poprzednim wykładzie, najważniejsza własność każdego sensownego systemu dowodzenia to jego poprawność: wszystkie stwierdzenia, które możemy w danym systemie wyprowadzić, są semantycznie prawdziwe.
W pewnym sensie, na poprzednim wykładzie nadużywaliśmy nieco terminologii, mówiąc niekiedy, że dowodzimy częściowej poprawności pewnych programów względem podanych warunków wstępnego i końcowego, a naprawdę pokazując "tylko", że odpowiednie stwierdzenia o częściowej poprawności są wyprowadzalne w systemie dowodzenia dla logiki Hoare'a.
Spieszymy teraz tę lukę wypełnić: pokażemy, że rzeczywiście system dowodzenia dla logiki Hoare'a jest poprawny. W istocie więc, dowodząc w tym systemie na przykład stwierdzenia o częściowej poprawności naszego przykładowego programu względem podanych warunków wstępnego i końcowego, rzeczywiście pokazaliśmy, że jest częściowo poprawny względem tych warunków w zdefiniowanym na po przednim wykładzie (slajd 8), semantycznym sensie.
