SW wykład 12 - Slajd6

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

Podobnie jak dla logiki Hoare'a stwierdzeń o częściowej poprawności, przedstawimy teraz system dowodzenia dla stwierdzeń całkowitej poprawności instrukcji języka TINY względem warunków wstępnego i końcowego. Zacznijmy od reguł, które choć formalnie mówią o innych stwierdzeniach, tak naprawdę są odziedziczone z systemu dowodzenia dla logiki Hoare'a. Dotyczy to wszystkich reguł poza regułą dla instrukcji pętli, jako jedyną tu konstrukcją językową, która może wprowadzić niebezpieczeństwo nieskończonych obliczeń.

Zauważmy raz jeszcze, że powyższe reguły należałoby nieco zmodyfikować, gdyby trzeba było uwzględniać możliwość pojawienia się błędów przy wyliczaniu wartości wyrażeń arytmetycznych lub logicznych.