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 posed about a set of function definitions, and ii) a domain-specific language L in which the extracted property is to be expressed (we call properties in the language L-properties). Each of the property is a best L-property for the query: there is no other L-property that is strictly more precise. Furthermore, the set of synthesized L-properties is exhaustive: no more L-properties can be added to it to make the conjunction more precise. We implemented our method in a tool, Spyro. The ability to modify both the query 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.

翻译：每个程序都应附带一份描述代码行为重要方面的规范，但编写好的规范往往比编写代码本身更困难。本文研究了在用户提供的两类输入指导下自动合成规范的问题：i) 针对一组函数定义提出的查询，以及 ii) 用于表达所提取属性的领域特定语言 L（我们将 L 语言中的属性称为 L 属性）。每个属性都是针对查询的最佳 L 属性：不存在其他严格更精确的 L 属性。此外，合成得到的 L 属性集合是穷尽的：无法向该集合中添加更多 L 属性以使合取式更精确。我们将该方法实现为工具 Spyro。通过修改查询和 L 的能力，Spyro 用户可以自定义待合成规范的种类。我们利用这一能力展示了 Spyro 可应用于多种场景，例如挖掘程序规范、执行抽象域操作以及合成程序模块的代数性质。