SW wykład 12 - Slajd15

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

Rozpatrzmy prosty przykład w (rozszerzonym o wywołania dowolnych funkcji w wyrażeniach) języku TINY. Ciało powyższej pętli albo zmniejsza o jeden wartość zmiennej $y$ albo zmniejsza o jeden wartość zmiennej $x$ zmieniając przy tym wartość zmiennej $y$ w bliżej nieokreślony sposób. Zakładamy jednak, że zmiana ta nie powoduje błędu i nie wyprowadza poza liczby naturalne. Bez dalszych informacji o funkcji $f$ nie można liczyć na dowód całkowitej poprawności tej pętli na mocy pierwotnej reguły dowodzenia całkowitej poprawności dla instrukcji pętli (opartej o licznik o wartościach naturalnych). Jednak dowód całkowitej poprawności zgodny z metodą przedstawioną na poprzednim slajdzie jest łatwy: wystarczy rozważyć oczywistą funkcję w pary liczb naturalnych, która przy każdym wykonaniu ciała pętli zmniejsza swą wartość względem leksykograficznego (dobrze ufundowanego) porządku na takich parach.