SW wykład 10 - Slajd3

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

Mając już pojęcie poprawności programów względem specyfikacji formalnie zdefiniowane w terminach ich semantyki, dla wykorzystania tego pojęcia w praktyce ważne jest podanie pewnego formalnego systemu dowodzenia takich własności. Stwierdzenia o poprawności programu względem specyfikacji traktujemy tu jak formuły logiczne i wprowadzamy pewien formalny system dowodzenia. Niezbędny jest też wtedy dowód poprawności podanego systemu dowodzenia: musimy wiedzieć, że pozwala on na dowodzenie jedynie prawdziwych (zachodzących w sensie semantycznym, zgodnie z definicją) stwierdzeń o poprawności programów względem specyfikacji. Tak rozumiana poprawność logiki nie może być pominięta. Nieco mniej ważna jest pełność proponowanego systemu dowodzenia: wymaganie, że w proponowanym rachunku logicznym można udowodnić wszystkie stwierdzenia o poprawności programów względem ich specyfikacji, które zachodzą w sensie semantycznym. Dla praktycznych systemów dowodzenia poprawności programów względem nietrywialnych specyfikacji, pełność jest na ogół nieosiągalna: musimy się zadowolić pokazaniem nieco słabszych własności, które pełnić będą podobną rolę (pełność przy różnych dodatkowych założeniach o programach i ich specyfikacjach). Jakaś forma pełności jest jednak także niezbędna: nie chcemy zadowolić się systemem, który nie pozwala na przykład pokazać poprawności żadnej instrukcji pętli...