Lehrveranstaltung

Vorlesung, 4 SWS, Schein, ECTS-Studium, ECTS-Credits: 8,0, Modul: MS0401; Fachgebiet: Theoretische Informatik/Praktische Informatik
Zeit und Ort: Mo, Mi 10:00 - 12:00, LMS2 - R.Ü3 (außer Mi 1.7.2009); Einzeltermin am 1.7.2009 10:00 - 12:00, LMS6 - R.10[Steinitz-Hörsaal]
vom 15.4.2009 bis zum 15.7.2009

Voraussetzungen / Organisatorisches

Diese vierstündige Vorlesung (plus einer zweistündigen Übung) wendet sich an die Studierenden der Informatik im Haupt- und Nebenfach. Ihr Thema ist die formale semantische Beschreibung der Kontrollstrukturen von Programmiersprachen mit ordnungstheoretischen und axiomatischen Mitteln (Stichworte: denotationelle und axiomatische Semantik), sowie sich daraus ergebende Techniken zur Spezifikation, Entwicklung und Verifikation von Programmen.

Inhalt

Zuerst stellen wir, nach einigen motivierenden Beispielen und einer knappen Übersicht, die ordnungstheoretischen Grundlagen der denotationellen Semantik bereit.
Dann zeigen wir, wie man formal eine denotationelle Semantik für eine funktionale bzw. eine prozedurale Sprachen entwickeln kann und wie die Art der semantischen Beschreibung u.a. von der Gestalt der Sprache und den verwendeten Konzepten abhängt. Als nächstes erklären wir anhand des Spezialfalles D = [D -> D] was mit einem rekursiven semantischen Bereich "gemeint" ist.
Schließlich widmen wir uns noch der Programmverifikation.
Hier studieren wir einige Methoden, die auch zur Programmentwicklung vewendet werden können. Bei den funktionalen Sprachen behandeln wir Fixpunkt-Verifikationsmethoden.
Verifikation von prozeduralen Programmen führt hingegen zur axiomatischen Semantik. Hier behandeln wir die beiden bekanntesten Ausprägungen, nämlich den Hoare-Kalkül für partielle und den wp-Kalkül für totale Korrektheit.

Falls Zeit bleibt, so gehen wir noch auf weitere Anwendungen der Semantik von Programmiersprachen ein, etwa auf transformationelle Programmierung oder formale Korrektheitsbeweise von Übersetzern.

Die Vorlesung orientiert sich an dem Buch "Semantik von Programmiersprachen" von R. Berghammer, welches im Jahr 2001 beim Logos-Verlag erschienen ist.

Empfohlene Literatur

Berghammer, R.: Ordnungen, Verbände und Relationen mit Anwendungen, Teubner, 2008

Loeckx J., Sieber K.: The Foundations of Program Verification. Teubner, 1984

Nielson H.R., Nielson F.: Semantics with Applications. A Formal Introduction. Wiley, 1992

Schmidt D.A.: Denotational Semantics - A Methodology for Language Development. Allyn and Bacon, 1986

Winskel G.: The Formal Semantics of Programming Languages. The MIT Press, 1993

Zusätzliche Informationen

Schlagwörter: Semantik
Erwartete Teilnehmerzahl: 30
www: http://www.informatik.uni-kiel.de/inf/Berghammer/teaching/semantik/index.shtml

Zugeordnete Lehrveranstaltungen

UE: Übungen zu: Semantik von Programmiersprachen (080062): Dozentinnen/Dozenten: Prof. Dr. Rudolf Berghammer, Dipl.-Inf. Jan Christiansen
Zeit und Ort: Mi 14:15 - 15:45, WSP3 - Seminarraum 1
www: http://www.informatik.uni-kiel.de/inf/Berghammer/teaching/semantik/uebungen.shtml



	UnivIS ist ein Produkt der Config eG, Buckenhof