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:
“Alice grown lazy, mammoth but not fat,
Declines upon her lost and twilight age;
Above in the dozing leaves the grinning cat
Quivers forever with his abstract rage....”
—Allen Tate (1899–1979)
“The computer takes up where psychoanalysis left off. It takes the ideas of a decentered self and makes it more concrete by modeling mind as a multiprocessing machine.”
—Sherry Turkle (b. 1948)
“Will TV kill the theater? If the programs I have seen, save for “Kukla, Fran and Ollie,” the ball games and the fights, are any criterion, the theater need not wake up in a cold sweat.”
—Tallulah Bankhead (1903–1968)