程序和后置条件中具有未知变量的霍尔三元组的有效性？

如何解决程序和后置条件中具有未知变量的霍尔三元组的有效性？

我不确定这个霍尔三元组中 x 的值：{ a = 0 } while (x > a) do (x := x − 1) { x = 0 }。

关于如何证明这个 Hoare 三元组是否有效，我有 2 个潜在的想法：

• 假设 x 为 0，Hoare 三元组有效，或者
• 假设 x 是任意值，我们将其分解为多个情况并得出结论，Hoare 三元组不适用于 x 的所有值

上述方法中的任何一种都有效，还是我应该采用另一种方法？