Semantyka i weryfikacja programów

Z Studia Informatyczne
Wersja z dnia 16:50, 8 cze 2006 autorstwa 10.1.2.43 (dyskusja)
(różn.) ← poprzednia wersja | przejdź do aktualnej wersji (różn.) | następna wersja → (różn.)
Przejdź do nawigacjiPrzejdź do wyszukiwania

== Autor sylabusa prof. dr hab. Andrzej Tarlecki

==Typ zajęć wykład (30 godz.) + ćwiczenia (30 godz.)

== Wymagania wstępne

  • Wstęp do programowania
  • Wstęp do teorii mnogości i logiki

== Zawartość

  • Formalny opis języków programowania
  • Operacyjne i denotacyjne metody definiowania semantyki programów
  • Semantyczne definicje podstawowych konstrukcji programistycznych
  • Matematyczne podstawy semantyki denotacyjnej
  • Pojęcia poprawności programów: poprawność częściowa i całkowita
  • Metody dowodzenia poprawności programów
  • Logika Hoare'a, jej wykorzystanie i własności formalne
  • Systematyczne konstruowanie poprawnych programów

Zalecana literatura

  1. P. Dembiński, J. Mańuszynski. Matematyczne metody definiowania języków programowania. WNT, 1981.
  2. M. Gordon. Denotacyjny opis języków programowania. WNT, 1983.
  3. D. Gries. The Science of Programming. Springer-Verlag, 1981.
  4. E. Dijkstra. Umiejętność programowania. WNT, 1978.