SW wykład 10 - Slajd10

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

Pokażemy teraz prosty przykład dowodu stwierdzenia częściowej poprawności podanego na slajdzie programu w języku TINY względem podanych warunków wstępnego i końcowego. W poniższej prezentacji dowodu będziemy pomijać ważne (ale też oczywiste) kroki stosowania reguły wynikania, pozwalające w szczególności na zastąpienie dowolnej formuły pierwszego rzędu formułą jej równoważną (spełnioną przez ten sam zbiór stanów).

Nieformalnie: dla dowolnej liczby naturalnej $n$, podany program wylicza jej całkowity pierwiastek kwadratowy --- w stanie końcowym programu wartość tego pierwiastka ma zmienna $rt$. To właśnie mówi podane stwierdzenie o częściowej poprawności programu i tego właśnie będziemy dowodzić poniżej.