Abstract interpretation

related topics
{math, number, function}
{law, state, case}
{rate, high, increase}
{theory, work, human}
{day, year, event}
{build, building, house}
{system, computer, user}

In computer science, abstract interpretation is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices. It can be viewed as a partial execution of a computer program which gains information about its semantics (e.g. control structure, flow of information) without performing all the calculations.

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:

Abstract interpretation was formalized by Patrick Cousot and Radhia Cousot.

Contents

Intuition

This article now illustrates what abstract interpretation means, by using real-world, non-computing, examples.

Consider the people in a conference room. To prove that some persons were not present, one concrete method is to look up a list of the names and some identifiers unique to them, like a social security number in the United States, of all participants. Since two different people cannot have the same number, it is possible to prove or disprove the presence of a participant simply by looking up his or her number in the list.

However it is possible that only the names of attendees were registered. 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 inquiries, due to the possibility of homonyms (for example two people named John Smith). Note that this imprecise information will still be adequate for most purposes, because homonyms are rare in practice. However, in all rigor, we cannot say for sure that somebody was present in the room; all we can say is that he or she was possibly here. If the person we are looking up is a criminal, we will issue an alarm; but there is of course the possibility of issuing a false alarm. Similar phenomena will occur in the analysis of programs.

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 strictly 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.

Full article ▸

related documents
E (mathematical constant)
Binary relation
Algebraic structure
Linear combination
Random variable
Pushdown automaton
Ideal class group
Axiom schema of replacement
Sequence
Elliptic curve
IEEE 754-1985
Heine–Borel theorem
Euclidean algorithm
Glossary of topology
Presentation of a group
Gaussian quadrature
Natural transformation
Factorization
Linear independence
Absolute convergence
Type theory
Galois theory
Partition (number theory)
Fuzzy logic
Ultrafilter
Database normalization
Complex analysis
Dijkstra's algorithm
Exclusive or
Countable set