proof - 循环不变性和算法的证明

Question

我将如何获得循环不变量并为以下算法证明它。

power(x,y):
   z = 1
   m = 0
   while m < y:
       z = z*x
       m = m+1
   return z

Answer 1

首先，我认为您的意思是 z = z*x 要显示任何给定循环的循环不变性，您必须提出一个在任何迭代的开始和结束时都不会改变的语句。使用该不变量，您将证明当程序终止时，函数可以工作。你的功能基本上是在尝试做 x^y。

让我们构造一个循环不变量：Z = x^m。您可以看到在循环的开始和结束时都是如此。

你也知道循环只能在 not(m=y, or m =y.

因此，如果 Z=x^m，并且在终止时 m = y。那么 Z = x^y。

所以我们可以看到这个程序是部分正确的。