Nazwa przykładowego przedmiotu: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
 
Linia 1: Linia 1:
(forma zajęć: wykład + ćwiczenia, wykład+laboratorium, wykład, laboratorium)
(forma zajęć: wykład + ćwiczenia, wykład+laboratorium, wykład, laboratorium)


== Krótki opis ==
== Opis ==


treść opisu
treść opisu

Aktualna wersja na dzień 16:55, 8 cze 2006

(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