SW wykład 1 - Slajd16

<<powrót do strony wykładu

Wstęp Literatura Programy Programy, sprzeczne oczekiwania WielkiCel Składnia Semantyka Pragmatyka Logika Metodyka Implementacja Formalna semantyka Przykład Przykład, c.d. Przykład, reguła dowodzenia Uzasadnianie poprawności Plan zajęć

Budowę w pełni wiarygodnych metod rozumowania o programach i dowodzenia ich własności rozpocząć musimy od zdefiniowania semantyki rozważanych programów. Podobnie dla warunków poprawności tych programów: wykorzystując semantykę programów, należy formalnie zdefiniować, kiedy zachodzą dotyczące tych program warunki poprawności. Dalej możemy już opracować reguły dowodzenia tych warunków i w oparciu o ich semantykę, przeprowadzić dowód poprawności tych reguł. W ten sposób wykażemy poprawność systemu dowodzenia poprawności: każdy warunek poprawności programu, który potrafimy udowodnić, rzeczywiście będzie zachodził (w sensie określonym precyzyjnie przez semantykę). Pozostaje jeszcze analiza pełności proponowanego systemu: czy wszystkie semantycznie prawdziwe warunki poprawności można udowodnić? Na ogół jednak proponowane systemy w tak absolutny sposób nie będą pełne: wtedy można pokazać przynajmniej jakieś ograniczone wersje pełności, by przynajmniej przekonać się, że nie pominęliśmy możliwości (i potrzeby) dowodzenia poprawności jakiś ważnych klas programów.