Prof. Dr. Manfred Schmidt-Schauß Fachbereich Informatik (20) Künstliche Intelligenz/Softwaretechnologie Johann Wolfgang Goethe-Universität Frankfurt am Main

Funktionales Programmieren II: Semantik, statische Analyse, Verifikation und abstrakte Interpretation

Wintersemester 1996/97

Übungsblatt Nr. 9

‘What other explanation could there be?’

‘For what?’

‘For this boy. For this! He waved the Meisterwerk with a snarl. My world began to disintegrate. ‘You mean … you don’t like it?’ ‘Like it? Like it? It’s garbage. Offal. It’s not a thesis, it’s faeces! It’s pus, moral slime, ordure.’

aus Stephen Fry: making History

Aufgabe 1

Auf dem Netz des RBI liegt im Verzeichnis /usr/usersb2/ki/panitz/bin eine Version des Striktheitsanalyseprogramms von Marko Schütz. Das Programm trägt dort den Namen AnalyserNeu. Eine Beschreibung der Eingabesyntax und Aufrufzeile findet sich in der Diplomarbeit von Marko Schütz beschrieben, die unter

http://kiste-5.ki.informatik.uni-frankfurt.de/papers/masters.html

abrufbar ist.

Versuchen sie mit dieser Implementierung die Aufgaben vom Übungsblatt 8 automatisch zu lösen.

Eine kleine Beispieldatei liegt bei. Ein typischer Aufruf ist:

./AnalyserNeu 40 length.core

Aufgabe 2

Wir wollen den Datentyp von Bäumen betrachten, den wir in Haskell wie folgt definieren würden:

data Baum = Ende | Knoten Baum Int Baum

a) Definieren sie eine abstrakte Interpretation für den Typ Baum, mit Werten, so daß sie folgende Eigenschaften ausdrücken können:

– ein Ausdruck hat keine Kopfnormalform.

– ein Ausdruck hat höchstens eine Kopfnormalform.

– es kann höchstens der linkeste Pfad eines Baumes bis zum Ende ausgewertet werden.

– es kann höchstens der rechteste Pfad eines Baumes in der Länge bis zum Ende ausgewertet werden.

– es kann höchstens der linkeste Pfad eines Baumes komplett mit allen auf diesem Pfad enthaltenen Elementen ausgewertet werden.

– es kann höchstens der rechteste Pfad eines Baumes komplett mit allen auf diesem Pfad enthaltenen Elementen ausgewertet werden.

– die komplette Baumstruktur läßt sich unter Umständen auswerten.

– der Ausdruck kann eine Normalform haben.

b) Deninieren Sie für die abstrakte Interpretation auf Bäumen abstakte Interpretationen von Ende, Knoten und dem case auf Bäumen.