C2S: translating natural language comments to formal program specifications
C2S: translating natural language comments to formal program specifications
复制标题
DOI：
10.1145/3368089.3409716
复制
发表时间：
2020-11
期刊：
影响因子：
--
通讯作者：
Juan Zhai;Yu Shi;Minxue Pan;Guian Zhou;Yongxiang Liu;Chunrong Fang;Shiqing Ma;Lin Tan;X. Zhang
中科院分区：
文献类型：
--
作者：
Juan Zhai;Yu Shi;Minxue Pan;Guian Zhou;Yongxiang Liu;Chunrong Fang;Shiqing Ma;Lin Tan;X. Zhang
正式的程序规范对于各种软件工程任务至关重要，例如程序验证，程序合成，代码调试和软件测试。但是，手动推断正式的程序规格不仅耗时，而且容易出错。此外，它需要大量的专业知识。自然语言评论包含有关代码行为的丰富语义，使从评论中推断程序规范是可行的。受此启发，我们开发了一个名为C2S的工具，以通过将自然语言注释转换为正式程序规范来自动化规范综合任务。我们的方法首先从现有评论及其相应的规范中构建自然语言单词和规范令牌之间的一致性。然后，对于给定的方法注释，我们的方法组装了与单词相关联的单词，这些令牌是在对规范语法和目标方法上下文指导的规范中的评论中关联的。我们的工具成功地合成了511种不同项目中64个类方法的1,145个规格，其表现大大优于最先进的方法。生成的规格还用于改善许多软件工程任务，例如静态污点分析，该任务证明了规格的高质量。
Formal program specifications are essential for various software engineering tasks, such as program verification, program synthesis, code debugging and software testing. However, manually inferring formal program specifications is not only time-consuming but also error-prone. In addition, it requires substantial expertise. Natural language comments contain rich semantics about behaviors of code, making it feasible to infer program specifications from comments. Inspired by this, we develop a tool, named C2S, to automate the specification synthesis task by translating natural language comments into formal program specifications. Our approach firstly constructs alignments between natural language word and specification tokens from existing comments and their corresponding specifications. Then for a given method comment, our approach assembles tokens that are associated with words in the comment from the alignments into specifications guided by specification syntax and the context of the target method. Our tool successfully synthesizes 1,145 specifications for 511 methods of 64 classes in 5 different projects, substantially outperforming the state-of-the-art. The generated specifications are also used to improve a number of software engineering tasks like static taint analysis, which demonstrates the high quality of the specifications.