AutoProof验证器：非专家与标准代码上的可用性
软件工程
2015-08-20 v1 人机交互
计算机科学中的逻辑
摘要
形式化验证工具通常由专家为专家开发；因此，它们对于缺乏形式化方法经验的程序员的可用性可能严重受限。本文中，我们结合AutoProof这一工具讨论这一普遍现象：该工具能够验证面向对象软件的全部功能正确性。特别地，我们展示了在代表非专家使用的两种对比情境下使用AutoProof的经验。首先，我们讨论研究生软件验证课程中学生的使用情况，他们被要求验证各种排序算法的实现。其次，我们评估其在验证某本科课程编程作业所开发代码时的可用性。第一种情景代表了严肃非专家的使用；第二种代表了在并非为完整功能验证而开发的“标准代码”上的可用性。我们报告了经验与教训，并从中得出关于进一步提升验证工具可用性开发的一些一般性建议。
引用
@article{arxiv.1508.03895,
title = {The AutoProof Verifier: Usability by Non-Experts and on Standard Code},
author = {Carlo A. Furia and Christopher M. Poskitt and Julian Tschannen},
journal= {arXiv preprint arXiv:1508.03895},
year = {2015}
}
备注
In Proceedings F-IDE 2015, arXiv:1508.03388