Metody formalne w informatyce-zajęcia fakultatywne WM-MA-S1-E5-MFWI
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 2023/24_Z: E-Learning | W cyklu 2024/25_Z: E-Learning | W cyklu 2025/26_Z: E-Learning (pełny kurs) | W cyklu 2022/23_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: udział w zajęciach, 60h
nauka własna, 40h,
przygotowanie projektów informatycznych, 50h
w sumie 150h czyli 6ECTS | W cyklu 2022/23_Z: udział w zajęciach, 60h
nauka własna, 40h,
przygotowanie projektów informatycznych, 50h
w sumie 150h czyli 6ECTS | 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
Wymagania wstępne
Koordynatorzy przedmiotu
W cyklu 2024/25_Z: | W cyklu 2023/24_Z: | W cyklu 2025/26_Z: | W cyklu 2022/23_Z: |
Efekty kształcenia
Wykład
W1 - rozumie znaczenie metod formalnych w weryfikacji poprawności oprogramowania (MA1_W01),
W2 - zna podstawowe twierdzenia dotyczące semantyki języków programowania i logiki Hoare'a (MA1_W04).
Laboratoria
L1 - jest gotowy do rozwoju swojej wiedzy z dziedziny weryfikacji oprogramowania (MA1_K01),
L2 - jest gotowy do wykrywania brakujących elementów w formalizacji oprogramowania (MA1_K02),
L3 - jest gotowy do opiniowania poprawności formalizacji oprogramowania (MA1_K07).
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: