Metody formalne w informatyce - zajecia specjalnościowe WM-I-S1-E5-MFI
Przedmiot wprowadza w podstawowe metody formalne w informatyce: automaty, maszyny Turinga, funkcje rekurencyjne, rachunek lambda i rachunek termów. Obejmuje także wprowadzenie do semantyki języków programowania w różnych ujęciach (denotacyjnym, algebraicznym, aksjomatycznym), modele logiczne i współbieżne oraz wybrane zastosowania teorii kategorii. Celem kursu jest rozwinięcie umiejętności formalnej analizy programów, dowodzenia ich własności i rozumienia modeli obliczeń.
Dyscyplina naukowa, do której odnoszą się efekty uczenia się
E-Learning
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 2021/22_Z: E-Learning (pełny kurs) z podziałem na grupy |
Grupa przedmiotów ogólnouczenianych
Opis nakładu pracy studenta w ECTS
W cyklu 2023/24_Z: Wykład
udział w zajęciach, 30h
nauka własna zagadnień z wykładu, 20h,
studia nad literaturą, 25h,
suma: 75h (3 p. ECTS)
Laboratoria
udział w zajęciach, 30h,
nauka własna, 20h,
przygotowanie projektów informatycznych, 30h
Suma: 80h (3 p. ECTS) | W cyklu 2022/23_Z: Wykład
udział w zajęciach, 30h
nauka własna zagadnień z wykładu, 20h,
studia nad literaturą, 25h,
Suma: 75h (3 p. ECTS),
Laboratoria
udział w zajęciach, 30h,
nauka własna, 20h,
przygotowanie projektów informatycznych, 30h
Suma: 80h (3 p. ECTS) | W cyklu 2025/26_Z: Wykład
udział w zajęciach, 30h
nauka własna zagadnień z wykładu, 20h,
studia nad literaturą, 25h,
suma: 75h (3 p. ECTS)
Laboratoria
udział w zajęciach, 30h,
nauka własna, 20h,
przygotowanie projektów informatycznych, 25h
Suma: 75h (3 p. ECTS) |
Poziom przedmiotu
Symbol/Symbole kierunkowe efektów uczenia się
Typ przedmiotu
W cyklu 2023/24_Z: fakultatywny ograniczonego wyboru | W cyklu 2024/25_Z: obowiązkowy | W cyklu 2025/26_Z: fakultatywny ograniczonego wyboru | W cyklu 2022/23_Z: fakultatywny ograniczonego wyboru |
Wymagania wstępne
Koordynatorzy przedmiotu
W cyklu 2021/22_Z: | W cyklu 2023/24_Z: | W cyklu 2024/25_Z: | W cyklu 2025/26_Z: | W cyklu 2022/23_Z: |
Efekty kształcenia
Wykład:
W1 - student zna zasady formalizacji własności programów oraz rozumie ich semantykę (I1_W14),
U1 - student zna programy ułatwiające weryfikację oprogramowania oraz teorie formalne, na których się opierają (I1_U18),
Laboratoria:
W1 - student zna narzędzia informatyczne służące do automatycznej weryfikacji programów (I1_W14),
U1 - student potrafi wykorzystać wybrane narzędzia informatyczne, aby udowodnić poprawność zaprogramowanych funkcji (I1_U18)
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
Dodatkowe informacje (np. o kalendarzu rejestracji, prowadzących zajęcia, lokalizacji i terminach zajęć) mogą być dostępne w serwisie USOSweb: