找到算法的循环不变量答案

【问题标题】：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 的乘积

【讨论】：