Course at
Faculty of Mathematics, Informatics and Mechnics
The University of Warsaw

Program Semantics and Verification


Sorry, no English version...

Semantyka i weryfikacja programów

UWAGA: zmieniony format zajęć w roku 2024/25!

wykład i laboratorium w roku akademickim 2024/25, semestr zimowy


Egzamin odbył się -- wyniki już zatwierdzone w USOSie, zadania poniżej.

Dla zainteresowanych, termin egzaminu poprawkowego:
środa, 19 lutego 2025, godz. 10.00, sala 3230



Celem przedmiotu jest przedstawienie znaczenia, a także podstawowych problemów, technik i zastosowań formalnego opisywania programów. Wykład omawia różne metody definiowania semantyki programów, ich niezbędne podstawy i techniki matematyczne oraz wprowadza podstawowe pojęcia poprawności programów wraz metodami i formalizmami jej dowodzenia. Zajęcia laboratoryjne ilustrują wykorzystanie tych metod w praktyce projektowej i programistycznej.

Tematy wykładów: Zajęcia laboratoryjne: poświęcone będą ilustracji wykorzystania tych metod w praktycznym projektowaniu i implementacji języków programowania i weryfikacji programów. Studenci będą mieli okazję stworzyć implementację własnego języka programowania. W ramach zajęć, w niewielkich zespołach będą realizowane projekty obejmujące opis prostego języka programowania, definicję jego semantyki i bazującą na semantyce implementację interpretera. Te działania zostaną uzupełnione dalej praktycznymi przykładami weryfikacji programów przy wykorzystaniu narzędzi wspomagających dowodzenie.

Materialy do wykladu:


Warunki zaliczenia i egzaminu


Przykładowe zadania z lat ubiegłych

DISCLAIMER: zadania są tu umieszczane w formie i postaci oryginalnej. Zwracam uwagę, że notacja i wymagania dotyczące rozwiązań mogły się w czasie zmieniać; udostepniając tutaj zadania (i niekiedy proponowane wówczas rozwiązania) nie ponoszę odpowiedzialności za możliwe niedokładności (czy wręcz błedy) w rozwiązaniach i za rozbieżnosci z obecnymi kryteriami ocen podobnych zadań.


Może jeszcze coś tu się pojawi...


AT