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

wykład i laboratorium w roku akademickim 2025/26, semestr zimowy

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

mini-prezentacja zajęć
WoW 2025

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:

Formalny opis języków programowania
Operacyjne i denotacyjne metody definiowania semantyki programów
Semantyczne definicje podstawowych konstrukcji programistycznych
Matematyczne podstawy semantyki denotacyjnej
Pojęcia poprawności programów: poprawność częściowa i całkowita
Metody dowodzenia poprawności programów
Logika Hoare'a, jej wykorzystanie i własności formalne
Podstawowe pojęcia algebry uniwersalnej i ich rola w opisie języków programowania

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:

Przezrocza do wykładu:
Poniższe wersje przezroczy i ostateczna treść wykładu mogą być jeszcze (nieco) modyfikowane. Ostateczne wersje przezroczy wykorzystywane na wykładzie w roku 2025/26 będą stopniowo oznaczane planowaną lub zrealizowaną datą wykładu.
Przykładowa literatura:
- M. Fernandez. Programming Languages and Operational Semantics: An Introduction. College Publications, 2004.
- M. Hennessy. The Semantics of Programming Languages: An Elementary Introduction Using Structural Operational Semantics. Wiley, 1990.
- M. Gordon. Denotacyjny opis języków programowania. WNT, 1983.
- H. Riis Nielson, F. Nielson. Semantics with Applications: An Appetizer. Springer, 2007.
- K. R. Apt, Ten Years of Hoare’s Logic: A Survey — Part 1, ACM Toplas 3(4), 1981, 431-483.
- E. Dijkstra. Umiejętność programowania. WNT, 1978.

Warunki zaliczenia i egzaminu

Laboratorium: na podstawie projektów realizowanych w ciągu semestru.
Egzamin: pisemny, dwa zadania, w stylu podobnym do lat ubiegłych (patrz poniżej).
Egzamin poprawkowy: zapewne teź moze okazać sie potrzebny, zasady jak dla egzaminu w I terminie.
Ocena końcowa bedzie ustalona na podstawie wyników laboratorium i egzaminu, odpowiednio ważonych według formuły max(LAB+0,5*EGZ,0,5*LAB+EGZ), gdzie LAB to punktowy wynik zaliczenia laboratorium (do 20pkt plus do 5 pkt za super-pomysły i opracowania), a EGZ -- egzaminu (do 10pkt za każde zadanie). Na ocenę pozytywną wystarczy 18pkt (o ewentualnym obniżeniu tego progu mogę zdecydować w zalezności od trudności zadań i wyników).

Przykładowe zadania z lat ubiegłych
- przykłady zadań z kilku ubiegłych lat.
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