SW wykład 12 - Slajd12

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

Algebrę pierwotnego typu danych (nad sygnaturą z predykatami, stałymi i operacjami arytmetycznymi) nazwiemy arytmetyczną, jeśli zbiór wartości interpretowanych w niej jako liczby naturalne (tzn., spełniających predykat $nat$) ze stałymi, operacjami i relacjami arytmetycznymi określonymi jak w tej algebrze tworzy standardowy model arytmetyki.

Przy założeniu, że algebra pierwotnego typu danych jest arytmetyczna, dowód poprawności reguł dowodzenia dla stwierdzeń całkowitej poprawności jest taki sam, jak dla podstawowej wersji języka. Każde stwierdzenie całkowitej poprawności instrukcji uogólnionego języka TINY względem warunków wstępnego i końcowego, które można pokazać w tym systemie reguł korzystając z formuł pierwszego rzędu prawdziwych w algebrze pierwotnego typu danych, jest prawdziwe w sensie semantycznym.

Jeżeli założymy ponadto, że w rozważanej algebrze pierwotnego typu danych, skończone ciągi elementów można zakodować jako pojedyncze elementy algebry, to system tych reguł dowodzenia jest relatywnie pełny: każde prawdziwe stwierdzenie całkowitej poprawności instrukcji uogólnionego 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 pierwotnego typu danych.