SHF: Small: Interacting to Specify Software

University Of California-Los Angeles, Los Angeles CA

Investigators

Abstract

All sectors of our society rely on the proper functioning of software. While many tools exist to help software developers ensure important functional, security, and performance properties of their software, these tools generally require developers to provide a specification of the desired properties. Unfortunately writing specifications today is a tedious, error-prone, and costly proposition. Specifications are software artifacts in their own right, yet developers have almost no support in creating and evolving them. Therefore, developers tend to write highly simple or incomplete specifications, if they write specifications at all. This project aims to address that problem by producing techniques and tools that aid and incentivize developers in creating and maintaining high-quality specifications. The new techniques will lead to improved software quality and maintainability, and the associated tools will be made available for use by both other researchers as well as practitioners. The research focuses on two kinds of specifications: logical specs which are traditional pre/post conditions, and structural specs which are essentially boilerplate code patterns. The same principles will be followed for both kinds of specifications: a language will be defined to make the specifications highly expressive, and analysis-driven interactions with the programmer will be used to elicit and refine the specifications. Techniques will be used from code synthesis and dynamic invariant detection. A novel query language will enable programmers to interrogate their specifications. The approach will be fundamentally interactive, leveraging human judgment to guide the construction of high-quality specifications, where the user is iteratively asked specific questions targeted at improving the correctness and completeness of generated specifications.