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 w roku akademickim 2023/24, semestr zimowy
poniedziałki, godz. 14.15-16.00, sala 3180

Egzamin poprawkowy: 24 lutego 2024, godz. 14.00, sala 3180

Celem wykładu jest pokazanie roli i najważniejszych problemów i technik formalizacji opisu programów. Omawiane będą metody definiowania semantyki programów, z ich matematycznymi podstawami i praktycznymi technikami. Wprowadzone zostaną pojęcia poprawności programów oraz techniki i formalizmy dla ich dowodzenia. Przedstawione też będą najważniejsze idee systematycznego konstruowania poprawnych programów.

Materialy do wykladu:

Przezrocza do 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.
- D. Gries. The Science of Programming. Springer-Verlag, 1981.
- E. Dijkstra. Umiejętność programowania. WNT, 1978.
- P. Dembiński, J. Małuszyński. Matematyczne metody definiowania języków programowania. WNT, 1981.
- A. Blikle, P. Chrząstowski-Wachtel. Denotacyjna inżynieria języków programowania. preprint, 2019.

Warunki zaliczenia i egzaminu

Prace domowe: Zaliczenie ćwiczeń i dopuszczenie do egzaminu odbyło się na podstawie prac domowych. Były trzy prace domowe, każda złożona z jednego zadania, oceniane na skali 0-10. Zadania były wspólne dla wszystkich grup, ale sprawdzane i omawiane przez prowadzących poszczgólne grupy ćwiczeniowe.
- trzecie zadnie domowe (weryfikacja) -- i możliwe jego rozwiązanie
  Do przygotowania rozwiązania można było wykorzystać:
  - zad3dom2023program.txt tekst programu i/lub
  - zad3dom2023program.tex plik LaTeXowy z programem i miejscem na wpisanie asercji.
  Wątpliwości i pytania dotyczące tego zadania można było zgłaszać na adres tarlecki@mimuw.edu.pl po sprawdzeniu już widocznych pytań i odpowiedzi.
- drugie zadanie domowe (semantyka denotacyjna) ze szkicem rozwiązania
  Wątpliwości i pytania dotyczące tego zadania można było zgłaszać na adres tarlecki@mimuw.edu.pl po sprawdzeniu już widocznych pytań i odpowiedzi.
- pierwsze zadanie domowe (semantyka operacyjna) ze szkicem rozwiązania
  Wątpliwości i pytania dotyczące tego zadania można było zgłaszać na adres tarlecki@mimuw.edu.pl po sprawdzeniu już widocznych pytań i odpowiedzi.
Do zaliczenia ćwiczeń i dopuszczenia do pierwszego terminu egzaminu niezbędne było uzyskanie więcej niż 15 punktów z trzech prac domowych.
Egzamin: odbył się 2 lutego 2024, godz. 10.00-13.00(+ epsilon).
Były trzy zadania:
Ostateczne wyniki egzaminu są dostępne w USOSie.
Egzamin poprawkowy: odbędzie się w sobotę, 24 lutego 2024, o godz. 14.00, sala 3180. Do przystąpienia do egzaminu poprawkowego nie będzie wymagane zaliczenie ćwiczeń/prac domowych.
Przykładowe zadania: 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ń.