INF.01110.08 - Semantik von Programmiersprachen (Vollständige Modulbeschreibung)

INF.01110.08	5 CP
Modulbezeichnung	Semantik von Programmiersprachen
Modulcode	INF.01110.08
Semester der erstmaligen Durchführung
Fachbereich/Institut	Institut für Informatik
Verwendet in Studiengängen / Semestern	Bioinformatik (MA120 LP) (Master) > Bioinformatik BioinformatikMA120, Akkreditierungsfassung gültig ab SoSe 2023 > Softwaretechnik und Übersetzerbau (Anteil gem. § 5 Abs. 4-6, Anlage 2) Bioinformatik (MA120 LP) (Master) > Bioinformatik BioinformatikMA120, Akkreditierungsfassung (WS 2009/10 - SS 2016) > Softwaretechnik und Programmiersprachen Bioinformatik (MA120 LP) (Master) > Bioinformatik BioinformatikMA120, Akkreditierungsfassung (WS 2016/17 - WS 2022/23) > Softwaretechnik und Übersetzerbau Informatik (MA120 LP) (Master) > Informatik InformatikMA120, Akkreditierungsfassung gültig ab SoSe 2023 > Vertiefende Module der Vertiefungsrichtung `Algorithmen und Theoretische Informatik` Informatik (MA120 LP) (Master) > Informatik InformatikMA120, Akkreditierungsfassung gültig ab SoSe 2023 > Vertiefende Module der Vertiefungsrichtung `Softwaretechnik und Übersetzerbau` mehr... Informatik (MA120 LP) (Master) > Informatik InformatikMA120, Akkreditierungsfassung (WS 2006/07 - SS 2013) > Primärmodule Informatik (MA120 LP) (Master) > Informatik InformatikMA120, Akkreditierungsfassung (WS 2013/14 - SS 2016) > Vertiefende Module der Vertiefungsrichtung `Algorithmen und Theoretische Informatik` Informatik (MA120 LP) (Master) > Informatik InformatikMA120, Akkreditierungsfassung (WS 2013/14 - SS 2016) > Vertiefende Module der Vertiefungsrichtung `Softwaretechnik und Übersetzerbau` Informatik (MA120 LP) (Master) > Informatik InformatikMA120, Akkreditierungsfassung (WS 2016/17 - WS 2022/23) > Vertiefende Module der Vertiefungsrichtung `Algorithmen und Theoretische Informatik` Informatik (MA120 LP) (Master) > Informatik InformatikMA120, Akkreditierungsfassung (WS 2016/17 - WS 2022/23) > Vertiefende Module der Vertiefungsrichtung `Softwaretechnik und Übersetzerbau` Mathematik (MA120 LP) (Master) > Mathematik MathematikMA120, Akkreditierungsfassung gültig ab WS 2022/23 > Anwendungsfach Informatik (20 LP sind zu erbringen) Mathematik (MA120 LP) (Master) > Mathematik MathematikMA120, Akkreditierungsfassung (WS 2013/14 - SoSe 2023) > Anwendungsfach Informatik Wirtschaftsinformatik (Business Information Systems) (MA120 LP) (Master) > Wirtschaftsinformatik WirtschaftsinformatMA120, Akkreditierungsfassung (WS 2008/09 - WS 2015/16) > II. Informatik Wirtschaftsinformatik (Business Information Systems) (MA120 LP) (Master) > Wirtschaftsinformatik WirtschaftsinformatMA120, Akkreditierungsfassung (WS 2008/09 - WS 2015/16) > Informatik (W)
Modulverantwortliche/r
Weitere verantwortliche Personen	Prof. Dr. Wolf Zimmermann
Teilnahmevoraussetzungen
Kompetenzziele	Die Teilnehmerinnen 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 Teilnehmerinnen sollen beurteilen können, zu welchem Zweck die unterschiedlichen Arten formaler Semantiken von Programmiersprachen eingesetzt werden können. Die Teilnehmerinnen sollen in der Lage sein, auf Basis formaler Semantiken von Programmiersprachen Eigenschaften von Programmiersprachen wie z.B. Typsicherheit zu beweisen. Die Teilnehmerinnen 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 Operationale Semantik: Inferenzregeln, statische Semantik, natürliche Semantik, strukturell operationale Semantik, Nachweis der Typkorrektheit, Validierung Abstrakte Maschine: Abstrakte Zusatzmaschinen, Validierung und Übersetzerkorrektheit
Lehrveranstaltungsformen	Seminar (3 SWS) Übung (2 SWS) Kursus
Unterrichtsprachen	Deutsch, Englisch
Dauer in Semestern	1 Semester Semester
Angebotsrhythmus Modul	beginnend im Wintersemester im Wechsel mit
Aufnahmekapazität Modul	unbegrenzt
Prüfungsebene
Credit-Points	5 CP
Modulabschlussnote	LV 1: %; LV 2: %; LV 3: %.
Faktor der Modulnote für die Endnote des Studiengangs	1
Hinweise	Dieses Modul ist ein weiterführendes Modul der Vertiefungsrichtung "Softwaretechnik und Übersetzerbau"

Modulveranstaltung	Lehrveranstaltungsform	Veranstaltungstitel	SWS	Workload selbstgestaltete Arbeit	Workload Summe
LV 1	Seminar	Seminar	3		0
LV 2	Übung	Übung	2		0
LV 3	Kursus	Bearbeitung der Übungsaufgaben/Selbststudium			0
Workload modulbezogen				150	150
Workload Modul insgesamt					150

Prüfung	Prüfungsvorleistung	Prüfungsform
LV 1
LV 2
LV 3
Gesamtmodul	Bearbeitung aller Übungsaufgaben	mündl. Prüfung oder Klausur
Wiederholungsprüfung

Regularien	Angebotsrhythmus	Anwesenheitspflicht	Gewicht an Modulnote in %
LV 1	Wintersemester	Nein	%
LV 2	Wintersemester	Nein	%
LV 3	Wintersemester	Nein	%