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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
← poprzednia edycjanastępna edycja →
WizualnieWikikod
Linia 7: Linia 7:
== Sylabus ==
== Sylabus ==


bla: blablalizator ''rozproszony'' bla bla bla
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.)
 
Opis:
 
Celem wykładu jest pokazanie roli i najważniejszych problemów i technik formalizacji opisu programów. Omawiane będą metody definiowania semantyki programów, z ich matematycznymi podstawami i praktycznymi technikami. Wprowadzone zostaną pojęcia poprawności programów oraz techniki i formalizmy dla ich dowodzenia. Przedstawione też będą najważniejsze idee systematycznego konstruowania poprawnych program.
 
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:
 
* P. Dembiński, J. Mańuszynski. Matematyczne metody definiowania języków programowania. WNT, 1981.
* M. Gordon. Denotacyjny opis językęw programowania. WNT, 1983.
* D. Gries. The Science of Programming. Springer-Verlag, 1981.
* E. Dijkstra. Umiejętność programowania. WNT, 1978.


== Zalecana literatura ==
== Zalecana literatura ==

Wersja z 15:03, 8 cze 2006

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

Krótki 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.)

Opis:

Celem wykładu jest pokazanie roli i najważniejszych problemów i technik formalizacji opisu programów. Omawiane będą metody definiowania semantyki programów, z ich matematycznymi podstawami i praktycznymi technikami. Wprowadzone zostaną pojęcia poprawności programów oraz techniki i formalizmy dla ich dowodzenia. Przedstawione też będą najważniejsze idee systematycznego konstruowania poprawnych program.

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:

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

Zalecana literatura

  1. Pozycja pierwsza
  2. Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, Wprowadzenie do algorytmów,WNT 2004.

Moduły

Bibliografia

  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=1418”