SW wykład 1 - Slajd16: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 8: | Linia 8: | ||
zdefiniować, kiedy zachodzą dotyczące tych program warunki | zdefiniować, kiedy zachodzą dotyczące tych program warunki | ||
poprawności. Dalej możemy już opracować reguły dowodzenia tych | poprawności. Dalej możemy już opracować reguły dowodzenia tych | ||
warunków i w oparciu o ich semantykę | warunków i w oparciu o ich semantykę przeprowadzić dowód poprawności | ||
tych reguł. W ten sposób wykażemy poprawność systemu dowodzenia | tych reguł. W ten sposób wykażemy poprawność systemu dowodzenia | ||
poprawności: każdy warunek poprawności programu, który potrafimy | poprawności: każdy warunek poprawności programu, który potrafimy | ||
| Linia 14: | Linia 14: | ||
precyzyjnie przez semantykę). Pozostaje jeszcze analiza pełności | precyzyjnie przez semantykę). Pozostaje jeszcze analiza pełności | ||
proponowanego systemu: czy wszystkie semantycznie prawdziwe warunki | proponowanego systemu: czy wszystkie semantycznie prawdziwe warunki | ||
poprawności można udowodnić? Na ogół jednak proponowane | poprawności można udowodnić? Na ogół jednak proponowane w tak | ||
absolutny sposób nie będą pełne: wtedy można pokazać przynajmniej | absolutny sposób systemy nie będą pełne: wtedy można pokazać przynajmniej | ||
jakieś ograniczone wersje pełności, by przynajmniej przekonać się, że | jakieś ograniczone wersje pełności, by przynajmniej przekonać się, że | ||
nie pominęliśmy możliwości (i potrzeby) dowodzenia poprawności | nie pominęliśmy możliwości (i potrzeby) dowodzenia poprawności jakichś | ||
ważnych klas programów. | ważnych klas programów. | ||
Aktualna wersja na dzień 09:58, 27 wrz 2006
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 w tak absolutny sposób systemy 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 jakichś ważnych klas programów.
