如何找到循环不变量并证明正确性？答案

【问题标题】：How to find the loop invariant and prove correctness?如何找到循环不变量并证明正确性？
【发布时间】：2023-10-04 09:04:01
【问题描述】：

int i, temp; 
a is an array of integers [1...100] 

i = 1; 

while i < 100 
    if a[i] > a[i+1] 
        temp = a[i]
        a[i] = a[i+1]
        a[i+1] = temp 
    i = i+1

我无法理解如何找到循环不变量并为它们编写正式语句。因此，循环不变量只是在循环的每次迭代之前和之后立即为真的条件。看起来代码正在执行交换：如果数组中的以下元素大于当前元素，则切换位置。我的意思是从循环不变量的定义来看，它听起来真的是 i

【问题讨论】：

“Accelerated C++”一书帮助我理解了“循环不变”术语。也许你应该试一试。它位于“第 2 章：循环和计数”中。
这样看：你写循环的时候在想什么？

标签： algorithm loops proof loop-invariant proof-of-correctness

【解决方案1】：

按照你的定义，我可以看到两个循环不变条件：

1. i < 100
2. a[i] = greater than a[j] for all j < i, where i is the loop variable.

这实际上是冒泡排序的一种外循环迭代。在这个循环结束时，数组中的最大值冒泡到顶部（a[100]） .

【讨论】：

【解决方案2】：

粗略地说，你是对的。循环不变量是“只是在循环的每次迭代之前和之后立即为真的条件”。然而，在这个定义下，对于所讨论的代码，实际上存在无限数量的循环不变量，其中大多数都没有特别的意义。例如，i

但是，通常我们不会仅仅为了找到循环不变量而简单地找到循环不变量。相反，我们感兴趣的是证明程序正确，如果我们想证明程序正确，那么精心挑选的循环不变量将非常有用。

例如，有问题的代码是冒泡排序算法的内部循环，其目的是使数组“更有序”。因此，为了证明这段代码的完全正确性，我们必须证明三件事：

(1) 当执行到代码末尾时，数组是代码开头的数组的排列。 (2) 当执行到代码末尾时，数组的反转数要么为零，要么小于代码开头的数组反转数（这个条件帮助我们证明外层冒泡排序算法的循环终止）。 (3) 代码终止。

为了证明 (1)，我们需要考虑三个执行路径（当我们考虑 PATH 2 时，循环不变量将发挥关键作用）。

(PATH 1) 考虑当执行从代码的开头开始并第一次到达循环顶部时会发生什么。由于在此执行路径上没有对数组进行任何操作，因此该数组是代码开头的数组的排列。

(PATH 2) 现在考虑当执行从循环顶部开始、绕过循环并返回到循环顶部时会发生什么。如果 a[i] a[i+1] 则交换确实发生。但是，数组仍然是代码开头的数组的排列（因为交换是一种排列）。因此，每当执行到循环的顶部时，数组就是代码开头的数组的排列。请注意，“数组是代码开头的数组的排列”语句是我们需要帮助我们证明代码正确的精心选择的循环不变量。

(PATH 3) 最后，考虑一下当执行从循环顶部开始但没有进入循环而是进入代码末尾时会发生什么。由于在此执行路径上没有对数组进行任何操作，因此该数组是代码开头的数组的排列。

这三个路径涵盖了执行从代码开头到代码结尾的所有可能方式，因此，我们证明了（1）代码末尾的数组是数组的排列在代码的开头。

【讨论】：

【解决方案3】：

循环不变量是一些谓词（条件），它适用于每个循环的迭代，这在之前和之前必然是正确的在循环的每次迭代之后立即进行。

当然可以有无限多的循环不变量，但是循环不变量属性用于证明算法的正确性这一事实限制了我们只考虑所谓的“有趣的循环不变量”。

您的程序的目的是对给定的数组进行排序，它是一个简单的冒泡排序。

Goal Statement: The array a is sorted at the end of while loop
Some interesting properties can be like: At the end of ith iteration, a[0:i] is sorted, which when extended to i=100, results in the whole array being sorted.

Loop Invariant for your case: a[100-i: 100-1] is sorted

请注意，当 i 等于 100 时，上述语句意味着整个数组已排序，这就是您希望在算法结束时实现的结果。

PS：刚刚意识到这是一个老问题，无论如何有助于提高我的回答能力:)

【讨论】：

【解决方案4】：

您的循环由测试i < 100 控制。在循环体中，i 在多个地方使用，但只分配在一处。赋值总是发生，对于任何允许进入循环的i 值，赋值将收敛于终止条件。因此循环保证终止。

至于您的程序的正确性，这是另一个问题。根据您的数组是使用从零开始的索引还是从一开始的索引，您使用i 进行数组访问的方式可能会出现问题。如果它是从零开始的，那么您永远不会查看第一个元素，并且您将在最后一次迭代中使用 a[i+1] 越界。

【讨论】：