Semantyka i weryfikacja programów

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)

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