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:
“If the abstract rights of man will bear discussion and explanation, those of women, by a parity of reasoning, will not shrink from the same test: though a different opinion prevails in this country.”
—Mary Wollstonecraft (1759–1797)
“The analogy between the mind and a computer fails for many reasons. The brain is constructed by principles that assure diversity and degeneracy. Unlike a computer, it has no replicative memory. It is historical and value driven. It forms categories by internal criteria and by constraints acting at many scales, not by means of a syntactically constructed program. The world with which the brain interacts is not unequivocally made up of classical categories.”
—Gerald M. Edelman (b. 1928)
“Government ... thought [it] could transform the country through massive national programs, but often the programs did not work. Too often they only made things worse. In our rush to accomplish great deeds quickly, we trampled on sound principles of restraint and endangered the rights of individuals.”
—Gerald R. Ford (b. 1913)