名称: dafny-verifier
描述: “使用Dafny验证语言构建带有证明的验证程序。”
版本: “1.0.0”
标签: [验证, dafny, 证明, popl]
难度: 中级
语言: [dafny]
依赖: [hoare-logic-verifier, smt-solver-interface]
Dafny验证器
Dafny是一种验证感知的编程语言，支持一起编写规范、程序和证明。它编译成多种语言的验证代码（C#、Java、Go、JavaScript）。
何时使用此技能
- 编写验证程序
- 学习形式化验证
- 证明算法正确性
- 教学程序证明
- 开发认证软件
此技能的作用
- 规范编写：定义前/后条件和不变式
- 验证：自动根据规范验证程序
- 引理证明：编写并证明辅助引理
- 终止性：证明程序终止
- 代码提取：生成验证代码
关键概念
| 概念 |
描述 |
| 方法 |
带有规范的可执行代码 |
| 函数 |
数学函数（纯，无副作用） |
| 引理 |
可以像函数一样调用的证明 |
| 不变式 |
在循环头部保持的属性 |
| 确保 |
后条件规范 |
| 要求 |
前条件规范 |
提示
- 从强规范开始，如果需要再减弱
- 使用引理来分解复杂证明
- 在循环体之前编写循环不变式
- 使用
calc语句进行计算证明
old()函数指代前状态
常见用例
- 验证算法
- 认证库
- 教学形式化方法
- 安全关键代码
- 协议验证
相关技能
hoare-logic-verifier - Dafny背后的理论coq-proof-assistant - 更具表达力的证明助手smt-solver-interface - Z3驱动Dafnyseparation-logician - 用于堆推理
规范参考文献
| 参考文献 |
为何重要 |
| Leino, “Dafny: An Automatic Program Verifier for Functional Correctness” (LPAR 2010) |
Dafny原始论文 |
| Leino, “Program Proofs” (MIT Press, 2023) |
全面的Dafny书籍 |
| Dafny documentation (dafny.org) |
官方参考 |
权衡与限制
方法权衡
| 方法 |
优点 |
缺点 |
| Dafny |
自动，易用 |
表达力有限 |
| Coq |
非常具有表达力 |
手动证明 |
| F* |
更多功能 |
学习曲线陡峭 |
何时不使用此技能
- 当不需要证明时
- 对于低级系统代码（使用Verus）
- 当性能关键时
限制
- 堆推理可能棘手
- 一些证明需要显式引理
- 不如Coq具有表达力
评估标准
高质量的实现应具备：
| 标准 |
要寻找什么 |
| 验证 |
所有证明检查通过 |
| 可读性 |
清晰的规范 |
| 模块性 |
良好的引理结构 |
| 终止性 |
所有循环/函数终止 |
质量指标
✅ 好：所有规范验证，清晰的不变式，模块化引理
⚠️ 警告：一些规范需要手动提示
❌ 差：未验证代码，缺少不变式
研究工具与工件
验证工具：
| 工具 |
语言 |
学习内容 |
| Verus |
Rust |
验证Rust |
| F* |
F* |
验证 |
研究前沿
1. 自动化
实现陷阱
| 陷阱 |
实际后果 |
解决方案 |
| 证明失败 |
验证失败 |
添加引理 |