Semantyka i weryfikacja programów (d. 1000-215bSWP) 1000-2M24SWP
Wykład obejmuje następujące zagadnienia:
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
Zajęcia laboratoryjne poświęcone są ilustracji wykorzystania tych metod w praktycznym projektowaniu i implementacji języków programowania i weryfikacji programów. Studenci będą mieli okazję stworzyć implementację własnego języka programowania. W ramach zajęć, w niewielkich zespołach będą realizowane projekty obejmujące opis takiego języka programowania, definicję jego semantyki i bazującą na semantyce implementację interpretera. Te działania zostaną uzupełnione dalej praktycznymi przykładami weryfikacji programów przy wykorzystaniu narzędzi wspomagających dowodzenie.
Rodzaj przedmiotu
Założenia (lista przedmiotów)
Koordynatorzy przedmiotu
Efekty kształcenia
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 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).
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;
- możliwości wykorzystania semantyki jako bazy dla implementacji systemów oprogramowania;
- pojęcie poprawności programu względem formalnej specyfikacji;
- metody formalne dowodzenia częściowej i całkowitej poprawności prostych programów oraz ich praktyczne stosowanie przy wykorzystaniu narzędzi wspomagających.
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).
Kryteria oceniania
Ocena końcowa na podstawie egzaminu i zaliczenia projektów realizowanych w ramach laboratorium w ciągu semestru.
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. K. R. Apt, Ten Years of Hoare’s Logic: A Survey — Part 1, ACM Toplas 3(4), 1981, 431-483.
6. E. Dijkstra. Umiejętność programowania. WNT, 1978.
Więcej informacji
Więcej informacji o poziomie przedmiotu, roku studiów (i/lub semestrze) w którym się odbywa, o rodzaju i liczbie godzin zajęć - szukaj w planach studiów odpowiednich programów. Ten przedmiot jest związany z programami:
Dodatkowe informacje (np. o kalendarzu rejestracji, prowadzących zajęcia, lokalizacji i terminach zajęć) mogą być dostępne w serwisie USOSweb: