使用 Dafny 开发验证程序以评估易用性的案例研究

形式化验证技术旨在针对形式化规约正式证明计算机程序的正确性，但应用形式化规约与验证技术所需的专业知识和工作量以及可扩展性问题限制了其实际应用。近年来，SAT 和 SMT 求解器的巨大进展使得新一代工具的构建成为可能，这些工具有望通过自动化大部分乃至全部验证过程，使软件工程师更容易进行形式化验证。Dafny 系统是这一趋势的突出代表。然而，关于其易用性的证据甚少。为填补这一空白，我们开展了一组 10 个案例研究，用 Dafny 开发一些真实世界算法和数据结构的验证实现，以确定其对软件工程师的易用性。我们发现，平均而言，为规约和验证目的编写的代码量与为实现和测试目的编写的传统代码量处于同一数量级（比率为 1.14）——这一“开销”对于高完整性软件无疑是值得的。Dafny 验证器的性能令人印象深刻，平均每条编写的代码行生成 2.4 个证明义务，每个生成并验证的证明义务平均耗时 24 毫秒。然而，我们也发现编写辅助验证代码所需的手工工作可能相当可观且难以预测和掌握。因此，验证任务的进一步自动化与系统化是该领域未来发展的可能方向。