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:

Najważniejsze problemy i techniki formalizacji opisu programów. Metody definiowania semantyki programów, z ich

matematycznymi podstawami i praktycznymi technikami. Pojęcia poprawności programów oraz techniki i formalizmy

dla ich dowodzenia. Najważniejsze idee systematycznego konstruowania poprawnych programów.

Pełny opis:

1. Analiza składniowa programów ze szczególnym uwzględnieniem składni abstrakcyjnej i konfliktów przy parsowaniu

2. Formalny opis języków programowania

3. Operacyjne i denotacyjne metody definiowania semantyki programów

4. Semantyczne definicje podstawowych konstrukcji programistycznych

5. Matematyczne podstawy semantyki denotacyjnej

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

7. Metody dowodzenia poprawności programów

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

9. 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. P. Dembiński, J. Manuszyński. Matematyczne metody definiowania języków programowania. WNT, 1981.

2. E. Dijkstra. Umiejętność programowania. WNT, 1978.

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

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

Efekty uczenia się:

Wiedza: absolwent zna i rozumie

* ma uporządkowaną, podbudowaną teoretycznie wiedzę ogólną w zakresie programowania, algorytmów i złożoności,

architektury systemów komputerowych, systemów operacyjnych, technologii sieciowych, języków i paradygmatów

programowania, baz danych, inżynierii oprogramowania [K_W02],

* w zaawansowanym stopniu podstawowe konstrukcje programistyczne (przypisanie, instrukcje sterujące,

wywoływanie podprogramów i przekazywanie parametrów) oraz pojęcia składni i semantyki języków programowania

[K_W03],

* metody definiowania semantyki programów, z ich matematycznymi podstawami i praktycznymi technikami, a także

pojęcia poprawności programów oraz techniki i formalizmy dla ich dowodzenia [K_W13],

* podstawy teorii języków formalnych (języki, wyrażenia regularne, gramatyki) i formalnych modeli obliczeniowych

(automaty, automaty ze stosem, maszyny Turinga) [K_W16].

Umiejętności: absolwent potrafi

* pozyskiwać informacje z literatury, baz wiedzy, Internetu oraz innych wiarygodnych źródeł, integrować je,

dokonywać ich interpretacji oraz wyciągać wnioski i formułować opinie [K_U02],

* zrozumieć opis semantyki języka; posługuje się semantyką formalną przy wnioskowaniu o poprawności programów

[K_U03],

* samodzielnie planować i realizować własne uczenie się przez całe życie [K_U09],

Kompetencje społeczne: absolwent jest gotów do

* uznawania znaczenia wiedzy w rozwiązywaniu problemów poznawczych i praktycznych oraz wyszukiwania

informacji w literaturze oraz zasięgania opinii ekspertów [K_K03]

Metody i kryteria oceniania:

Zaliczenie ćwiczeń na podstawie prac domowych: z trzech prac, ocenianych na skali [0,1] dla zaliczenia niezbędne jest uzyskanie 1.8 pkt.

Zaliczenie ćwiczeń jest warunkiem dopuszczenia do egzaminu w I terminie. Do egzaminu w II terminie dopuszczeni są wszyscy uprawnieni do zaliczania przedmiotu.

Egzamin ma formę pisemną, składa się z 3 zadań, punktowanych na skali [0-10]. Do zaliczenia na ocenę dostateczną wystarczy 15 pkt, ale próg ten może być obniżany w zależności od trudności zadań.

Zajęcia w cyklu "Semestr zimowy 2019/20" (zakończony)

Okres: 2019-10-01 - 2020-01-27
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, Grzegorz Grudziński, Bartosz Klin, Ewa Madalińska-Bugaj, Julian Salamanca Tellez, Michał Skrzypczak
Lista studentów: (nie masz dostępu)
Zaliczenie: Egzamin

Zajęcia w cyklu "Semestr zimowy 2020/21" (jeszcze nie rozpoczęty)

Okres: 2020-10-01 - 2021-01-27
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, Marcin Engel, 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.