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. 10

Was suchst Du mir Dich zu verstecken Sei offen, flieh nicht meinem Blick Früh oder später mußte ichs entdecken Und hier hast Du mein Wort zurück

Goethe

Aufgabe 1

Errechnen Sie per Fixpunktiteration korrekte abstrakte Werte der folgenden Funktionen auf der 4-Punkt-Domain.

a) append :: [Int] -> [Int] -> [Int]
b) map :: (Int -> Int) -> [Int] -> [Int]
c) filter :: (Int -> Bool) -> [Int] -> [Int]

d) Generieren Sie dieselbe Information mit abstrakter Reduktion.

Aufgabe 2

Wir benutzen in dieser Aufgabe die Baumdomain von Übungsblatt 9.

a) Berechnen Sie den abstrakten Wert der folgenden Funktion, die auf Bäumen operiert.

> BNil         = Cons{17,0};
> BCons l w r    = Cons{18,3} l w r;
> linear b
>  = case b of
>      <17> -> BNil;
>      <18> l w r
>          -> case l of
>              <17> ->  BCons l w (linear r);
>              <18> l1 wl l2 -> linear (BCons l1 wl (BCons l2 w r));

b) Versuchen Sie Werte für die Baumdomain für die abstrakte Reduktion darzustellen und generieren Sie per abstrakter Reduktion die entsprecenden Ergebnisse.