Discovering Likely Method Specifications

From FSL
Jump to: navigation, search

Nikolai Tillmann and Feng Chen and Wolfram Schulte
ICFEM'06, to appear in LNCS, 2006
Abstract. Software specifications are of great use for more rigorous software development. They are useful for formal verification and automated testing, and they improve program understanding. In practice, specifications often do not exist and software is implemented in an ad-hoc fashion. We describe a new way to automatically infer specifications from code. Given the code of a set of methods, our approach infers a likely specification for any method such that the method's behavior, i.e.\ its effect on the state and possible result values, is summarized and expressed in terms of some other methods. We use symbolic execution to analyze and relate the behaviors of the considered methods. In our experiences, the resulting likely specifications are compact and human-understandable. They can be examined by the user, used as input to program verification systems, or as input for test generation tools for validation. We implemented the technique for .NET programs in a tool called Axiom Meister. It inferred concise specifications for base classes of the .NET platform and found flaws in the design of a new library.

Personal tools