SW wykład 10 - Slajd11
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
Krok po kroku dowodzimy, że zachodzą kolejne stwierdzenia o częściowej poprawności fraz występujących w podanym programie.
Pierwsze ze stwierdzeń na slajdzie wynika wprost z reguły dla instrukcji przypisania. Podobnie drugie. W obu przypadkach zachęcamy Państwa do samodzielnego podstawienia w warunku końcowym za zmienną, na którą wykonywane jest przypisanie, przypisywanego tej zmiennej wyrażenia oraz eliminację trywialnych składowych otrzymanej przez takie podstawienie formuły tak, aby otrzymać odpowiedni warunek wstępny.
Trzecie stwierdzenie o częściowej poprawności instrukcji złożonej z dwóch kolejnych przypisań wyprowadzamy z dwóch poprzednich za pomocą reguły dla instrukcji złożonej.
Zauważmy, że warunki końcowe podawane w tych stwierdzeniach możemy otrzymać niejako "mechanicznie", jako najmocniejsze warunki końcowe takie, że instrukcja przypisania jest częściowo poprawna względem zadanego wcześniej warunku wstępnego i tego właśnie warunku końcowego.
Strategii tej nie da się jednak stosować dalej. Kolejna instrukcja to bowiem instrukcja pętli, a warunek końcowy w ostatnim stwierdzeniu częściowej poprawności niewątpliwie niezmiennikiem tej pętli nie jest. Właśnie wymyślenie niezmienników pętli to najtrudniejsza część dowodów poprawności rozważanych programów. Choć istnieją narzędzia świetnie sobie radzące z "wymyślaniem" odpowiednich niezmienników dla typowych pętli, w ogólności jest to jednak zadanie wymagające inwencji programisty, czy osoby prowadzącej dowód poprawności (i dobrego rozumienia programu, którego poprawności dowodzimy). W tym przypadku, otrzymany dotychczas warunek końcowy należy wzmocnić do warunku końcowego podanego w ostatnim na tym slajdzie stwierdzeniu o częściowej poprawności instrukcji złożonej. Stwierdzenie to wynika z poprzedniego na mocy reguły wynikania.
