Discovering Likely Method Specifications

It is widely accepted that software specifications are of great use for more rigorous software development. They can be used for formal verification and automated testing. They are essential for precise program understanding. But despite their usefulness, specifications often do not exist in practice. This paper describes a new way to automatically infer specifications from code. Given a modifier method and a set of observer methods, we first symbolically execute the modifier method to obtain a set of execution paths. Then, the conditions and final states of the paths are summarized by observer methods. The result is a likely specification of the modifier method that is compact and human-understandable. The inferred specification 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. Our preliminary experience has been promising. We were able to infer concise specifications for base classes of the .NET platform and found flaws in the design of a new library.