INF.01110.08 - Semantik von Programmiersprachen (Complete module description)
INF.01110.08 - Semantik von Programmiersprachen (Complete module description)
INF.01110.08
5 CP
Module label
Semantik von Programmiersprachen
Module code
INF.01110.08
Semester of first implementation
Faculty/Institute
Institut für Informatik
Module used in courses of study / semesters
Bioinformatik (MA120 LP) (Master) > Bioinformatik BioinformatikMA120, Version of accreditation valid from SoSe 2023 > Softwaretechnik und Übersetzerbau (Anteil gem. § 5 Abs. 4-6, Anlage 2)
Bioinformatik (MA120 LP) (Master) > Bioinformatik BioinformatikMA120, Version of accreditation (WS 2009/10 - SS 2016) > Softwaretechnik und Programmiersprachen
Bioinformatik (MA120 LP) (Master) > Bioinformatik BioinformatikMA120, Version of accreditation (WS 2016/17 - WS 2022/23) > Softwaretechnik und Übersetzerbau
Informatik (MA120 LP) (Master) > Informatik InformatikMA120, Version of accreditation valid from SoSe 2023 > Vertiefende Module der Vertiefungsrichtung `Algorithmen und Theoretische Informatik`
Informatik (MA120 LP) (Master) > Informatik InformatikMA120, Version of accreditation valid from SoSe 2023 > Vertiefende Module der Vertiefungsrichtung `Softwaretechnik und Übersetzerbau`
Informatik (MA120 LP) (Master) > Informatik InformatikMA120, Version of accreditation (WS 2006/07 - SS 2013) > Primärmodule
Informatik (MA120 LP) (Master) > Informatik InformatikMA120, Version of accreditation (WS 2013/14 - SS 2016) > Vertiefende Module der Vertiefungsrichtung `Algorithmen und Theoretische Informatik`
Informatik (MA120 LP) (Master) > Informatik InformatikMA120, Version of accreditation (WS 2013/14 - SS 2016) > Vertiefende Module der Vertiefungsrichtung `Softwaretechnik und Übersetzerbau`
Informatik (MA120 LP) (Master) > Informatik InformatikMA120, Version of accreditation (WS 2016/17 - WS 2022/23) > Vertiefende Module der Vertiefungsrichtung `Algorithmen und Theoretische Informatik`
Informatik (MA120 LP) (Master) > Informatik InformatikMA120, Version of accreditation (WS 2016/17 - WS 2022/23) > Vertiefende Module der Vertiefungsrichtung `Softwaretechnik und Übersetzerbau`
Mathematik (MA120 LP) (Master) > Mathematik MathematikMA120, Version of accreditation valid from WS 2022/23 > Anwendungsfach Informatik (20 LP sind zu erbringen)
Mathematik (MA120 LP) (Master) > Mathematik MathematikMA120, Version of accreditation (WS 2013/14 - SoSe 2023) > Anwendungsfach Informatik
Wirtschaftsinformatik (Business Information Systems) (MA120 LP) (Master) > Wirtschaftsinformatik WirtschaftsinformatMA120, Version of accreditation (WS 2008/09 - WS 2015/16) > II. Informatik
Wirtschaftsinformatik (Business Information Systems) (MA120 LP) (Master) > Wirtschaftsinformatik WirtschaftsinformatMA120, Version of accreditation (WS 2008/09 - WS 2015/16) > Informatik (W)
Responsible person for this module
Further responsible persons
Prof. Dr. Wolf Zimmermann
Prerequisites
Skills to be acquired in this module
Die Teilnehmer*innen sind in der Lage, die wissenschaftlichen Grundlagen zur Definition formaler Semantiken von Programmiersprachen zu verstehen und sie zur Definition formaler Semantiken von Programmiersprachen zu nutzen.
Die Teilnehmer*innen sollen beurteilen können, zu welchem Zweck die unterschiedlichen Arten formaler Semantiken von Programmiersprachen eingesetzt werden können.
Die Teilnehmer*innen sollen in der Lage sein, auf Basis formaler Semantiken von Programmiersprachen Eigenschaften von Programmiersprachen wie z.B. Typsicherheit zu beweisen.
Die Teilnehmer*innen sollen formale Semantiken von Programmiersprachen gegenüber den informellen Sprachdefinitionen validieren können.
Module contents
Ohne die Definition einer Semantik einer Programmiersprache ist für die Konstruktion korrekter Softwarewerkzeuge unmöglich, weil die formale Basis für die Korrektheit fehlt. Insbesondere kann die Korrektheit von Programmanalysen und Transformationen nicht beurteilt werden. Das Modul zeigt auf welchen verschiedenen Arten eine formale Semantik definiert werden kann und welchen Nutzen diese Definition hat, z.B. indem gezeigt wird das Programmiersprachen stark typisiert sind, also keine Typfehler zur Laufzeit aufweisen, dass Verifikationskalküle korrekt sind, oder wie Übersetzer verifiziert werden können.
Denotationale Semantik: Lambda-Kalkül, Bereiche, vollständige Halbordnungen, Fixpunkte, Nachweis der Typkorrektheit