我不确定x这个 Hoare 三元组中的值：{ a = 0 } while (x > a) do (x := x − 1) { x = 0 }.
对于如何证明这个 Hoare 三元组是否有效，我有 2 个潜在的想法：
- 假设
x为 0，Hoare 三元组有效，或 - 假设
x是任意值，我们将其分解为案例并得出结论，Hoare 三元组并非对所有值都有效x
上述任何一种方法是否有效，还是我应该采取另一种方法？
问问题
38 次
我不确定x这个 Hoare 三元组中的值：{ a = 0 } while (x > a) do (x := x − 1) { x = 0 }.
对于如何证明这个 Hoare 三元组是否有效，我有 2 个潜在的想法：
x为 0，Hoare 三元组有效，或x是任意值，我们将其分解为案例并得出结论，Hoare 三元组并非对所有值都有效x上述任何一种方法是否有效，还是我应该采取另一种方法？