|
Detailinformationen |
Quellcurriculum |
Bachelorstudium Technische Mathematik 2013W |
Ziele |
Die Studierenden lernen die wesentlichen Ansätze zur formalen Beschreibung der Semantik von Programmiersprachen und deren Zusammenhänge kennen; sie können die Semantik einfacher Sprachen formalisieren und diese in Form von Interpretern für diese Sprachen implementieren.
|
Lehrinhalte |
Abstrakte Syntax von Programmiersprachen als Basis der Formalisierung ihrer Semantik.
- Denotationale Semantik: die Formalisierung durch eine mathematische Funktion, die Programme auf mathematische Strukturen abbildet.
- Operationale Semantik: die Formalisierung durch eine Sammlung von Reduktionsregeln, die den Anfangszustand eines Programms in seinen Endzustand überführen.
- Axiomatische Semantik: die Formalisierung durch Korrektheitsbehauptungen, die es uns erlauben, Schlüsse über das Eingabe/Ausgabe-Verhalten von Programmen zu ziehen.
Beweis der Äquivalenz von denotationaler und operationaler Semantik einer einfachen imperativen Programmiersprache; Beweis der Korrektheit der axiomatischen Semantik anhand der denotationalen Semantik; konstruktive
Implementierung der denotationalen Semantik in Form eines Interpreters.
|
Beurteilungskriterien |
Schriftliche Aufgaben/Mini-Projekte (Formalisierungen einer Sprache mit einer prototypischen Implementierung als ein Interpreter).
|
Lehrmethoden |
Folien-basierter Vortrag mit praktischen Beispielen von Formalisierungen.
|
Abhaltungssprache |
Englisch |
Literatur |
- Wolfgang Schreiner. Thinking Programs (manuscript). Chapter "Programming Languages", 2020.
- David A. Schmidt. Denotational Semantics -- A Methodology for Language Development, Allyn and Bacon, Boston, MA, 1986.
- Glynn Winskel: The Formal Semantics of Programming Languages -- An Introduction, Foundations of Computing Series, MIT Press, Cambridge, MA, 1994.
- David A. Schmidt: The Structure of Typed Programming Languages, Foundations of Computing Series, MIT Press, Cambridge, MA, 1994.
- Hanne Riis Nielson and Flemming Nielson. Semantics with Applications - A Formal Introduction, John Wiley & Sons, 1992.
|
Lehrinhalte wechselnd? |
Nein |
Sonstige Informationen |
https://risc.jku.at/courses/
|
Äquivalenzen |
TM1WIVOFSEM: VO Formale Semantik von Programmiersprachen (3 ECTS)
|
|