Das Kefk Network Wiki befindet sich im Testbetrieb.

Abstrakte Interpretation

Aus Kefk.

Wechseln zu: Navigation, Suche

Die abstrakte Interpretation ist eine Methode aus dem Bereich der Programmanalyse.

Ziel der abstrakten Interpretation ist es Informationen über das Verhalten von Programmen (Analyse der Semantik) zu bekommen, indem man von Teile des Programms abstrahiert und die Anweisungen Schritt für Schritt nachvollzieht (Interpretation).

Bei der abstrakten Interpretation konzentriert man sich auf Teilaspekte der Ausführung der Anweisungen, man lässt einiges an Information geschickt weg (Abstraktion), erhält letztlich eine Näherung an die Programmsemantik, die aber für den gewünschten Zweck vollkommen ausreichen kann.

Viele Eigenschaften von Programmen sind nicht berechenbar, d.h. man kann hier kein Programm angeben, welches in endlicher Zeit, mit endlichen Speicherresourcen für beliebige Programme diese Frage beantwortet. Das Weglassen an Information bringt es nun mit sich, dass man an der Approximation zwar weniger Fragen klären kann, diese Fragestellungen jedoch in dieser vergröberten Sicht plötzlich berechenbar sein könnten.

Inhaltsverzeichnis

Beispiel

Ein Compiler möchte analysieren, was für einen Rückgabetyp eine bestimmte Funktion hat. Dazu reicht schon ein vergröbertes Nachvollziehen (sprich: abstrakte Interpretation) der Berechnungen. 

    function f()
        x = 4 + 5
        y = x * 3.14
        return y

Z.B. kann die Anweisung 

   x = 4 + 5

als Berechnung 

   int + int

mit Ergebnistyp "int" für die Variable x betrachtet werden. Es reicht die Information, dass 4 und 5 jeweils ganze Zahlen (also hier vom Typ int) sind, ihr genauer Wert interessiert hingegen nicht für die Typbestimmung, kann also weggelassen werden.

Weiter geht es mit 

   y = x * 3.14

welches als 

  int * real

mit Ergebniswert real aufgefasst würde.

Vollzieht man alle Anweisungen der Funktion in dieser vergröbernden Sicht nach, so ist am Schluss klar, welchen Typ der Rückgabewert hat.


Weblinks


Software

Literatur

  • Principles of Program Analysis von Flemming Nielson, Hanne R. Nielson, Chris Hankin
  • Patrick Cousot, Radhia Cousot: Static Verification of Dynamic Properties of Variables. Technischer Bericht der Universite Scientifique et Medicale Grenoble, November 1975.
  • Patrick Cousot, Radhia Cousot: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, In Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 238--252, Los Angeles, California, 1977. ACM Press, New York.[[1]]
Von „http://www.kefk.org/wiki/Abstrakte_Interpretation“
Persönliche Werkzeuge
Andere Sprachen