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

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 2024/25 będą stopniowo oznaczane planowaną lub zrealizowaną datą wykładu.
- Wstęp (2/10)
- Semantyka operacyjna (7,14/10)
- Semantyka denotacyjna (14,21/10)
- Deklaracje i bloki (28/10)
- Kontynuacje (4/11)
- Logika Hoare'a (18/11)
- Całkowita poprawność (25/11)
  - Notatka o dowodzeniu własności stopu pętli while
- Punkty stałe i teoria dziedzin (2/12)
- Metody dowodzenia formalnych własności języków (9/12)
- Podstawowe pojęcia algebry uniwersalnej (16/12, 9/01)
- Logika Hoare'a raz jeszcze
- Specyfikacje i systematyczne konstruowanie programów
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)
Ocena końcowa: na podstawie ważonych wyników laboratorium i egzaminu

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ń.