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 |
 |
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
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.
Leistungserfassungsprozeß
Die Abschlußnote wird durch folgenden Prozeß ermittelt:
-
Klausur im Umfang von ca. 2h am Schluß der Vorlesung.
Sie erhalten eine Note gem. §10 der Prüfungsordnung.
Zur Übung werden unregelmäßig Übungsblätter
zur Verfügung stehen, deren Bearbeitung aber nicht in die Bewertung
eingeht.
Einen Überblick über Ihren aktuellen Leistungsstand erhalten
Sie jederzeit auf diesem Server.
Belegung
Die Belegung erfolgt elektronisch entsprechend der Bestimmungen des
Instituts
für Informatik.
Literaturhinweise
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).
|
Formale Semantik - R. Hartwig - 1996
Übersicht über den Leistungsstand aller Teilnehmer - WS2003/2004
Übungsblätter