Abstract interpretation

from Wikipedia, the free encyclopedia

The abstract interpretation is a method in the field of program analysis .

The aim of abstract interpretation is to get information about the behavior of programs (analysis of semantics ) by abstracting parts of the program and following the instructions step by step ( interpretation ).

With the abstract interpretation, one concentrates on partial aspects of the execution of the instructions, one skilfully omits some information ( abstraction ), and ultimately one obtains an approximation to the program semantics, which can, however, be completely sufficient for the desired purpose.

Many properties of programs cannot be calculated . H. you cannot specify a program that calculates it in a finite time with finite memory resources for any programs. With an approximation , i.e. the omission of some information, questions about certain properties can no longer be answered at all, but other properties can only be calculated in the coarsened view.

The method comes from Radhia Cousot and Patrick Cousot .

example

A compiler wants to analyze what type of return a particular function has. A coarse understanding (read: abstract interpretation) of the calculations is sufficient for this. 

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

For example, the statement 

   x = 4 + 5

as a calculation 

   int + int

with result type “int” for the variable x. It is sufficient to know that 4 and 5 are each whole numbers (here of the “int” type), but their exact value is not of interest for determining the type and can therefore be omitted.

It goes on with 

   y = x * 3.14

which as 

  int * real

would be interpreted with the result value "real".

If you follow all the instructions of the function in this coarsened view, it is clear at the end what type the return value has.

literature

  • Flemming Nielson, Hanne R. Nielson, Chris Hankin: Principles of Program Analysis.
  • Patrick Cousot, Radhia Cousot: Static Verification of Dynamic Properties of Variables . Technical report of the 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. Los Angeles, California 1977. ACM Press, New York, pp. 238-252. (on-line)

Web links

software