Semantyka i weryfikacja programów

informatyka techniczna i telekomunikacja

zaawansowany

Wyklad: I2_W01, I2_W05; laboratorium: I2_U01, I2_U02, I2_U04, I2_U08, I2_K05

Znajomość podstaw logiki matematycznej, matematyki dyskretnej oraz programowania.

Przedmiot ma za zadanie zapoznanie studentów z:

- metodami formalnego określania semantyk wykonań algorytmów (programów),

- modelowania formalnego ich własności,

- badania tychże własności w oparciu o modele formalne.

W ramach przedmiotu studenci zostaną zapoznani z metodami formalnego opisu wykonań algorytmów (programów). Przedstawione zostaną semantyki naturalne, denotacyjne i operacyjne. Bazą do tych rozważań będzie wprowadzenie do teorii automatów, języków formalnych i obliczeń. Studenci zapoznają się z podstawowymi strukturami i algorytmami tej teorii. Przedstawiona zostanie hierarchia Chomsky'ego. Na odpowiednich przykładach zostaną zaprezentowane własności algorytmów (programów) oraz metody ich weryfjikacji.

1. J. Hopcroft, J. Ullman, Wprowadzenie do teorii automatów, języków i obliczeń, PWN, Warszawa 2003.

2. J. Hopcroft, R. Motwani, J. Ullman, Wprowadzenie do teorii automatów, języków i obliczeń, PWN, Warszawa 2005.

3. A. Kościelski, Teoria obliczeń, wyd. UWr, Wrocław 1997.

Wyklad

W1 - Student zna i rozumie teoretyczne podstawy badania semantyk oprogramowania

W2 - Student zna i rozumie metody weryfikacji semantyki programów, a także pojęcia poprawności programów oraz techniki i formalizmy dla ich dowodzenia

K1 - Student jest gotów do identyfikacji ograniczeń własnej wiedzy i do ustawicznego samokształcenia

Laboratorium

U1 - Student potrafi stosować matematyczne metody analizy algorytmów i procesów

U2 - Student potrafi stosować wiedzę matematyczną i techniczną do formułowania, analizowania i rozwiązywania zadań związanych z informatyką

U3 - Student potrafi posługiwać się semantyką formalną przy wnioskowaniu o poprawności programów

U4 - Student potrafi określić kierunki dalszego uczenia się i realizować proces samokształcenia

K2 - Student jest gotowy do myślenia i działania w sposób kreatywny i przedsiębiorczy

Dla wszystkich efektów przyjmuje się następujące kryteria oceny we wszystkich formach weryfikacji:

ocena 5: osiągnięty w pełni (bez uchwytnych niedociągnięć),

ocena 4,5: osiągnięty niemal w pełni i nie są spełnione kryteria przyznania wyższej oceny,

ocena 4: osiągnięty w znacznym stopniu i nie są spełnione kryteria przyznania wyższej oceny,

ocena 3,5: osiągnięty w znacznym stopniu – z wyraźną przewagą pozytywów – i nie są spełnione kryteria przyznania wyższej oceny,

ocena 3: osiągnięty dla większości przypadków objętych weryfikacją i nie są spełnione kryteria przyznania wyższej oceny,

ocena 2: nie został osiągnięty dla większości przypadków objętych weryfikacją.

obowiązkowy

nie dotyczy

E-Learning (pełny kurs) z podziałem na grupy

obowiązkowy

nie dotyczy

Przedmiot ma za zadanie zaoznanie studentów z:

- metodami formalnego określania semantyk wykonań algorytmów (programów),

- modelowania formalnego ich własności,

- badania tychże własności w oparciu o modele formalne.

W ramach przedmiotu studenci zostaną zapoznani z metodami formalnego opisu wykonań algorytmów (programów). Przedstawione zostaną semantyki naturalne, denotacyjne i operacyjne. Bazą do tych rozważań będzie wprowadzenie do teorii automatów, języków formalnych i obliczeń. Studenci zapoanzją się z podstawowymi struktorami i algorytmami tej teorii. Przedstawiona zostanie hierarchia Chomsky'ego. Na odpowiednich przykładach zostaną zaprezentowane własności algorytmó (programów) oraz metody ich weryfjikacji.

1. J. Hopcroft, J. Ullman, Wprowadzenie do teorii automatów, języków i obliczeń, PWN, Warszawa 2003.

2. J. Hopcroft, R. Motwani, J. Ullman, Wprowadzenie do teorii automatów, języków i obliczeń, PWN, Warszawa 2005.

3. A. Kościelski, Teoria obliczeń, wyd. UWr, Wrocław 1997.

Podstawowa wiedza z Logiki matematycznej

E-Learning (pełny kurs) z podziałem na grupy

obowiązkowy

nie dotyczy

E-Learning (pełny kurs) z podziałem na grupy

WYKŁAD

Szacunkowy nakład pracy studenta:

- uczestnictwo w zajęciach 30 h,

- uczestnictwo w egzaminie 1 h,

- konsultacje z prowadzącym 2 h,

- przygotowanie do zajęć 5 h,

- przygotowanie do egzaminu 14 h,

razem 52 h, co odpowiada 2 ECTS.

LABORATORIA

Szacunkowy nakład pracy studenta:

- uczestnictwo w zajęciach 30 h,

- konsultacje z prowadzącym 3 h,

- prace domowe 30 h,

- przygotowanie do weryfikacji 15 h,

razem 78 h, co odpowiada 3 ECTS.

obowiązkowy

nie dotyczy

Przedmiot ma za zadanie zapoznanie studentów z:

- metodami formalnego określania semantyk wykonań algorytmów (programów),

- modelowania formalnego ich własności,

- badania tychże własności w oparciu o modele formalne.

W ramach przedmiotu studenci zostaną zapoznani z metodami formalnego opisu wykonań algorytmów (programów). Przedstawione zostaną semantyki naturalne, denotacyjne i operacyjne. Bazą do tych rozważań będzie wprowadzenie do teorii automatów, języków formalnych i obliczeń. Studenci zapoznają się z podstawowymi strukturami i algorytmami tej teorii. Przedstawiona zostanie hierarchia Chomsky'ego. Na odpowiednich przykładach zostaną zaprezentowane własności algorytmów (programów) oraz metody ich weryfjikacji.

1. J. Hopcroft, J. Ullman, Wprowadzenie do teorii automatów, języków i obliczeń, PWN, Warszawa 2003.

2. J. Hopcroft, R. Motwani, J. Ullman, Wprowadzenie do teorii automatów, języków i obliczeń, PWN, Warszawa 2005.

3. A. Kościelski, Teoria obliczeń, wyd. UWr, Wrocław 1997.