SW wykład 11 - Slajd8

<<powrót do strony wykładu

Poprawność systemu dowodzenia Hoare'a Dowód Dowód, c.d. Problem z pełnością Uogólnienie TINY${}_A$ TINY${}_A$ 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.