SW wykład 10 - Slajd2

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

Dla ścisłego przedstawienia pojęcia poprawności programów niezbędna jest oczywiście ścisła definicja języka programowania, którego programy chcemy rozważać --- ścisła definicja jego składni i semantyki. W świetle dotychczasowych wykładów, możemy przyjąć, że taką definicją dysponujemy (a przynajmniej, że wiemy jak można takie formalne definicje budować).

Drugim niezbędny składnikiem dyskusji o poprawności programów jest formalna definicja stosowanych specyfikacji: składnia i semantyka języka budowania specyfikacji. Nie będziemy tu zbytnio zgłębiać tej tematyki --- przy bogactwie metod specyfikacji programów i formalizmów budowania specyfikacji równym przynajmniej wielości języków programowania, pełne przedstawienie licznych metod specyfikacji programów to temat na zupełnie odrębne zajęcia. Składnię i semantykę specyfikacji programów wprowadzimy tu tylko dla niektórych, najprostszych sformułowaniem warunków poprawności programów. Oczywistym punktem wyjścia będą formuły logiki pierwszego rzędu.

Kluczowa jednak dla analizy poprawności programów jest formalna definicja własności poprawności: posługując się semantycznymi pojęciami znaczenia programu i jego specyfikacji, możemy też ściśle i precyzyjnie zdefiniować, co to znaczy, że jakiś program jest poprawny względem podanej specyfikacji; czy też, jak się niekiedy mówi, co to znaczy, że program spełnia daną specyfikację.