SHF: Small: Interacting to Specify Software

我们社会的所有部门都依赖于软件的正常运行。虽然存在许多工具来帮助软件开发人员确保其软件的重要功能、安全性和性能属性，但这些工具通常要求开发人员提供所需属性的规范。 不幸的是，今天编写规范是一个乏味的、容易出错的、代价高昂的提议。规格说明本身就是软件工件，但是开发人员几乎不支持创建和发展它们。因此，开发人员倾向于编写非常简单或不完整的规范，如果他们编写规范的话。 该项目旨在通过产生技术和工具来解决这个问题，这些技术和工具可以帮助和激励开发人员创建和维护高质量的规范。 新技术将导致提高软件质量和可维护性，相关的工具将提供给其他研究人员以及practitioners.The研究集中在两种规格：逻辑规格，这是传统的前/后条件，和结构规格，这本质上是样板代码模式。这两种规格说明将遵循相同的原则：将定义一种语言，使规格说明具有高度的表达性，并与程序员进行分析驱动的交互，以引出和细化规格说明。技术将使用从代码合成和动态不变检测。一种新的查询语言将使程序员能够查询他们的规范。 该方法将从根本上是交互式的，利用人类的判断来指导高质量规范的构建，其中用户被反复询问针对提高生成的规范的正确性和完整性的特定问题。

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.