Abstract Interpretation Intuition Abstract Interpretation Of

Its main concrete application is formal static analysis, the automatic extraction of information about the possible executions of computer programs; such analyses have two main usages:

1 Intuition

We shall now illustrate what abstract interpretation would mean on concrete, not computing examples.

Let us consider the people in a conference room. If we wish to prove that some persons were not present, one concrete method is to look up a list the names and social security numbers of all participants.

We may however have restricted ourselves to registering only their names. If the name of a person is not found in the list, we may safely conclude that that person was not present; but if it is, we cannot conclude definitely without further enquiries, due to the possibility of homonyms. Let us note that this imprecise information will still be adequate for most purposes, because homonyms are rare in practice.

If we are only interested in some specific information, say, "was there a person of age n in the room", keeping a list of all names and dates of births is unnecessary. We may safely and without loss of precision restrict ourselves to keeping a list of the participants' ages. If this is already too much to handle, we might keep only the minimal m and maximal M ages. If the question is about an age strictly lower than m or stricty higher than M, then we may safely respond that no such participant was present. Otherwise, we may only be able to say that we do not know.

In the case of computing, concrete, precise information is in general not computable within finite time and memory (see Rice's theorem and the halting problemIn computability theory the halting problem is a decision problem which can be informally stated as follows: : Given a description of an algorithm and its initial input, determine whether the algorithm, when executed on this input, ever halts (completes).). AbstractionThis article is about the concept of abstraction in general. For other uses, please see abstract (disambiguation). Abstraction is the thought process wherein ideas are distanced from objects. Abstraction uses a strategy of simplification of detail, wherei is used to simplify problems up to problems amenable to automatic solutions. One crucial issue is to diminish precision so as to make problems manageable while still keeping enough precision for answering the questions (such as "may the program crash?") one is interested in.

2 Abstract interpretation of computer programs

Given a programming or specification language, abstract interpretation consists in giving several semantics linked by relations of abstraction. The most precise semantics, describing very closely the actual execution of the program, is called the concrete semantics. For instance, the concrete semantics of an imperative programming language may associate to each program the set of execution traces it may produce – an execution trace being a sequence of possible consecutive states of the execution of the program; a state typically consists of the value of the program counter and the memory locations (globals, stack and heap). More abstract semantics are then derived; for instance, one may consider only the set of reachable states in the executions (which amounts to considering the last states in finite traces).

For goals of static analysis, some computable abstract semantics must be derived at some point. For instance, one may choose to represent the state of a program manipulating integer variables by forgetting the actual values of the variables and only keeping their signs (+, - or 0). For some elementary operations, such as multiplicationArithmetic In its simplest form, multiplication is a quick way of adding identical numbers. The result of multiplying numbers is called a product''. The numbers being multiplied are called coefficients or factors and individually as the multiplicand and m, such an abstraction does not lose any precision: to get the sign of a product, it is sufficient to know the sign of the operands. For some other operations, the abstraction may lose precision: for instance, it is impossible to know the sign of a sum whose operands are respectively positive and negative.

Such loss of precision may not, in general, be avoided so as to make a decidable semantics (see Rice's theorem, halting problemIn computability theory the halting problem is a decision problem which can be informally stated as follows: : Given a description of an algorithm and its initial input, determine whether the algorithm, when executed on this input, ever halts (completes).). There is, in general, a compromise to be made between the precision of the analysis and its tractability, either from a computability point of view or from a complexityThere are different senses of complexity In information processing, complexity is a measure of the total number of properties transmitted by an object and detected by an observer. Such a collection of properties is often referred to as a state. In physica point of view.

3 Formalization

Let L be an ordered set, called a concrete set and let L' be another ordered set, called an abstract set. These two sets are related to each other by defining total functions that map elements from one to the other.

A function α is called an abstraction function if it maps an element x in the concrete set L to an element α(x) in the abstract set L'. That is, element α(x) in L' is the abstraction of x in L.

A function γ is called a concretization function if it maps an element x' in the abstract set L' to an element γ(x') in the concrete set L. That is, element γ(x') in L is the concretization of x' in L'.

Let L₁, L₂, L'₁ and L'₂ be ordered sets. The concrete semantics f is a monotonic function from L₁ to L₂. A function f' from L'₁ to L'₂ is said to be a valid abstraction of f if for all x'₁ in L'₁, f ∘ γ(x') ≤ γ ∘ f'(x').

Program semantics are generally described using fixed pointSee also fixed-point arithmetic. In mathematics, a fixed point of a function is a point that is mapped to itself by the function. For example, if f is defined on the real numbers by f ''x x''2 − 3''x + 4, then 2 is a fixed point of f because f 2) 2.s in the presence of loops or recursive procedures. Let us suppose that L is a complete lattice and let f be a monotonic function from L into L. Then, any x' such that f'(x') ≤ x' is an abstraction of the least fixed-point of f, which exists, according to the Knaster-Tarski theorem.

The difficulty is now to obtain such an x'. If L' is of finite height, or at least verifies the "ascending chain condition" (all ascending sequences are ultimately stationary), then such an x' may be obtained as the stationary limit of the ascending sequence x'_n defined by induction as follows: x'₀=⊥ (the least element of L') and x'_n+1=f'(x'_n).

In other cases, it is still possible to obtain such an x' through a widening operator ∇: for all x and y, x ∇ y should be greater or equal than both x and y, and for all sequence y'_n, the sequence defined by x'₀=⊥ and x'_n+1=x'_n ∇ y'_n is ultimately stationary. We can then take y'_n=f(x'_n).

In some cases, it is possible to define abstractions using Galois connections (α, γ) where α if from L to L' and γ is from L' to L. This supposes the existence of best abstractions, while is not necessarily the case. For instance, if we abstract sets of couples (x,y) of real numbers by enclosing convex polyhedra, there is no optimal abstraction to the disc defined by x²+y² ≤ 1.

4 Tools

5 See also

6 External links

Computation Logic in computer science

<Hide>

Home > Abstract interpretation