SW wykład 1 - Slajd7

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

Znając składnię programów, można już przystąpić do definiowania ich znaczenia --- formalnej, matematycznej semantyki. Trzeba tu podkreślić, że nawet najlepsze nieformalne przedstawienie konstrukcji programistycznych w języku naturalnym, choć niezwykle cenne dla wielu celów, musi okazać się niewystarczające, gdy niezbędna jest pełna precyzja i jasność, formalna analiza i brak jakichkolwiek wątpliwości dotyczących interpretacji tej czy innej konstrukcji językowej w takim czy innym złożonym kontekście.

Kolejne moduły tych zajęć omawiają dokładniej różne wersje operacyjnej i denotacyjnej metody definiowania semantyki programów. Oczywiście, nie zawsze niezbędne jest wykorzystanie jednej z tych metod. Na przykład, dla wielu celów (dowodzenie poprawności!) użyteczna może okazać się tzw. aksjomatyczna metoda definiowania semantyki, gdzie semantykę programów opisuje się nie wprost, lecz przez podanie własności, które spełniają poszczególne programy (na ogół z kolei, przez podanie szeregu elementarnych aksjomatów o prostych składowych programów i dalej, reguł wnioskowania o ich dalszych własnościach i o własnościach programów złożonych).