SW wykład 11 - Slajd8
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
Dla analizy pełności systemu dowodzenia dla logiki Hoare'a dla tak uogólnionego języka TINY wygodne są jeszcze dodatkowe pojęcia.
Dla dowolnej instrukcji i warunku końcowego, zdefiniujmy semantyczny najsłabszy częściowy warunek wstępny jako zbiór dokładnie tych stanów, dla których wynik znaczenia tej instrukcji jest albo nieokreślony, albo jest określony i spełnia warunek końcowy.
Powiemy, że formuły pierwszego rzędu są ekspresywne nad naszym pierwotnym typem danych dla języka TINY, gdy dla każdej instrukcji i dla każdej formuły pierwszego rzędu, semantyczny najsłabszy warunek wstępny dla tej instrukcji i warunku końcowego będącego tą formułą jest wyrażalny formułą pierwszego rzędu, tzn., istnieje taka formuła pierwszego rzędu, że jest on dokładnie zbiorem stanów, w których ona zachodzi. Czasem łatwiej będzie wówczas powiedzieć po prostu, że nasz pierwotny typ danych jest ekspresywny.
