SW wykład 12 - Slajd1
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
Na poprzednich dwóch wykładach wprowadziliśmy i analizowaliśmy logikę Hoare'a: logikę stwierdzeń o częściowej poprawności programów najprostszej wersji języka TINY względem ich specyfikacji danych jako para warunków (wstępnego i końcowego) wyrażonych formułami logiki pierwszego rzędu. Specyfikacje te traktowaliśmy jako część stwierdzeń o częściowej poprawności programów, gdzie naszym zadaniem było pokazanie tej własności (częściowej poprawności właśnie) dla danego programu. Innymi słowy, omawialiśmy problem weryfikacji programu względem jego specyfikacji i przedstawiliśmy system dowodzenia dla odpowiednich stwierdzeń poprawności.
Na specyfikacje, także na specyfikacje postaci danej dla logiki Hoare'a, można też patrzeć nieco inaczej: jako na sformułowanie zadania programistycznego "zbuduj program, który jest poprawny względem zadanej specyfikacji". Spróbujmy tak właśnie przeczytać specyfikację daną parą warunków (wstępnego i końcowego). Specyfikacja taka opisuje zadanie programistyczne: zbuduj program (naszego języka TINY), który jest częściowo poprawny względem zadanych warunków wstępnego i końcowego. Oczywiście, nie definiuje to programu jednoznacznie: zadaniem programisty jest zbudowanie dowolnego takiego programu. Może się też zdarzyć, że zadanie to jest nierozwiązywalne: taki program może nie istnieć. Może się też zdarzyć, że nawet gdy takie programy istnieją, są one zbyt trudne do zbudowania (w jakimkolwiek sensie) i zadanie nie zostanie rozwiązane...
