Tool-Assisted Loop Invariant Development and Analysis
Tool-Assisted Loop Invariant Development and Analysis
复制标题
工具辅助循环不变开发和分析
DOI：
10.1109/cseet.2016.28
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
M. Sitaraman
中科院分区：
文献类型：
--
作者：
Caleb Priester;Yu;M. Sitaraman
识别一个适当的不变量是有价值的推理的正确性，涉及一个循环，非正式或正式。几乎每一个现代的自动化验证系统都要求程序员用断言来注释他们的代码，比如不变量，以促进自动化。但是许多学习者很难掌握如何得到一个断言，这个断言保持不变，并且足够强大，可以证明依赖于循环结果的后续断言。本研究的目的是提出一种方法，以帮助理解学生在开发合适的循环不变式时所面临的困难，并帮助他们在这个过程中。我们描述的结果，从实验中的软件工程教室，学生负责开发验证基于组件的代码使用基于Web的前端验证编译器。我们在后台收集数据，因为学生们试图在课堂活动和带回家的项目中使用循环不变式生成经过验证的代码。初步结果显示了我们可以期待看到什么样的信息，以及什么样的反馈可能是有用的。
Identification of an adequate invariant is valuable for reasoning about the correctness of code involving a loop, informally or formally. Almost every modern system for automated verification demands that programmers annotate their code with assertions, such as invariants to facilitate automation. But many learners struggle to grasp how to arrive at an assertion that remains an invariant and is sufficiently strong to prove subsequent assertions reliant on the outcome of the loop. The objective of this research is to present a method to help understand the difficulties students face in developing suitable loop invariants, and assist them in the process. We describe results from an experimentation in a software engineering classroom where students were charged with developing verified component-based code using a web-based front end for a verifying compiler. We collected data in the background as students attempted to produce verified code with loop invariants in in-class activities and take-home projects. Initial results show what kinds of information we can expect to see and what kinds of feedback might be useful.