Semantyka języków programowania (wykład i ćwiczenia)
Instytut Informatyki UWr
Semestr zimowy 2008/09
Opis przedmiotu
Przedmiot stanowi wprowadzenie do zagadnień związanych z matematycznym
opisem semantyki języków programowania, w tym semantyki operacyjnej,
denotacyjnej i aksjomatycznej języków imperatywnych, jak również
semantyki operacyjnej i denotacyjnej języków funkcyjnych.
Czas i miejsce
- Wykład: środa 12:15-14:00, sala 140
- Ćwiczenia: środa 16:15-18:00, sala 141
- Konsultacje: czwartek 14:30-16:00, pokój 327
|
Rozkład jazdy
|
Nr
|
Data
|
Zagadnienia
|
Do poczytania
|
Zadania
|
|
1.
|
08.10.2008
|
wstęp do wykładu i jego organizacja
modelowy język imperatywny IMP
operacyjna semantyka naturalna (dużych kroków) języka IMP
|
[NN99]: 1, 2.1
[Kah87]
|
lista 1
|
|
2.
|
15.10.2008
|
operacyjna semantyka strukturalna (małych kroków) języka IMP
|
[NN99]: 2.2 - 2.4
[Pit02]: 1.1, 3
|
lista 2
|
|
3.
|
22.10.2008
|
modularna semantyka operacyjna
semantyka operacyjna języka IMP w formie maszyny abstrakcyjnej
|
[NN99]: 3
[Pit02]: 1 - 3
[Mos04]
|
lista 3
|
|
4.
|
29.10.2008
|
dobrze ufundowana indukcja
indukcja matematyczna, indukcja strukturalna i indukcja na drzewach wyprowadzeń
definicje przez rekursję strukturalną
definicje indukcyjne i indukcja na regułach wyprowadzenia
|
[Hen90]: 1.3 - 1.5
[Har08]: 1 - 3
|
lista 4
|
|
5.
|
05.11.2008
|
semantyka denotacyjna języka IMP
elementy teorii dziedzin
|
[NN99]: 4.1 - 4.4
[Gor83]: 2 - 4
|
lista 5
|
|
6.
|
12.11.2008
|
obserwacyjna równoważność instrukcji i full abstraction
semantyka kontynuacyjna języka IMP
|
[NN99]: 4.5
[Gor83]: 5
|
lista 6
|
|
7.
|
19.11.2008
|
teoria dziedzin, c.d. (konstrukcje na dziedzinach, konstrukcje funkcji ciągłych, równania dziedzinowe)
|
[Pit99]: 1 - 3
[Plo83]: 1 - 3
[Gor83]: Dodatek
|
lista 7
|
|
8.
|
26.11.2008
|
semantyka aksjomatyczna języka IMP (semantyka asercji, reguły Hoare'a, poprawność reguł Hoare'a)
|
[NN99]: 6
[SK95]: 11
|
lista 8
|
|
9.
|
03.12.2008
|
względna pełność systemu reguł Hoare'a
warunki weryfikacji
|
[NN99]: 6
|
lista 9
|
|
10.
|
10.12.2008
|
semantyka rekursji (język definicji
rekursywnych REC, semantyka operacyjna
i denotacyjna języka REC oraz ich
równoważność przy ewaluacji przez
wartość oraz przez nazwę)
rekursywne definicje lokalne i twierdzenie Bekića
|
--
|
lista 10
|
|
11.
|
17.12.2008
|
indukcja stałopunktowa
semantyka
gorliwych języków funkcyjnych z typami wyższymi
(semantyka operacyjna i denotacyjna;
poprawność semantyki operacyjnej i
adekwatność semantyki denotacyjnej; relacje logiczne)
|
[NN99]: 6.1
[Pit99]: 4
|
--
|
|
12.
|
14.01.2009
|
PCF (semantyka operacyjna i denotacyjna;
poprawność semantyki operacyjnej i
adekwatność semantyki denotacyjnej; full abstraction)
|
[Pit99]: 5 - 8
[Plo77]
|
--
|
Literatura podstawowa
-
[Hen90]
Hennessy M., Semantics of Programming Languages, Wiley, 1990
-
[NN99] Nielson H. R., Nielson F.,
Semantics with Applications: A Formal Introduction, 1999
-
[Pit02] Pitts A.,
Semantics of Programming Languages, Lecture Notes, University of Cambridge, 2001
-
[Pit99] Pitts A.,
Denotational Semantics, Lecture Notes, University of Cambridge, 1999
-
[Win93] Winskel G., The Formal Semantics of Programming Languages: An Introduction, MIT Press, 1993
Literatura uzupełniająca
-
[Gor83] Gordon M., Denotacyjny opis języków programowania, WNT, 1983
-
[Gun92] Gunter C., Semantics of Programming Languages: Structures and Techniques, MIT Press, 1992
-
[Har08]
Harper R., Practical Foundations for Programming Languages, Working Draft, CMU, 2008
-
[Plo77]
Plotkin G. D., LCF Considered as a Programming Language,
Theoretical Computer Science , Vol. 5, pp. 223-255, 1977
-
[Plo81]
Plotkin G. D., A Structural Approach to Operational Semantics,
Lecture Notes, University of Aarhus, 1981
-
[Plo83]
Plotkin G. D., Domains,
Lecture Notes, University of Edinburgh, 1983
-
[Kah87] Kahn G., Natural semantics, 4th Annual Symposium on Theoretical Aspects of Computer Sciences, 1987
-
[Mos04]
Mosses P., Modular Structural Operational Semantics,
Journal of Logic and Algebraic Programming, 2004
-
[Rey98] Reynolds J., Theories of Programming Languages, Cambridge University Press, 1998
-
[Sch86]
Schmidt D., Denotational Semantics: A Methodology for Language Development, William C. Brown Publishers, 1986
-
[SK95]
Slonneger K., Kurtz B., Formal Syntax and Semantics of Programming Languages, Addison-Wesley Publishing Company, 1995
-
[Str06] Streicher T., Domain-Theoretic Foundations of Functional Programming,
World Scientific Publishing Corporation, 2006
|
|