我目前正在努力弄清楚如何证明包含循环的程序是正确的。我在 wp、vc 和 pc 的基础上工作。
有问题的循环是：
wp(while(i<n) i = i+1; | i >= n)
wp(while(true) x=4; |x=4)
“;”之前的所有内容 是程序和“|”之后的所有内容 是后置条件。
我在讲座中听说你必须找到程序的不变量以及终止函数，但我目前并不知道如何直观地做到这一点。我听说你需要训练这个，但我还没有看到一个例子，主要是理论。如果有人可以帮助我解释循环的验证，那将非常好。
我感谢每一点帮助。