SW wykład 10 - Slajd10
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 , podany program wylicza jej całkowity pierwiastek kwadratowy --- w stanie końcowym programu wartość tego pierwiastka ma zmienna . To właśnie mówi podane stwierdzenie o częściowej poprawności programu i tego właśnie będziemy dowodzić poniżej.
