Uniwersytet Warszawski - Centralny System UwierzytelnianiaNie jesteś zalogowany | zaloguj się
katalog przedmiotów - pomoc

Semantyka i weryfikacja programów

Informacje ogólne

Kod przedmiotu: 1000-215bSWP Kod Erasmus / ISCED: 11.303 / (0612) Database and network design and administration
Nazwa przedmiotu: Semantyka i weryfikacja programów
Jednostka: Wydział Matematyki, Informatyki i Mechaniki
Grupy: Przedmioty obowiązkowe dla III roku informatyki
Przedmioty obowiązkowe dla III roku JSIM - wariant 3I+4M
Przedmioty obowiązkowe dla III roku JSIM - wariant 3M+4I
Strona przedmiotu: http://www.mimuw.edu.pl/~tarlecki/teaching/semwer/
Punkty ECTS i inne: 5.00
zobacz reguły punktacji
Język prowadzenia: polski
Rodzaj przedmiotu:

obowiązkowe

Wymagania (lista przedmiotów):

Języki, automaty i obliczenia 1000-214bJAO
Podstawy matematyki 1000-211bPM
Wstęp do programowania (podejście imperatywne) 1000-211bWPI

Tryb prowadzenia:

w sali

Skrócony opis:

Celem przedmiotu jest przedstawienie znaczenia, a także podstawowych problemów i technik formalnego opisywania programów. Omówione są różne metody definiowania semantyki programów, a także przedstawione są ich podstawy i techniki matematyczne. Wprowadza się podstawowe pojęcia poprawności programów wraz metodami i formalizmami jej dowodzenia.

Pełny opis:

1. Formalny opis języków programowania

2. Operacyjne i denotacyjne metody definiowania semantyki programów

3. Semantyczne definicje podstawowych konstrukcji programistycznych

4. Matematyczne podstawy semantyki denotacyjnej

5. Pojęcia poprawności programów: poprawność częściowa i całkowita

6. Metody dowodzenia poprawności programów

7. Logika Hoare'a, jej wykorzystanie i własności formalne

8. Podstawowe pojęcia algebry uniwersalnej i ich rola w opisie języków programowania

Wymagania wstępne:

- Wstęp do programowania (1000-211bWPI i/lub 1000-211bWPF)

- Podstawy matematyki (1000-211bPM)

- Języki, automaty i obliczenia (1000-214bJAO)

Literatura:

1. M. Hennessy. The Semantics of Programming Languages. Wiley, 1990.

2. M. Fernandez. Programming Languages and Operational Semantics: An Introduction. College Publications, 2004.

3. A. Blikle, P. Chrząstowski-Wachtel. Denotacyjna inżynieria języków programowania. preprint, 2019.

4. M. Gordon. Denotacyjny opis języków programowania. WNT, 1983.

5. D. Gries. The Science of Programming. Springer-Verlag, 1981.

Efekty uczenia się:

Wiedza. Student zna i rozumie:

- pojęcia składni i semantyki języków programowania, metody ich definiowania, a także definicje podstawowych konstrukcji programistycznych (K_W02, K_W03, K_W13);

- matematyczne podstawy i praktyczne techniki definiowania semantyki programów (K_W13);

- pojęcie poprawności programu względem formalnej specyfikacji (K_W02, K_W04, K_W13);

- metody formalne dowodzenia częściowej i całkowitej poprawności prostych programów (K_W04, K_W10, K_W13).

Umiejętności. Student potrafi:

- definiować semantykę prostych konstrukcji programistycznych, a także zrozumieć działanie konstrukcji programistycznych na podstawie ich opisów semantycznych (K_U01, K_U03);

- stosować metody formalnej weryfikacji do dowodzenia poprawmości prostych programów (K_U03, K_U07);

- uzasadnić poprawność programów odnosząc się do ich semantyki (K_U03).

Kompetencje. Student jest gotów:

- znać ograniczenia swojej wiedzy i rozumieć potrzebę dalszego kształcenia (K_K01);

- zrozumieć i docenić znaczenie precyzji i dokładności w formułowaniu problemów i uzasadnianiu poprawności rozwiązań (K_K03).

Metody i kryteria oceniania:

Ocena końcowa na podstawie egzaminu i prac domowych zadawanych w ciągu semestru.

Zajęcia w cyklu "Semestr zimowy 2020/21" (w trakcie)

Okres: 2020-10-01 - 2021-01-31
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Ćwiczenia, 30 godzin więcej informacji
Wykład, 30 godzin więcej informacji
Koordynatorzy: Bartosz Klin
Prowadzący grup: Lorenzo Clemente, Tomasz Gogacz, Grzegorz Grudziński, Bartosz Klin, Ewa Madalińska-Bugaj, Julian Salamanca Tellez
Lista studentów: (nie masz dostępu)
Zaliczenie: Egzamin
Opisy przedmiotów w USOS i USOSweb są chronione prawem autorskim.
Właścicielem praw autorskich jest Uniwersytet Warszawski.