Suche Home Einstellungen Anmelden Hilfe  

UNI Didaktik der
Informatik
DdI

Spezialvorlesung
"Semantik und Programmverifikation"

Veranstalter: Prof. Dr. Andreas Schwill
Zielgruppe: Hauptstudium
Umfang: 2 SWS Vorlesung, Übung nach Bedarf
Fachzuordnung: Theoretische Informatik
Leistungspunkte: 3 benotete Punkte
Beginn: 16.10.2003
Zeit: donnerstags 17.00-18.30 Uhr
Ort: 3.04.0.02
Aktuelles: In Abänderung der angekündigten Bedingungen erfolgt die Leistungserfassung statt durch eine Klausur in Form einer kurzen mündlichen Prüfung (ca. 15 Minuten).
Dazu werden die Teilnehmer bis zum 31.3.2004 um Absprache eines Prüfungstermins gebeten.
Letzter Termin für eine Prüfung ist der 31.03.2004.
    Inhaltsübersicht
    Unter Semantik versteht man allgemein die Lehre von der inhaltlichen Bedeutung einer Sprache, wobei man sich in der Informatik auf Programmiersprachen oder mathematische Kalküle bezieht.
    Während die Semantik früher überwiegend umgangssprachlich erklärt wurde, da nur wenige formale Beschreibungsmethoden bekannt waren, wurden seit 1970 erhebliche Fortschritte bei den formalen Beschreibungsmethoden gemacht.
    Warum benötigt man eine formale und exakte Semantik einer Programmiersprache? Diese Notwendigkeit ergibt sich aus der Forderung, Programme in unmißverständlicher Art und Weise aufschreiben und interpretieren sowie sie präzise daraufhin untersuchen zu können, ob sie das leisten, was beabsichtigt war.
    Auch um Übersetzer konstruieren zu können, muß man genaue Semantikdefinitionen der Quell- und Zielsprache besitzen, denn der Übersetzer soll ja zu jedem Quellprogramm ein semantisch äquivalentes Zielprogramm erzeugen.
    Als Verifikation bezeichnet man den formalen Nachweis von Eigenschaften von Programmen oder Programmteilen. Sie dient zum Nachweis der Korrektheit eines Programms, also der Übereinstimmung von Spezifikation und Funktion des Programms. Während man beim Testen die Funktion des Programms für einzelne gut gewählte Eingaben überprüft und hofft, daß das Programm dann auch für alle Eingaben korrekt arbeitet, wird bei der Verifikation die Korrektheit füralle Eingaben bewiesen.
    Software kann nur durch Methoden der Spezifikation und Verifikation und durch Beweistechniken als zuverlässig nachgewiesen werden, und Grundlage einer Verifikation ist eine formale Semantik der zugrundeliegenden Programmiersprache.
    In der Vorlesung führen wir in unterschiedliche Zugänge zur Definition der Semantik von (sequentiellen) Programmiersprachen und zur Verifikation von Programmen ein.
    Inhalte:
    • Übersetzersemantik
    • operationale Semantik - abstrakte Maschinen
    • funktionale Semantik - Fixpunktberechnung, Induktion, Halbordnungen
    • axiomatische Semantik - Prädikatenlogik
    Funktionale und axiomatische Semantik bilden den Schwerpunkt der Vorlesung.
    Skriptum
    • handschriftliche Notizen des Dozenten und Begleitmaterialien können in Eigenregie kopiert werden.

    Note: §10 der Prüfungsordnung bestimmt die Form der Noten: Zulässig sind 1,0 bis 4,0 mit Zwischennoten sowie 5,0 (= nicht bestanden, kein Erwerb von Leistungspunkten).

info  Formale Semantik - R. Hartwig - 1996
Skriptum
info  Logik, Semantik und Verifikation - G. Smolka - 2002
Skriptum
info  Programmverifikation - R. Hartwig - 2000
Skriptum
info  Übersicht über den Leistungsstand aller Teilnehmer - WS2003/2004
info  Übungsblätter

Benutzer: gast • Besitzer: schwill • Zuletzt geändert am: