如何寻找循环不变式？一段计数循环的程序验证疑问

首先看你的代码：

y = 0;
while (y != x) {
    y = y + 1;
}

前置条件x >= 0，后置条件x = y。

你想到的y >= 0 && y <= x其实就是合适且有效的循环不变式，完全满足循环不变式的三个核心要求：

• 初始化成立：程序开头y=0，结合前置条件x>=0，显然0 >=0 && 0 <=x成立。
• 循环体执行后保持：假设进入循环时满足y >=0 && y <=x，且此时y !=x（循环条件成立），说明y <x。执行y = y+1后，y的新值必然满足0 <= y <=x——因为原y <x且x是整数，所以y+1 <=x，同时y始终非负。
• 循环结束推导后置条件：循环终止时y ==x，结合不变式直接得到x=y，完全符合后置条件。

如果想要更精准地体现循环的进展性，也可以把不变式写成0 ≤ y ≤ x ∧ (y == x ∨ 循环尚未终止)，但其实前者已经足够完成程序验证的需求——循环不变式不需要过度复杂，只要能连接前置条件、循环体执行逻辑和后置条件即可。

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