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.
Modulinhalte
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
