name: 循环不变式生成器 description: 自动生成并验证算法正确性证明中的循环不变式 allowed-tools:
- Bash
- Read
- Write
- Edit
- Glob
- Grep metadata: specialization: 计算机科学 domain: 科学 category: 算法分析 phase: 6
循环不变式生成器
目的
提供专家指导，使用形式化方法生成和验证算法正确性证明中的循环不变式。
能力
- 从代码结构推断候选循环不变式
- 验证初始化、保持和终止条件
- 生成形式化证明模板
- 处理嵌套循环和复杂数据结构
- 导出到定理证明器（Dafny, Why3）
- 建议不变式强化
使用指南
- 代码分析：分析循环结构并识别关键属性
- 候选生成：从代码模式生成候选不变式
- 验证：检查初始化、保持、终止
- 强化：精炼不变式以证明所需属性
- 导出：为定理证明器生成证明义务
工具/库
- Dafny
- Why3
- SMT求解器（Z3, CVC5）
- 静态分析框架