Formale Methoden und Deduktion
Prof. Dr. J. Avenhaus

Häufig gestellte Fragen und ihre Antworten

Warum werden nicht alle Folien der gesamten Vorlesung zum Kopieren zur Verfügung gestellt?
Das geht nicht, da Prof. Avenhaus nach jeder Vorlesung die Folien für die nächste Vorlesung ergänzt, ändert oder neu schreibt, um auf die Reaktionen der Studenden optimal eingehen zu können.
Wir geben uns immer Mühe, dass der entsprechende Satz für eine Vorlesung spätestens am Nachmittag vorher in der Bibliothek und in der Fachschaft Informatik vorhanden ist.
Warum kann man nicht auf die WWW-Seiten zur Vorlesung von außerhalb der Uni zugreifen?
Die Einschränkung hatte (leider) mit Sicherheitsproblemen zu tun. Nachdem das Anmeldeverfahren abgeschlossen ist, ist der Zugriff auf die Web-Seiten auch von außerhalb der Universität gestattet. Auf jedem Übungsblatt findet sich die aktuelle Adresse.
Können die Übungsblätter nicht im WWW zur Verfügung gestellt werden?
Aktuelle Übungsblätter wird es nur in der Vorlesung geben, nicht im Web.
Ich verstehe die Bedeutung der ganzen seltsamen Symbole nicht. Können Sie nicht eine Übersicht machen?
Eine entsprechende Liste zu machen ist eine gute Idee, sich selbständig mit dem Stoff auseinanderzusetzen. Die Bedeutung (und Aussprache) erfährt man in der Vorlesung: Einfach zuhören und ggf. auf der Folienkopie vermerken. In Zweifelsfällen können die Hiwis konsultiert werden.
Was ist eigentlich der Unterschied zwischen denotationaler und operationaler Semantik?
Kurz gefasst: Die denotationale Semantik legt die Bedeutung über den Aufbau von Programmen fest, die operationale über den Ablauf von Programmen. (Hier darf man sich nicht verwirren lassen, dass bei der operationalen Semantik die Einschrittrelation über den Aufbau von Programmen definiert ist.) Also: Fasst man ein while-Programm als Baum auf, werden bei der denotationalen Semantik von den Blättern hin zur Wurzel die Knoten mit Funktionen versehen, welche ggf. aus Funktionen der zugehörigen Söhne zusammengesetzt werden. Hier werden also nur mathematische Objekte betrachtet, es findet keine schrittweise Berechnung statt - wie auf konkreten Computern Maschinenbefehl für Maschinenbefehl. Dem viel näher ist offensichtlich die operationale Semantik und man könnte mit ihrer Hilfe sehr leicht einen Interpreter für while-Programme realisieren. Der Unterschied zwischen den beiden Semantiken wird noch deutlicher, wenn man rekursive Prozeduren betrachtet. Dies wird allerdings recht kompliziert und wurde deshalb nicht in der Vorlesung behandelt. Interessierte finden geeigneten weiterführenden Stoff unter den Stichwort Fixpunktsemantik oder cpo, wichtige Autoren sind Scott, Strachey oder Stoy.
Wenn wir beweisen, dass denotationale und operationale Semantik übereinstimmen, warum betrachten wir denn beide, eine würde doch genügen?
Die denotationale Semantik beschreibt eigentlich, was man haben will, die operationale, wie man es berechnen kann. In dem Sinne entspricht die denotationale Semantik einer Anforderungsspezifikation, die operationale einer (abstrakten) Implementierung. Beispielsweise ist für die Programmiersprache Scheme im Sprachreport die denotationale Semantik mit angegeben. Jede Implementierung (ob Interpreter oder Compiler) entspricht dann einer eigenen operationalen Semantik. Der Äquivalenzbeweis zeigt dann die Korrektheit der Implementierung.
Die beiden Semantiken haben auch unterschiedliche Anwendungsfelder: Die denotationale Semantik eignet sich eher für abstrakte Aussagen oder Untersuchungen, während die operationale Semantik beispielsweise direkt einen Zeitbegriff (Schrittzahl) mitbringt, was für Komplexitätsaussagen wichtig sein kann.

Impressum

AG Formale Methoden und Deduktion

Fachbereich Informatik

Technische Universität Kaiserslautern

Letzte Änderung: Wednesday, 26-Oct-05 08:59:15 GMT
www-aven@informatik.uni-kl.de

Formale Methoden und Deduktion Prof. Dr. J. Avenhaus

Häufig gestellte Fragen und ihre Antworten

Formale Methoden und Deduktion
Prof. Dr. J. Avenhaus