Hoare Logic Loop Invariant
我正在研究Hoare Logic，我在理解寻找循环不变量的方法时遇到了问题。
有人可以解释用于计算循环不变量的方法吗？
循环不变量应该包含什么才能成为“有用的”？
我只是处理简单的例子，找到不变量并在例子中证明部分和完整的修正：
{ i ≥ 0 } while i > 0 do i := i−1 { i = 0 }
没有找到相关结果
已邀请:
3 个回复
嗓瑰
{p} while b do S {p^not(b)} <=> {p^b} S {p}{i ≥ 0 ^ i > 0} i := i−1 {i ≥ 0}坝硷操
眠缝