| |
|
Next: Open Problem: Error Quantification
Up: Background
Previous: Background
Abstract Interpretation is a theory for formally constructing conservative
approximations of the semantics of programming languages. In practice, it
is used for constructing semantics-based analysis algorithms for the
automatic, static and conservative determination of dynamic properties
of infinite-state programs. Such properties of the run-time behaviour
of programs are useful for debugging (e.g. type inference), code
optimisation (e.g. run time tests elimination), program transformation
(e.g. partial evaluation, parallelisation), and even program correctness
proofs (e.g. termination proof) [15].
According to the classical framework
[16, 14, 18],
an abstract interpretation is defined as a non-standard (approximated)
program semantics obtained from the standard (or concrete) one by
replacing the actual (concrete) domain of computation and its basic
(concrete) semantic operations with, respectively, an abstract
domain and corresponding abstract semantic operations.
The idea of non-standard semantics for analysis purposes dates back
to [55], where it was called pseudo-evaluation. Similar
ideas were developed in [58] and [63].
This approach, under the name ``data flow analysis'', was used later
on for compiler optimisation [33, 54]. A general
framework for abstract interpretation was developed in a series of
papers by Cousot starting with [16]. Recently,
the area of abstract interpretation in logic and constraint based
programming languages is very active [29, 8].
For a more detailed overview see for example [40].
Next: Open Problem: Error Quantification
Up: Background
Previous: Background
|
|
|
|
