Semantyka i weryfikacja programów 1000-215bSWP
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)
Rodzaj przedmiotu
Tryb prowadzenia
Wymagania (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 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).
Kryteria oceniania
Ocena końcowa na podstawie egzaminu i prac domowych zadawanych 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. D. Gries. The Science of Programming. Springer-Verlag, 1981.
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: