SW wykład 11 - Slajd7
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
Stwierdzenia o częściowej poprawności instrukcji uogólnionego języka TINY wprowadzamy i definiujemy ich prawdziwość dokładnie tak, jak poprzednio. Uwaga jednak: oczywiście, formuły pierwszego rzędu wykorzystują teraz wyrażenia logiczne zmodyfikowanego języka, a więc mówią o stanach wartościujących zmienne w nośnik algebry modelującej pierwotny typ danych, używając predykatów podanych w sygnaturze tego typu.
Zachowujemy też dokładnie reguły dowodzenia dla logiki Hoare'a, jak podane one zostały na slajdzie 9 poprzedniego wykładu. Oczywiście, implikacje wykorzystywane w regule wynikania mówią teraz o warunkach dotyczących algebry pierwotnego typu danych, nie o modelu liczb całkowitych. I właśnie z formuł prawdziwych w tej algebrze możemy teraz korzystać w dowodach prowadzonych w tym systemie dowodzenia dla logiki Hoare'a.
Nadal zachodzi twierdzenie o poprawności tak określonego systemu dowodzenia dla logiki Hoare'a (dowód bez istotnych zmian w stosunku do dowodu poprawności dla początkowej wersji języka TINY operującej na typie liczb całkowitych).
