Abstract Interpretation of Computer Programs
Given a programming or specification language, abstract interpretation consists of giving several semantics linked by relations of abstraction. A semantics is a mathematical characterization of a possible behavior of the program. The most precise semantics, describing very closely the actual execution of the program, are 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).
The goal of static analysis is to derive a computable semantic interpretation 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 multiplication, 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.
Sometimes a loss of precision is necessary to make the semantics decidable (see Rice's theorem, halting problem). In general, there is a compromise to be made between the precision of the analysis and its decidability (computability), or tractability (complexity).
In practice the abstractions that are defined are tailored to both the program properties one desires to analyze, and to the set of target programs. The first large scale automated analysis of computer programs with abstract interpretation can be attributed to an accident that resulted in the destruction of the first flight of the Ariane 5 rocket in 1996.
Read more about this topic: Abstract Interpretation
Famous quotes containing the words abstract, computer and/or programs:
“The whole body of what is now called moral or ethical truth existed in the golden age as abstract science. Or, if we prefer, we may say that the laws of Nature are the purest morality.”
—Henry David Thoreau (1817–1862)
“Family life is not a computer program that runs on its own; it needs continual input from everyone.”
—Neil Kurshan (20th century)
“Short of a wholesale reform of college athletics—a complete breakdown of the whole system that is now focused on money and power—the women’s programs are just as doomed as the men’s are to move further and further away from the academic mission of their colleges.... We have to decide if that’s the kind of success for women’s sports that we want.”
—Christine H. B. Grant, U.S. university athletic director. As quoted in the Chronicle of Higher Education, p. A42 (May 12, 1993)