SW wykład 12 - Slajd9
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
Okazuje się, że system reguł dowodzenia stwierdzeń całkowitej poprawności dla instrukcji języka TINY jest też (relatywnie) pełny: każde prawdziwe stwierdzenie całkowitej poprawności instrukcji języka TINY względem warunków wstępnego i końcowego można pokazać w tym systemie reguł korzystając jedynie z formuł pierwszego rzędu prawdziwych w algebrze liczb całkowitych z operacjami i predykatami z języka TINY. Szczegółowy dowód pomijamy. Zauważmy jedynie, że kluczem w tym dowodzie, jak i w dowodzie relatywnej pełności pełności logiki Hoare'a dla stwierdzeń częściowej poprawności, jest możliwość wyrażenia asercji niezbędnych do wykorzystania odpowiednich reguł dowodzenia. Zauważmy jednak, że w arytmetyce liczb całkowitych każdy skończony ciąg (i każdy skończony ciąg skończonych wektorów liczb całkowitych) można zakodować jako pojedynczą liczbę. Pozwala to na wyrażenie jako formuł pierwszego rzędu wszelkich niezbędnych dla przeprowadzenia dowodu asercji, w tym kluczowych dla całkowitej poprawności stwierdzeń, określających liczbę wykonań ciała pętli niezbędnych do zakończenia jej obliczeń.
