SW wykład 12 - Slajd13
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
Dowodzenie własności stopu dla instrukcji pętli w sposób określony regułą dla instrukcji pętli często okazuje się jednak niewygodne. Wymaganie dokładnego określenia liczby wykonań ciała pętli niezbędnych do zakończenia jej wykonania może okazać się zbyt mocne i nierealistyczne w praktyce. Pierwsza, oczywista modyfikacja, to dopuszczenie możliwości dowolnego zmniejszania wartości "licznika" pętli przy każdym wykonaniu jej ciała o być może więcej niż jeden.
Często wygodne okazuje się też dalsze uogólnienie, gdzie wartości "licznika" przebiegają pewien zbiór (niekoniecznie liczby naturalne) z dodatkowo określoną dobrze ufundowaną relacją. Relacja jest dobrze ufundowana, gdy nie istnieje nieskończony ciąg wartości takich, że każda z nich jest w tej relacji z wartością następną w tym ciągu.
Na slajdzie podajemy kilka typowych przykładów zbiorów z relacją dobrze ufundowaną.
Aby pokazać, że obliczenia pętli się kończą, wymagamy, by wartość "licznika" w stanie (spełniającym niezmiennik pętli) przed wykonaniem ciała pętli była w relacji z wartością "licznika" w stanie po wykonaniu ciała pętli. Łatwo teraz widać, że jeśli ta własność jest spełniona, to obliczenia instrukcji pętli nie mogą nieskończenie wiele razy wykonywać ciała pętli.
