一句话：提出自动合成规范的方法与工具 Spyro，在用户给定查询和 DSL 下生成最精确且穷尽的 L-性质。
编写程序规范往往比写代码更难。本文研究自动合成规范的问题：用户提供一个关于一组函数定义的查询，以及一个用于表达待抽取性质的领域特定语言 L（称 L-性质）。方法为在每个查询下合成“最佳”L-性质，即不存在严格更精确的 L-性质，并保证合成出的 L-性质集合是穷尽的，不能再加入新的 L-性质使合取更精确。作者实现工具 Spyro，用户可通过修改查询和 L 定制所需规范。案例表明 Spyro 可用于程序规范挖掘、执行抽象域操作以及合成程序模块的代数性质等应用。
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.