SW wykład 11 - Slajd10

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

Stwierdzenia o częściowej poprawności względem warunków wstępnego i końcowego można oczywiście rozszerzyć na kolejne postacie instrukcji, dodawane stopniowo do naszego języka TINY. Odpowiednio rozszerza się wówczas system dowodzenia, podając reguły dla wprowadzanych konstrukcji językowych.

Na przykład, dla procedur bezparametrowych (a raczej dla ich wywołań) poprawna jest reguła podana na powyższym slajdzie: stwierdzenie o poprawności wywołania procedury bezparametrowej względem podanych warunków wstępnego i końcowego można wywieść pod warunkiem, że z tegoż stwierdzenia można wywieść stwierdzenie o częściowej poprawności ciała procedury względem tychże warunków wstępnego i końcowego. W pewnym sensie, jest to reguła "wyższego rzędu", wykorzystująca dowodzoną tezę jako przesłankę, którą można wykorzystać w dowodzie istotnej przesłanki (poprawności ciała procedury) dla analizy rekurencyjnych wywołań tej procedury. Przy tym, choć często ta reguła okazuje się wystarczająca, to dla zapewnienia relatywnej pełności tak rozszerzonego systemu trzeba ją jeszcze uzupełnić o możliwość manipulacji zmiennymi pomocniczymi.

Łatwo też sformułować regułę dla dowodzenia stwierdzeń o częściowej poprawności instrukcji bloku z deklaracjami zmiennych lokalnych --- patrz slajd.

Pełna analiza tych czy podobnych reguł dla innych konstrukcji wykracza poza zakres tych zajęć. Trzeba tylko wiedzieć, że reguły takie opracowano dla wszelkich właściwie pojawiających się konstrukcji językowych, a analiza (relatywnej) pełności otrzymywanych systemów długo była tematem prac badawczych, z czasem dopiero stając się raczej rutynowym przedsięwzięciem, o dobrze zakreślonych granicach i z dość standardowymi technikami dowodzenia.