Every program should always be accompanied by a specification that describes important aspects of the code's behavior, but writing good specifications is often harder that writing the code itself. This paper addresses the problem of synthesizing specifications automatically. Our method takes as input (i) a set of function definitions, and (ii) a domain-specific language L in which the extracted properties are to be expressed. It outputs a set of properties--expressed in L--that describe the behavior of functions. Each of the produced property is a best L-property for signature: there is no other L-property for signature that is strictly more precise. Furthermore, the set 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. When given the reference implementation for a variety of SyGuS and Synquid synthesis benchmarks, spyro often synthesized properties that that matched the original specification provided in the synthesis benchmark.

翻译：每个程序都应附带描述代码行为重要方面的规范，但编写优质规范往往比编写代码本身更具挑战性。本文研究自动合成规范的问题。我们的方法输入包括：（i）一组函数定义，以及（ii）用于表达提取属性的领域特定语言L。其输出是用L表达的、描述函数行为的一组属性。每个生成的属性都是该签名下的最佳L属性：不存在其他针对同一签名的L属性具有严格更高的精确度。此外，该属性集是完备的：无法向其中添加更多L属性以增强合取式的精确度。我们将该方法实现为工具spyro。在针对多种SyGuS和Synquid合成基准测试的参考实现进行测试时，spyro经常能合成与原始基准规范完全匹配的属性。