Uniwersytet Warszawski - Centralny System Uwierzytelniania
Strona główna

Semantyka i weryfikacja programów

Informacje ogólne

Kod przedmiotu: 1000-215bSWP
Kod Erasmus / ISCED: 11.303 Kod klasyfikacyjny przedmiotu składa się z trzech do pięciu cyfr, przy czym trzy pierwsze oznaczają klasyfikację dziedziny wg. Listy kodów dziedzin obowiązującej w programie Socrates/Erasmus, czwarta (dotąd na ogół 0) – ewentualne uszczegółowienie informacji o dyscyplinie, piąta – stopień zaawansowania przedmiotu ustalony na podstawie roku studiów, dla którego przedmiot jest przeznaczony. / (0612) Database and network design and administration Kod ISCED - Międzynarodowa Standardowa Klasyfikacja Kształcenia (International Standard Classification of Education) została opracowana przez UNESCO.
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 Podstawowe informacje o zasadach przyporządkowania punktów ECTS:
  • roczny wymiar godzinowy nakładu pracy studenta konieczny do osiągnięcia zakładanych efektów uczenia się dla danego etapu studiów wynosi 1500-1800 h, co odpowiada 60 ECTS;
  • tygodniowy wymiar godzinowy nakładu pracy studenta wynosi 45 h;
  • 1 punkt ECTS odpowiada 25-30 godzinom pracy studenta potrzebnej do osiągnięcia zakładanych efektów uczenia się;
  • tygodniowy nakład pracy studenta konieczny do osiągnięcia zakładanych efektów uczenia się pozwala uzyskać 1,5 ECTS;
  • nakład pracy potrzebny do zaliczenia przedmiotu, któremu przypisano 3 ECTS, stanowi 10% semestralnego obciążenia studenta.

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 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. H. Riis Nielson, F. Nielson. Semantics with Applications: An Appetizer. Springer, 2007.

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

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

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

Efekty uczenia się:

Wiedza. Student zna i rozumie:

* 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 pojecia poprawnosci programow 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).

W bardziej szczegółowym ujęciu student zna:

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

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

- pojęcie poprawności programu względem formalnej specyfikacji;

- metody formalne dowodzenia częściowej i całkowitej poprawności prostych programów.

Umiejętności. Student 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. Student jest gotów:

* do krytycznej oceny posiadanej wiedzy i odbieranych treści (K_K01);

* 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:

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

Zajęcia w cyklu "Semestr zimowy 2023/24" (zakończony)

Okres: 2023-10-01 - 2024-01-28
Wybrany podział planu:
Przejdź do planu
Typ zajęć:
Ćwiczenia, 30 godzin więcej informacji
Wykład, 30 godzin więcej informacji
Koordynatorzy: Andrzej Tarlecki
Prowadzący grup: Ewa Madalińska-Bugaj, Aleksy Schubert, Michał Skrzypczak, Andrzej Tarlecki
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.
ul. Banacha 2
02-097 Warszawa
tel: +48 22 55 44 214 https://www.mimuw.edu.pl/
kontakt deklaracja dostępności USOSweb 7.0.3.0-2b06adb1e (2024-03-27)