---

名称: 不变性分析器 描述: 识别和验证循环不变式以进行正确性证明 允许的工具:

• 读取
• 写入
• 搜索
• 全局匹配

---

不变性分析器技能

目的

识别和验证循环不变式，以帮助构建算法的正确性证明。

能力

• 自动推断循环不变式
• 根据代码验证不变式
• 提取前置条件和后置条件
• 生成形式化证明结构
• 识别缺失的不变式

目标流程

• 正确性证明测试
• 算法实现

不变式分析框架

循环不变式属性

1. 初始化: 在第一次迭代前为真
2. 保持: 如果在迭代前为真，则在迭代后也为真
3. 终止: 在循环结束时提供有用的属性

常见不变式模式

• 范围不变式: “对于所有在 [0, k) 中的 i，属性 P(i) 成立”
• 累加器不变式: “和等于 a[0…k-1] 的和”
• 指针不变式: “left < right 且所有小于 left 的元素都已处理”
• 状态不变式: “数据结构保持属性 X”

输入模式

{
  "type": "object",
  "properties": {
    "code": { "type": "string" },
    "language": { "type": "string" },
    "loopIndex": { "type": "integer" },
    "expectedInvariant": { "type": "string" }
  },
  "required": ["code"]
}

输出模式

{
  "type": "object",
  "properties": {
    "success": { "type": "boolean" },
    "invariants": { "type": "array" },
    "preconditions": { "type": "array" },
    "postconditions": { "type": "array" },
    "proofOutline": { "type": "string" }
  },
  "required": ["success"]
}