Editing Abstract interpretation (section)

== Formalization ==

[[File:Abstract interpretation of integers by signs svg.svg|thumb|Example: abstraction of integer sets (red) to sign sets (green)]]
Let <math>L</math> be an [[ordered set]], called ''concrete set'', and let <math>L'</math> be another ordered set, called ''abstract set''. These two sets are related to each other by defining [[total function]]s that map elements from one to the other.

A  function <math>\alpha</math> is called an ''abstraction function'' if it maps an element <math>x</math> in the concrete set <math>L</math> to an element <math>\alpha(x)</math> in the abstract set <math>L'</math>. That is, element  <math>\alpha(x)</math> in <math>L'</math> is the ''abstraction'' of <math>x</math> in <math>L</math>.

A function <math>\gamma</math> is called a ''concretization function'' if it maps an element <math>x'</math> in the abstract set <math>L'</math> to an element <math>\gamma(x')</math> in the concrete set <math>L</math>. That is, element <math>\gamma(x')</math> in <math>L</math> is a ''concretization'' of <math>x'</math> in <math>L'</math>.

Let <math>L_1</math>, <math>L_2</math>, <math>L'_{1}</math>, and <math>L'_2</math> be ordered sets. The concrete semantics <math>f</math> is a monotonic function from <math>L_1</math> to <math>L_2</math>. A function <math>f'</math> from <math>L'_{1}</math> to <math>L'_2</math> is said to be a ''valid abstraction'' of <math>f</math> if, for all <math>x'</math> in <math>L'_{1}</math>, we have <math>(f \circ \gamma)(x') \leq (\gamma \circ f')(x')</math>.

Program semantics are generally described using [[fixed point (mathematics)|fixed point]]s in the presence of loops or recursive procedures. Suppose that <math>L</math> is a [[complete lattice]] and let <math>f</math> be a [[monotonic function]] from <math>L</math> into <math>L</math>. Then, any <math>x'</math> such that <math>f(x') \leq x'</math> is an abstraction of the least fixed-point of <math>f</math>, which exists, according to the [[Knaster&ndash;Tarski theorem]].

The difficulty is now to obtain such an <math>x'</math>. If <math>L'</math> is of finite height, or at least verifies the [[ascending chain condition]] (all ascending sequences are ultimately stationary), then such an <math>x'</math> may be obtained as the stationary limit of the [[monotonic sequence|ascending sequence]] <math>x'_{n}</math> defined by induction as follows: <math>x'_{0} = \bot</math> (the least element of <math>L'</math>) and <math>x'_{n+1} = f'(x'_{n})</math>.

In other cases, it is still possible to obtain such an <math>x'</math> through a (pair-)[[Widening (computer science)|widening operator]],<ref>{{cite book |first1=P. |last1=Cousot |first2=R. |last2=Cousot| chapter=Comparing the Galois Connection and Widening / Narrowing Approaches to Abstract Interpretation |chapter-url=http://www.dsi.unive.it/%7Ecortesi/paperi/sefm08.pdf |editor-first=Maurice |editor-last=Bruynooghe |editor-first2=Martin |editor-last2=Wirsing |title=Proc. 4th Int. Symp. on Programming Language Implementation and Logic Programming (PLILP)|date=August 1992 |pages=269–296| publisher=Springer |isbn=978-0-387-55844-8 |volume=631 |series=Lecture Notes in Computer Science}}</ref> defined as a binary operator <math>\nabla\colon L\times L\to L</math> which satisfies the following conditions:

# For all <math>x</math> and <math>y</math>, we have <math>x \leq x \mathbin{\nabla} y</math> and <math>y \leq x \mathbin{\nabla} y</math>, and
# For any ascending sequence <math>(y'_{n})_{n\geq 0}</math>, the sequence defined by <math>x'_{0} := \bot</math> and <math>x'_{n+1} := x'_{n} \mathbin{\nabla} y'_{n}</math> is ultimately stationary. We can then take <math>y'_{n}=f'(x'_{n})</math>.

In some cases, it is possible to define abstractions using [[Galois connection]]s <math>(\alpha, \gamma)</math> where <math>\alpha</math> is from <math>L</math> to <math>L'</math> and <math>\gamma</math> is from <math>L'</math> to <math>L</math>. This supposes the existence of best abstractions, which is not necessarily the case. For instance, if we abstract sets of couples <math>(x, y)</math> of [[real number]]s by enclosing convex [[polyhedron|polyhedra]], there is no optimal abstraction to the disc defined by <math>x^2 + y^2 \leq 1</math>.