含未知变量x的Hoare三元组有效性验证思路咨询

待验证的目标三元组为：{ a = 0 } while (x > a) do (x := x − 1) { x = 0 }

两种待选思路的可行性判断 #

• 仅假设x取0值时验证三元组有效性
  该思路无法支撑严谨的有效性证明。Hoare三元组的有效判定要求是：所有满足前置条件的初始状态下，程序执行终止后必然满足后置条件。单独验证x=0的特例，只能证明这一个特殊场景下的逻辑成立，完全没有覆盖其他初始状态，属于以偏概全，甚至根本发现不了其他场景下的逻辑漏洞。
• 假设x取任意值，通过分情况讨论推导三元组的普适性
  该思路完全可行，也是符合形式化验证逻辑的正确路径。

分场景验证推导 #

该三元组的前置条件仅约束了a=0，没有对初始状态下x的取值做任何限制，覆盖所有可能的x取值分情况讨论：

• 初始x为正整数：循环会每次将x减1，直到x和a相等（即x=0）时退出，最终满足x=0的后置条件。
• 初始x=0：循环判断条件x > a即0 > 0不成立，直接跳过循环体，最终x=0，满足后置条件。
• 初始x为负数：循环判断条件x > a即负数大于0永远不成立，直接跳过循环体，最终x保持初始的负值，完全不满足x=0的后置要求。
• 若程序变量为非整数类型、初始x取正的非整数值：循环会持续将x减1，直到x小于a=0时才退出，最终x的取值会是负的非整数，同样不符合后置条件要求。

基于以上讨论可以明确：这个Hoare三元组不具备全局有效性，因为存在大量满足前置条件、但程序执行后无法满足后置条件的初始状态。

通用的循环类Hoare三元组验证方法 #

验证包含循环结构的Hoare三元组，需要严格遵循Hoare逻辑的循环推理规则：

1. 梳理循环逻辑，找到适配的循环不变式，保证循环每次执行前后不变式都恒成立
2. 证明初始的前置条件可以推导出循环不变式在循环开始前成立
3. 证明循环执行完一轮后，循环不变式依然成立
4. 证明循环退出时（即循环判断条件不成立时），循环不变式和循环退出条件共同成立，可以直接推出后置条件
5. 额外验证循环必然能够终止，不存在死循环的可能

回到本例，原三元组之所以验证不通过，核心问题是前置条件缺失了对x取值的约束——如果补充前置条件为{ a = 0, x >= 0 且 x为整数 }，这个三元组才能满足有效性要求。

内容的提问来源于stack exchange，提问作者Aryan Agrawal