Synthesizing Specifications

TL;DR

This paper introduces Spyro, a tool for automatically synthesizing precise and exhaustive program specifications based on user queries and a domain-specific language, enabling diverse applications like mining and algebraic property synthesis.

Contribution

It presents a novel method and tool for automatic, customizable specification synthesis guided by user queries and a domain-specific language.

Findings

Spyro can mine program specifications effectively.

It supports synthesis of algebraic properties of program modules.

The approach is flexible and customizable for various applications.

Abstract

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.