0 
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 < 100 因为循环运行必须是这样，但我不太明白。非常感谢一些澄清。

4

4 回答 4

2

根据您的定义，我可以看到两个循环不变条件：

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

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

于 2013-12-03T17:27:11.687 回答
1

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

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

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

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

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

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

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

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

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

于 2014-09-25T16:01:20.487 回答
0

循环不变量是对循环的每次迭代都成立的谓词（条件），在循环的每次迭代之前和之后都必须立即为真。

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

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

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：刚刚意识到这是一个老问题，无论如何有助于提高我的回答技巧:)

于 2018-02-17T07:48:56.533 回答
-1

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

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

于 2013-12-03T18:34:27.927 回答