Abstrakte Interpretation

Abstrakte Interpretation

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 Teilen 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 kein Programm angeben, welches sie in endlicher Zeit mit endlichen Speicherresourcen für beliebige Programme berechnet. Durch eine Approximation, also das Weglassen von einigen Informationen, kann man zwar Fragen nach bestimmten Eigenschaften gar nicht mehr klären, dafür werden aber andere Eigenschaften in der vergröberten Sicht erst berechenbar.

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

Zum Beispiel 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 ist hingegen für die Typbestimmung nicht interessant, 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öberten 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.online

Wikimedia Foundation.

Игры ⚽ Поможем написать реферат

Schlagen Sie auch in anderen Wörterbüchern nach:

  • Abstrakte Kunst — Frank Stella Memantra (2005) Abstrakte Kunst Abstrakte Kunst …   Deutsch Wikipedia

  • Abstrakte Zustandsmaschine — Eine abstrakte Zustandsmaschine (englisch Abstract State Machine (ASM), nicht zu verwechseln mit Algorithmic state machines, ehemals auch Evolving Algebra (EVA) genannt), ist in der Informatik ein Modell zur formalen, operationellen Beschreibung… …   Deutsch Wikipedia

  • Allgemeine Relativitätstheorie — Die allgemeine Relativitätstheorie (kurz: ART) beschreibt die Wechselwirkung zwischen Materie (einschließlich Feldern) einerseits und Raum und Zeit andererseits. Sie deutet Gravitation als geometrische Eigenschaft der gekrümmten vierdimensionalen …   Deutsch Wikipedia

  • Einsteintensor — Die allgemeine Relativitätstheorie (kurz: ART) beschreibt die Wechselwirkung zwischen Materie (einschließlich Feldern) einerseits und Raum und Zeit andererseits. Sie deutet Gravitation als geometrische Eigenschaft der gekrümmten vierdimensionalen …   Deutsch Wikipedia

  • Cartell — Verhältnisverträge regeln das Verhältnis von Studentenverbindungen oder deren Dachverbänden untereinander. Man unterscheidet Vorstellungs , Freundschafts , Kartell und Traditionsverhältnisse sowie, davon abgehoben, Paukverhältnisse, die nur die… …   Deutsch Wikipedia

  • Freundschaftsverhältnis — Verhältnisverträge regeln das Verhältnis von Studentenverbindungen oder deren Dachverbänden untereinander. Man unterscheidet Vorstellungs , Freundschafts , Kartell und Traditionsverhältnisse sowie, davon abgehoben, Paukverhältnisse, die nur die… …   Deutsch Wikipedia

  • KSCV — Gründung: 15. Juli 1848 in Jena Prinzipien: farbentragend, pflichtschlagend Mitgliedsverbindungen (2008): 101 …   Deutsch Wikipedia

  • Kartell (Verbindung) — Verhältnisverträge regeln das Verhältnis von Studentenverbindungen oder deren Dachverbänden untereinander. Man unterscheidet Vorstellungs , Freundschafts , Kartell und Traditionsverhältnisse sowie, davon abgehoben, Paukverhältnisse, die nur die… …   Deutsch Wikipedia

  • Kartellvertrag — Verhältnisverträge regeln das Verhältnis von Studentenverbindungen oder deren Dachverbänden untereinander. Man unterscheidet Vorstellungs , Freundschafts , Kartell und Traditionsverhältnisse sowie, davon abgehoben, Paukverhältnisse, die nur die… …   Deutsch Wikipedia

  • Kreise — Verhältnisverträge regeln das Verhältnis von Studentenverbindungen oder deren Dachverbänden untereinander. Man unterscheidet Vorstellungs , Freundschafts , Kartell und Traditionsverhältnisse sowie, davon abgehoben, Paukverhältnisse, die nur die… …   Deutsch Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”