Synthesizing Specifications

Every program should be accompanied by a specification that describes important aspects of the code's behavior, but writing good specifications is often harder than writing the code itself. This paper addresses the problem of synthesizing specifications automatically, guided by user-supplied inputs of two kinds: (i) a query Phi posed about a set of function definitions, and (ii) a domain-specific language L in which each extracted property phi(i) is to be expressed (we call properties in the language L-properties). Each of the phi(i) is a best L-property for Phi: there is no other L-property for Phi that is strictly more precise than phi(i). Furthermore, the set {phi(i)} is exhaustive: no more L-properties can be added to it to make the conjunction Lambda(i)phi(i) more precise. We implemented our method in a tool, spyro. The ability to modify both Phi and L provides a spyro user with ways to customize the kind of specification to be synthesized. We use this ability to show that SPYRO can be used in a variety of applications, such as mining program specifications, performing abstract-domain operations, and synthesizing algebraic properties of program modules.