一句话：提出 C2S，通过从已有注释与规约中学习词-token 对齐，将自然语言注释自动翻译为形式化程序规约。
形式化程序规约对程序验证、合成、调试与测试等任务至关重要，但人工编写耗时、易错且依赖专家经验。自然语言注释包含丰富的代码行为语义。本文提出 C2S，将注释自动翻译为形式化规约：先从已有注释及其对应规约中学习自然语言词与规约 token 之间的对齐关系；给定方法注释后，依据规约语法和目标方法上下文，将注释中词关联的 token 组装成规约。作者在 5 个项目的 64 个类、511 个方法上成功合成 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.
DOI 原文 ·
@inproceedings{paperbot5844,
title = {C2S: translating natural language comments to formal program specifications},
author = {Juan Zhai and Yu Shi and Minxue Pan and Guian Zhou and Yongxiang Liu and Chunrong Fang and Shiqing Ma and Lin Tan and Xiangyu Zhang},
booktitle = {FSE},
year = {2020},
doi = {10.1145/3368089.3409716}
}