Learning Loop Invariants
Learning Loop Invariants
复制标题
学习循环不变量
DOI：
10.1145/3328778.3372715
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Fowler, Megan
中科院分区：
文献类型：
--
作者：
Fowler, Megan
开发正确代码（按指定功能运行的代码）的一个方面是使用合适的不变量注释循环。循环不变量对人类推理很有用，对工具辅助的自动推理也是必要的。编写循环不变量对所有学生来说都是一项艰巨的任务，尤其是刚开始学习软件工程的学生。在帮助学生学会写足够的不变量时，我们不仅需要了解他们犯了什么错误，还要了解他们为什么会犯这些错误。这张海报讨论了使用由RESOLVE验证引擎支持的Web IDE来帮助学生开发循环不变量和收集性能数据。除了收集提交的不变的答案，学生被要求提供他们的步骤或思考过程，关于他们如何到达他们的答案，为每个提交。然后使用混合方法分析答案和原因。结果类别的答案表明，学生能够使用正式的方法概念，他们已经熟悉，如前置和后置条件作为一个起点，以开发足够的循环不变式。此外，在学习写不变量的一些常见的麻烦点被确定。研究结果将有助于指导课堂教学和自动辅导。
One aspect of developing correct code, code that functions as specified, is annotating loops with suitable invariants. Loop invariants are useful for human reasoning and are necessary for tool-assisted automated reasoning. Writing loop invariants can be a difficult task for all students, especially beginning software engineering students. In helping students learn to write adequate invariants, we need to understand not only what errors they make, but also why they make them. This poster discusses the use of a Web IDE backed by the RESOLVE verification engine to aid students in developing loop invariants and to collect performance data. In addition to collecting submitted invariant answers, students are asked to provide their steps or thought processes regarding how they arrived at their answers for each submission. The answers and reasons are then analyzed using a mixed-methods approach. Resulting categories of answers indicate that students are able to use formal method concepts with which they are already familiar, such as, pre and post-conditions as a starting place to develop adequate loop invariants. Additionally, some common trouble spots in learning to write invariants are identified. The results will be useful to guide classroom instruction and automated tutoring.