SW wykład 10 - Slajd5

<<powrót do strony wykładu

Poprawność programów i weryfikacja Poprawność programów Dowodzenie poprawności Wyspecyfikowany program Logika Hoare'a Definicje formalne Definicje formalne, c.d. Semantyka logiki Hoare'a Reguły wnioskowania Przykład dowodu Przykład dowodu, c.d. Niezmiennik pętli Przykład dowodu, c.d. W pełni wyspecyfikowany program Teorie pierwszego rzędu

Stwierdzenia o częściowej poprawności programów, takie jak pokazane na poprzednim slajdzie, zostały sformalizowane i zaopatrzone w odpowiedni system ich dowodzenia w systemie logicznym zaproponowanym przez C.A.R. Hoare'a (w końcu lat 60., w ślad za wcześniejszymi pracami Turinga, Floyda i innych).

Formalnie będziemy tu analizować wersję tej logiki dla programów naszego języka TINY w najprostszej jego wersji (patrz wykład 4, slajdy 5, 6, 9, 10), z warunkami wstępnymi i końcowymi zadanymi jako formuły pierwszego rzędu interpretowane w stanach. Stwierdzenia o (częściowej) poprawności instrukcji języka TINY względem warunków wstępnego i końcowego zapisywać będziemy jak w ramce na górze slajdu. Na razie nieformalnie, takie stwierdzenie o poprawności interpretować będziemy jak zapisano w ramce na dole slajdu.