找到算法的循环不变量

Posted 2023-02-21

【中文标题】找到算法的循环不变量

【英文标题】：finding the loop invariant for an algorithm

【发布时间】：2021-02-28 19:03:45

【问题描述】：

我在寻找以下算法的不变量时遇到了一些问题。此外，我必须按照所有步骤来证明我如何找到特定的不变量，但我不知道如何证明这一点。 我看到这个算法是加法乘法。

算法是：

alg1(integer a,b)
 x<-a
 y<-b
 z<-0
 while y>0 do
   z<-z+x
   y<-y-1
 end while
 return z

我希望有人可以帮助我分享一些关于这方面的信息，因为我在这里找到的类似案例还不够。

非常感谢您抽出宝贵时间。

【问题讨论】：

请至少格式化您的代码

没有循环不变量。有许多。但只有少数（甚至可能只有一个）对正确性证明有用。

【参考方案1】：

提示：

循环体显示 z 从零增加 x，而 y 以单位减少到零。因此，z + x y 可能是常数...

【参考方案2】：

循环不变量：在第 k 次迭代开始时，value of z is k-1 multiplied by x.

证明正确性：初始化 一开始，k=1，所以

z= (1-1) * x
z= 0 *z=0

维护 如果在第 k 次迭代开始时，z =(k-1)x，其中 k-1

终止： 在终止时，

k=y+1: 
z=(y+1)-1 * x
z=yx

z 成为 y 和 x 的乘积

【讨论】：

需要一点说明，我不明白