Abstract Interpretation
“Abstract interpretation is a theory of abstraction and constructive approximation of the mathematical structures used in the formal description of complex of infinite systems and the inference or verification of their combinatorial or undecidable properties” [0]
“Abstract interpretation of programs consists in using that denotation to describe computations in another universe of abstract objects, so that the results of abstract execution give some information on the actual computations” [1]
“The conclusion points out that abstract interpretation of programs is a unified approach to apparently unrelated program analysis techniques” [1]
Automatic program analyses are used for determining statically conservative approximations of dynamic properties of programs. Such properties of the run-time behaviour of programs are useful for debugging (e.g., type inference), code optimization (e.g., compile-time garbage collection useless occur-check elimination), program transformation (e.g., partial evaluation, parallelization), and even program correctness proofs (e.g., termination proof).
After a few simple introductory examples, we recall the classical framework for abstract interpretation of programs. Starting from a ground operational semantics formalizes as a transition system, classes of program properties are first encapuslated in collecting semantics expressed as fix points on partial orders representing concrete program properties. We consider invariance properties characterizing descendants of the initial states (corresponding to top/down or forward analyses), ascendant states of the final states (corresponding to bottom/up or backward analyses) as well as a combination of the two. Then we choose specific approximate abstract properties to be gathered about program behaviours and express them as elements of a poset of abstract properties. The correspondence between concrete and abstract properties is established by a concretization and abstraction function that is a Galois connection formalizing the loss of information. We can constructively derive the abstract program properties from the collecting semantics by a formal computation leading to a fix point in terms of abstract operators on the domain of abstract properties. The design of abstract interpreter then involves the choice of a chaotic iteration strategy to solve this abstract fix point equation.” [2]
“Abstract interpretation is a method for designing approximate semantics of programs which can be used to gather information about programs in oder to provide sound answers to questions about their run-time behaviours.” [3]
The purpose of abstract interpretation is to prove the soundness of such progra analysis methods with respect to a semantics, or better to formally design them by approximation of the semantics of programs. Hence from a theoretical point of view, the purpose of abstract interpretation is to design hierarchies of interrelated semantics specifying at various levels of details the behaviour of programs when executed by computers. This corresponds to understanding of “interpret” as “to explain the meaning of”, the qualification as “abstract” enforcing “to understand in a specified way”. From a practical point of view, the purpose of abstract interpretation is to design automatic program analysis tools for determining statically dynamic properties of programs. This corresponds to understanding of “interpret” as “to act as an interpreter”, the qualification as “abstract” enforcing the idea that the concrete domain of values is replaced by a domain of descriptions of values and concrete operators are given a corresponding non-standard interpretation.
“Abstract interpretation is a theory of abstraction and constructive approximation of the mathematical structures used in the formal description of complex or infinite systems and the inference or verification of their combinatorial or undecidable properties.” [1]