Invariant inference for static checking:
Invariant inference for static checking:
复制标题
静态检查的不变推理：
DOI：
10.1145/587051.587054
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
Michael D. Ernst
中科院分区：
文献类型：
--
作者：
Jeremy W. Nimmer;Michael D. Ernst
静态检查可以验证程序中没有错误，但通常需要书面注释或规格。结果，静态检查可能难以有效使用：很难确定规范并繁琐注释程序。辅助注释过程的自动化工具可以降低静态检查的成本，并使其更广泛地使用。本文描述了对两种技术（一种静态和一种动态）的有效性的评估，以帮助注释过程。我们在三个小程序的程序验证任务中使用ESC/Java进行定量和定性评估41个程序员，并使用Houdini进行静态推理，而Daikon进行动态推理。我们还研究了动态分析中不健全性的效果。统计学上有意义的结果表明，这两种推理工具都改善了任务完成。 Daikon使用户能够表达更正确的不变性；动态分析的不健全性对用户几乎没有阻碍。用户不完美地利用Houdini。访谈表明，初学者发现Daikon有帮助。 houdini是中立的；静态检查具有潜在的实际用途；而且，这两种援助工具都具有独特的好处。我们的观察结果不仅对这两种技术提供了批判性评估，而且还强调了创建未来援助工具的重要考虑因素。
Static checking can verify the absence of errors in a program, but often requires written annotations or specifications. As a result, static checking can be difficult to use effectively: it can be difficult to determine a specification and tedious to annotate programs. Automated tools that aid the annotation process can decrease the cost of static checking and enable it to be more widely used.This paper describes an evaluation of the effectiveness of two techniques, one static and one dynamic, to assist the annotation process. We quantitatively and qualitatively evaluate 41 programmers using ESC/Java in a program verification task over three small programs, using Houdini for static inference and Daikon for dynamic inference. We also investigate the effect of unsoundness in the dynamic analysis.Statistically significant results show that both inference tools improve task completion; Daikon enables users to express more correct invariants; unsoundness of the dynamic analysis is little hindrance to users; and users imperfectly exploit Houdini. Interviews indicate that beginning users found Daikon to be helpful; Houdini to be neutral; static checking to be of potential practical use; and both assistance tools to have unique benefits.Our observations not only provide a critical evaluation of these two techniques, but also highlight important considerations for creating future assistance tools.