SW wykład 11 - Slajd9

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

Dość łatwo teraz pokazać, że dla dowolnej ekspresywnej algebry pierwotnego typu danych, jeśli jakieś stwierdzenie o częściowej poprawności instrukcji języka TINY nad tym pierwotnym typem danych względem warunków wstępnego i końcowego jest prawdziwe, to istnieje dla niego dowód w systemie dowodzenia dla logiki Hoare'a wykorzystujący formuły pierwszego rzędu prawdziwe w algebrze pierwotnego typu danych.

Pomijamy dowód, który przebiega przez indukcję względem struktury instrukcji. Niezbędne dla konstrukcji wyprowadzenia w systemie dla logiki Hoare'a asercje konstruuje się tu korzystając z ekspresywności algebry pierwotnego typu danych.

Własność tę określa sie jako relatywną pełność (albo: pełność w sensie Cooke'a) logiki Hoare'a.

Pozostaje jeszcze pytanie, jak mocne jest założenie o ekspresywności algebry pierwotnego typu danych. Okazuje się, niestety, że jest to założenie spełnione tylko przez niektóre algebry: algebra jest ekspresywna, gdy dla każdej instrukcji można z góry ograniczyć liczbę stanów, które mogą się pojawić w obliczeniach tej instrukcji, niezależnie od stanu początkowego, lub gdy w algebrze możemy zakodować standardowy model arytmetyki Peano.

Ta ostatnia opcja wyjaśnia, dlaczego zachodzi relatywna pełność logiki Hoare'a dla początkowej wersji języka TINY (dla liczb całkowitych).