Nazwa przykładowego przedmiotu

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

(forma zajęć: wykład + ćwiczenia, wykład+laboratorium, wykład, laboratorium)

Opis

treść opisu

Sylabus

Autor sylabusa

prof. dr hab. Andrzej Tarlecki tarlecki@mimuw.edu.pl

Nazwa zajęć:

Semantyka i weryfikacja programów

Typ zajęć:

wykład (30 godz.) + ćwiczenia (30 godz.)


Wymagania wstępne:

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

Sylabus:

  • 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

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.

Moduły

Literatura uzupełniająca

  1. Pozycja pierwsza
  2. Pozycja druga

Autorzy opracowania

  1. Autor pierwszy
  2. Autor drugi
Źródło: „https://wazniak.mimuw.edu.pl/index.php?title=Nazwa_przykładowego_przedmiotu&oldid=1448”