DAReing：降低已验证程序的标注开销
软件工程
2017-06-14 v1 计算机科学中的逻辑
摘要
现代程序验证器使用同一统一的程序文本既用于规约也用于实现程序。该程序文本还用于提供必要的指导，以确保程序满足其规约。所需指导的量通常被称为标注开销。这种开销可能很高，常被视为程序验证器广泛使用的障碍，因为它增加了开发时间且指导可能使程序文本变得晦涩。在本文中，我们引入了 DARe 工具，它能为 Dafny 程序验证器自动移除尽可能多的不必要指导。该工具与 Dafny IDE 集成。为了评估 DARe，我们将其应用于 Dafny 库中的 252 个程序，并分析了其能够移除不必要指导的程度。我们的结果非常令人鼓舞，高达 88% 的指导可以被移除。
引用
@article{arxiv.1706.04023,
title = {DAReing to reduce the annotation overheads of verified programs},
author = {Gudmund Grov and Duncan Cameron and Leon McGregor},
journal= {arXiv preprint arXiv:1706.04023},
year = {2017}
}