Integrating tools and methods for rigorous analysis of C++ generic library components

This thesis presents a new program analysis methodology called dynamic verification, applicable to C++ generic algorithms. It includes dynamic formal verification, specification-based testing, and fast-prototyping, all at a meta-level and a support system (MELAS). The MELAS specification method allows specifications to be executed in the program execution environment. Dynamic verification integrates formal methods and traditional software development methods on the basis of behavioral abstraction. The formal methods we use include a concept specification system and rule-based inference engines derived from the concept specifications, each of which captures the general properties of an abstract notion used in generic software components; the use of the behavioral abstraction allows the generic algorithm be analyzed at a meta-level. The interpretation of the semantics of programming language constructs is left to a conventional compiler. The semantics defined in inference engines and that defined in the compiler are combined through special data types (C++ classes), called Run-time Analysis Oracles (RAOs). A RAO object holds symbolic values, but its functions communicate with inference engines to obtain the semantics for primitive concepts. By using RAOs as type parameters to instantiate generic functions, one can execute the functions with symbolic inputs.; The analysis environment for dynamic verification is a debugger, in which the symbolic execution can be controlled with the debugging commands, breakpoints can be set and attached with MELAS specifications, and the attached specifications can be evaluated separately in the debugger according to the analysis mode and the process model defined in an analysis controller (a debugger command program). The multiple path coverage needed by the verification is achieved through the cooperation of the analysis controller and a database system.; The testing method supported by dynamic verification allows a generic function to be tested at an abstract level; since symbolic values are used, the testing method also covers larger parts of the state space than traditional methods do. Our dynamic formal verification method is strong enough to formally verify STL-style C++ generic functions without having to transform them. Both the testing and the verification methods are non-intrusive, since specifications are evaluated separately from the programs under analysis.