Metody formalne w informatyce - zajęcia fakultatywne WM-MA-S1-MFI
Przedmiot przedstawia wybrane metody formalne stosowane w informatyce oraz ich matematyczne podstawy. Obejmuje różne modele obliczeń, w tym automaty, maszyny Turinga i funkcje rekurencyjne, rachunek lambda i rachunek termów, podstawowe zagadnienia teorii typów oraz wybrane systemy logiczne. Omawiane są również związki tych formalizmów z językami programowania i sposobami reprezentowania obliczeń.
W ramach kursu przedstawiane są metody formalnego opisu zachowania programów, specyfikowania ich własności oraz rozumowania o ich poprawności. Uzupełnieniem są wybrane modele współbieżności oraz podstawowe idee teorii kategorii i przykłady ich zastosowania w informatyce.
Celem przedmiotu jest zapoznanie studentów z różnymi sposobami matematycznego i formalnego modelowania obliczeń oraz rozwinięcie umiejętności doboru i stosowania wybranych metod formalnych do analizy problemów informatycznych.
Dyscyplina naukowa, do której odnoszą się efekty uczenia się
E-Learning
Grupa przedmiotów ogólnouczenianych
Koordynatorzy przedmiotu
Opis nakładu pracy studenta w ECTS
Poziom przedmiotu
Symbol/Symbole kierunkowe efektów uczenia się
Typ przedmiotu
Wymagania wstępne
Efekty uczenia się
WYKŁAD
Student:
W1 – charakteryzuje matematyczne podstawy wybranych formalnych modeli obliczeń oraz ich znaczenie i zastosowanie w informatyce (MA1_W01, MA1_W04),
W2 – opisuje podstawowe własności wybranych formalizmów logicznych, rachunków i systemów typów stosowanych do reprezentowania i analizowania obliczeń (MA1_W04),
W3 – opisuje zastosowanie metod matematycznych do formalnego opisu zachowania programów, specyfikowania ich własności oraz rozumowania o ich poprawności (MA1_W01, MA1_W04).
LABORATORIUM
Student:
K1 – identyfikuje ograniczenia własnej wiedzy i samodzielnie ją rozwija w zakresie formalnych i matematycznych podstaw informatyki (MA1_K01),
K2 – formułuje pytania, wyraża opinie oraz identyfikuje brakujące elementów rozumowania podczas analizy formalnych modeli, własności programów i procesów obliczeniowych (MA1_K02, 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: