python - 循环迭代程序正确性示例 - 循环不变量和程序终止

Question

我需要帮助证明迭代程序的正确性：

def term_ex_2(x,y):
 ''' Pre: x and y are natural numbers '''
 a = x
 b = y
 while a >= 0 or b >= 0:
     if a > 0:
         a -= 1
     else:
         b -= 1
 return x * y

我知道我需要以某种方式找到一个循环不变量并通过对循环的归纳来证明它。问题是这里的 if/else 语句让我不知道如何想出一个。

我还必须证明程序在那之后是否终止。

我对分步过程有一个大致的了解，但我不知道从作业中从哪里开始这个例子。

任何建议将被认真考虑。

标签： pythoncorrectnessproof-of-correctness

Answer 1

请注意，在外部循环的每次while迭代中，要么a或b减 1。

因为x和y被假定为自然数，所以它们最初都是> 0。

循环不变量：（ a >= 0可能还有其他可能性！）

此外，程序不会终止，这从上面的循环不变量中非常明显，因为它强制while循环评估为true始终。

证明草图：只要a > 0，循环不断递减a，直到达到0。然后else条件开始执行，b随着循环一次又一次地迭代，a == 0它会一直递减。while

将循环不变量本身放在循环终止条件中以使循环无限循环的经典用法！