SW wykład 12 - Slajd7

<<powrót do strony wykładu

Zadanie programistyczne Przykład Problemy z logiką Hoare'a Poprawność całkowita Poprawność całkowita, c.d. Poprawność całkowita, c.d. Reguła dla pętli Poprawność systemu dowodzenia dla Tiny Pełność systemu dowodzenia dla Tiny Przykład Uogólnienie Poprawność i pełność Relacje dobrze ufundowane Dowodzenie poprawności całkowitej Przykład Przykład Kolejny problem Binarne warunki końcowe Warunki poprawności Reguły dowodzenia Reguły dowodzenia, c.d. Przykład Logika algorytmiczna System dowodzenia

Istotnie nowa w stosunku do reguł dla dowodzenia częściowej poprawności jest reguła dla instrukcji pętli. Musimy tu nie tylko wskazać niezmiennik pętli, ale także pokazać, że dla stanów spełniających ten niezmiennik, obliczenia instrukcji pętli zakończą się po skończonej liczbie wykonań jej ciała. I tu tkwi klucz do zrozumienia podanej reguły: wprowadzamy dodatkową, nową zmienną $l$, której wartości przebiegają liczby naturalne i określają "licznik" wskazujący liczbę wykonań ciała pętli, po których realizacja całej instrukcji zostanie zakończona. Oczywiście, niezmiennik musi określać wartość zmiennej $l$ w zależności od wartości zmiennych występujących w instrukcji pętli.

Przesłanki reguły to trzy warunki: w stanach spełniających niezmiennik przy dodatnich wartościach licznika zachodzi warunek wejścia do pętli, ciało pętli wykonuje się prowadząc do stanu końcowego spełniającego niezmiennik, ale z wartością licznika o jeden mniejszą, i w końcu, w stanach spełniających niezmiennik przy wartości licznika równej zero warunek wejścia do pętli jest fałszywy. Łatwo widać, że z tych trzech warunków już wynika, że dla każdego stanu spełniającego niezmiennik (przy dowolnej naturalnej wartości licznika), instrukcja pętli wykona się, prowadząc do stanu końcowego spełniającego niezmiennik pętli przy wartości licznika zero (a dokładniej: niezmiennik, w którym stała zero zastępuje licznik).