Semantyka i weryfikacja programów WM-I-SWP

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.

Dyscyplina naukowa, do której odnoszą się efekty uczenia się

informatyka techniczna i telekomunikacja

E-Learning

W cyklu 2021/22_Z:

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

W cyklu 2024/25_Z:

E-Learning

W cyklu 2023/24_Z:

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

W cyklu 2022/23_Z:

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

W cyklu 2020/21_Z:

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

Grupa przedmiotów ogólnouczenianych

nie dotyczy

Opis nakładu pracy studenta w ECTS

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.

Poziom przedmiotu

zaawansowany

Symbol/Symbole kierunkowe efektów uczenia się

Wykład: I2_W01, I2_W05; laboratoria: I2_U01, I2_U02, I2_U04, I2_U08, I2_K05

Typ przedmiotu

obowiązkowy

Wymagania wstępne

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

Koordynatorzy przedmiotu

W cyklu 2023/24_Z:

Dorota Dąbrowska
William Steingartner

W cyklu 2019/20_Z:

W cyklu 2021/22_Z:

W cyklu 2020/21_Z:

W cyklu 2022/23_Z:

W cyklu 2024/25_Z:

Efekty kształcenia

WYKŁAD
Student:
W1 - zna i rozumie podstawy teorii języków formalnych i automatów wraz z zastosowaniami (I2_W01),
W2 - zna i rozumie różne rodzaje semantyk programów oraz metody weryfikacji własności programów (I2_W05),
W3 - zna i rozumie pojęcia związane z poprawnością programów oraz wybrane techniki i formalizmy dowodzenia poprawności algorytmów i programów (I2_W05).
LABORATORIA
Student:
U1 - potrafi stosować wybrane metody matematyczne do analizy poprawności algorytmów (I2_U01),
U2 - potrafi budować maszyny abstrakcyjne i analizować ich działanie (I2_U02),
U3 - potrafi posługiwać się różnymi rodzajami semantyk formalnych do wnioskowania o własnościach programów (I2_U04),
U4 - potrafi samodzielnie uczyć się (I2_U08),
K1 - jest gotów do aktywnego udziału w laboratorium oraz kreatywnego rozwiązywania postawionych problemów (I2_K05).

Kryteria oceniania

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

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:

Informatyka - studia II stopnia stacjonarne

Dodatkowe informacje (np. o kalendarzu rejestracji, prowadzących zajęcia, lokalizacji i terminach zajęć) mogą być dostępne w serwisie USOSweb:

Strona przedmiotu WM-I-SWP w USOSweb