Principles of program analysis.

*(English)*Zbl 0932.68013
Berlin: Springer. xxi, 450 p. (1999).

The authors concentrate on four main principal approaches to program analysis. They are data flow analysis, constraint based analysis, abstract interpretation and type and effect systems.

The content of data flow analysis covers the basic techniques for intraprocedural analysis, semantic correctness, monotone frameworks for solving equations, shape analyses.

An alternative to considering equations over program representation is the way of reasoning about programs using constraint systems. Constraint based analysis includes topics covering abstract control flow analysis without taking into account context information (0-CFA), well-definedness of the analysis, coinduction versus induction, semantic correctness and the existence of best solutions, adding data flow analysis to control flow analysis with the purpose to strengthen the quality of the control information.

Abstract interpretation is a methodology for calculating analyses through semantic relations rather than specifying then. From this viewpoint, the authors analyze a notion of correctness for a restricted class of analyses, approximation of fixed points by widening and narrowing operations, Galois connections, induced operations and applications to data flow analysis.

Control flow analysis or typed programming languages is considered in the part of the book devoted to type and effect systems. Semantic soundness and other theoretical properties for introduced annotated type systems are demonstrated. Type and effect systems with rules for subtyping, polymorphism and recursion with their use in an analysis for tracking side effect, exception analysis and region inference analyses are studied.

From the authors presentation it implies that there is a large amount of commonality among general principles of considered four approaches. Each chapter is appended with mini projects and exercises. The book gives a broad up to date view of general principles and techniques for formal program analysis. The book can be used as a textbook for programming technology courses.

The content of data flow analysis covers the basic techniques for intraprocedural analysis, semantic correctness, monotone frameworks for solving equations, shape analyses.

An alternative to considering equations over program representation is the way of reasoning about programs using constraint systems. Constraint based analysis includes topics covering abstract control flow analysis without taking into account context information (0-CFA), well-definedness of the analysis, coinduction versus induction, semantic correctness and the existence of best solutions, adding data flow analysis to control flow analysis with the purpose to strengthen the quality of the control information.

Abstract interpretation is a methodology for calculating analyses through semantic relations rather than specifying then. From this viewpoint, the authors analyze a notion of correctness for a restricted class of analyses, approximation of fixed points by widening and narrowing operations, Galois connections, induced operations and applications to data flow analysis.

Control flow analysis or typed programming languages is considered in the part of the book devoted to type and effect systems. Semantic soundness and other theoretical properties for introduced annotated type systems are demonstrated. Type and effect systems with rules for subtyping, polymorphism and recursion with their use in an analysis for tracking side effect, exception analysis and region inference analyses are studied.

From the authors presentation it implies that there is a large amount of commonality among general principles of considered four approaches. Each chapter is appended with mini projects and exercises. The book gives a broad up to date view of general principles and techniques for formal program analysis. The book can be used as a textbook for programming technology courses.

Reviewer: Anatoly V.Anisimov (Kyïv)