AT's teaching

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

Program Semantics and Verification

Sorry, no English version...
...i brak polskich znakow...

Semantyka i weryfikacja programow

wyklad w roku akademickim 2011/12, semestr zimowy
poniedzialki, godz. 12.15-14.00, sala 5440

EGZAMIN: odbyl sie.

EGZAMIN POPRAWKOWY: tez sie odbyl.

Celem wykladu jest pokazanie roli i najwazniejszych problemow i technik formalizacji opisu programow. Omawiane beda metody definiowania semantyki programow, z ich matematycznymi podstawami i praktycznymi technikami. Wprowadzone zostana pojecia poprawnosci programow oraz techniki i formalizmy dla ich dowodzenia. Przedstawione tez beda najwazniejsze idee systematycznego konstruowania poprawnych programow.

Warunki zaliczenia i egzaminu

Prace domowe: Zaliczenie cwiczen i dopuszczenie do egzaminu odbedzie sie na podstawie prac domowych. Beda trzy prace domowe, kazde zlozone z jednego zadania, oceniane na sklali 0-1. Zadania beda wspolne dla wszystkich grup, ale sprawdzane i omawiane przez prowadzacych poszczegolnych grupy cwiczeniowe.

Do zaliczenia cwiczen i dopuszczenia do pierwszego terminu egzaminu niezbedne jest uzyskanie nie mniej niz 1.8 punktow z trzech prac domowych.

zadanie pierwsze (semantyka operacyjna):
- tresc zadania i proponowane rozwiazanie
zadanie drugie (semantyka denotacyjna):
- tresc zadania i proponowane rozwiazanie
zadanie trzecie (weryfikacja):
- tresc zadania i proponowane rozwiazanie

Egzamin: odbyl sie 25 stycznia 2012, godz. 16.30. Mial forme pisemna, byly trzy zadania:

zadanie pierwsze (semantyka operacyjna):
- tresc zadania i proponowane rozwiazanie
zadanie drugie (semantyka denotacyjna):
- tresc zadania i proponowane rozwiazanie
zadanie trzecie (weryfikacja):
- tresc zadania oraz proponowane rozwiazanie i inna wersja rozwiazania

W srode, 1 lutego, w godz. 10.00-13.00(+ duzy epsilon :-) byly dostepne osoby sprawadzjace zadania i prowadzacy wyklad. Mozna bylo z nimi omowic uzyskane wyniki i uzyskac ewentualne modyfikacje oceny.

Ostateczne wyniki egzaminu: sa dostepne w USOSie.

Egzamin po prawkowy: odbyl sie w sesji poprawkowej, 28 lutego 2012, godz. 16.00-19.00(plus epsilon), sala 4420. Mial forme pisemna, byly trzy zadania:

zadanie pierwsze (semantyka operacyjna):
- tresc zadania i proponowane rozwiazanie
zadanie drugie (semantyka denotacyjna):
- tresc zadania i proponowane rozwiazanie
zadanie trzecie (weryfikacja):
- tresc zadania oraz proponowane rozwiazanie.

W czwartek lub piatek, 8/9 marca, byly dostepne osoby sprawadzjace zadania i prowadzacy wyklad. Mozna bylo z nimi omowic uzyskane wyniki i uzyskac ewentualne modyfikacje oceny.

Wyniki zostaly wtedy ustalone, protokol zamkniety. Dalsze zmiany nie leza w zakresie kompetencji prowadzacych przedmiot.

Materialy do wykladu:

Przezrocza do wykladow
- Wstep (3.10)
- Semantyka operacyjna (10.10, 17.10, 24.10)
- Semantyka denotacyjna (24.10, 7.11)
- Deklaracje i bloki (7.11, 14.11)
- Kontynuacje (21.11, 28.11)
- Punkty stale i teoria dziedzin (28.11, 5.12)
- Logika Hoare'a (12.12)
- Calkowita poprawnosc (19.12)
- Podstawowe pojecia algebry ogolnej (2.01, 9.01)
- Logika Hoare'a raz jeszcze (9.01)
- Systematyczne konstruowanie programow (16.01)
- O specyfikacjach i formalnym konstruowaniu oprogramowania (16.01)
Przykladowa literatura:
- P. Dembinski, J. Maluszynski. Matematyczne metody definiowania jezykow programowania. WNT, 1981.
- M. Gordon. Denotacyjny opis jezykow programowania. WNT, 1983.
- D. Gries. The Science of Programming. Springer-Verlag, 1981.
- E. Dijkstra. Umiejetnosc programowania. WNT, 1978.
Zadania z 5 lat ubieglych:
DISCLAIMER: zadania sa tu umieszczane w formie i postaci oryginalnej. Zwracam uwage, ze notacja i wymagania dotyczace rozwiazan mogly sie w czasie zmieniac; udostepniajac tutaj zadania i proponowane wowczas rozwiazania nie ponosze odpowiedzialnosci za mozliwe niedokladnosci (czy wrecz bledy) w rozwiazaniach i za rozbieznosci z obecnymi kryteriami ocen podobnych zadan.
Moze jeszcze cos tu sie pojawi...

AT (tarlecki@mimuw.edu.pl)