Semantyka i weryfikacja programów (d. 1000-215bSWP)

fakultatywne

Języki, automaty i obliczenia 1000-214bJAO
Podstawy matematyki 1000-211bPM
Wstęp do programowania 1000-211bWPI

Celem przedmiotu jest przedstawienie znaczenia, a także podstawowych problemów, technik i zastosowań formalnego opisywania programów. Wykład omawia różne metody definiowania semantyki programów, ich niezbędne podstawy i techniki matematyczne oraz wprowadza podstawowe pojęcia poprawności programów wraz metodami i formalizmami jej dowodzenia. Zajęcia laboratoryjne ilustrują wykorzystanie tych metod w praktyce projektowej i programistycznej.

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.

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.

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).

Ocena końcowa na podstawie egzaminu i zaliczenia projektów realizowanych w ramach laboratorium w ciągu semestru.