不变式和循环不变式

发表于   |   分类于   |  

不变式和循环不变式这一概念在许多的书上都有涉及，从介绍语言的《C++程序设计原理与实践》到讲算法的《算法导论》、《编程珠玑》，都会介绍循环不变式。

不变式

不变式（Invariant）是一个在程序执行过程中永远保持成立的条件。不变式在检测程序是否正确方面非常有用。例如编译器优化就用到了不变式。维基百科上用了MU puzzle的例子来证明不变式是非常有用的。

循环不变式

循环不变式（Loop Invariant）是在循环的第一次迭代前、循环中的每一次迭代和循环结束后都为真的不变式。也可以将循环不变式看作是一个逻辑断言。

《算法导论》中使用循环不变式来证明插入排序的正确性。插入排序由N-1趟排序组成，插入排序的第i趟（i的范围是从1到N-1）都保证了从位置0到位置i-1的元素是已经排序的。从位置0到i-1都是已经排序的，这就可以被称为是插入排序的循环不变式。

循环不变式要能够检测程序，必须具有下面3个性质：

  • 初始化（Initialization）：循环初次执行前，不变式为真。
  • 保持（Maintenance）：循环的迭代
  • 终止（Termination）：When the loop terminates, the invariant gives us a useful property that helps show that the algorithm is correct.

循环不变式和数学归纳法有类似之处。循环不变式的初始化对应数学归纳法的初始步骤，保持对应着数学归纳法的保持步骤。循环不变式与数学归纳法的差别在于循环不变式多了一个终止步骤，终止用于查看循环终止时发生的事件。在插入排序的例子中，终止时所有元素都已排序，所以排序算法是正确的。

一个例子

以二分搜索为例，二分搜索的思想是在一次搜索的过程中，若没有找到目标元素，就将当前的搜索范围减半。二分搜索的思想虽然简单，但要正确运行却并不简单。《TAOCP, Volum 3》中指出第一篇二分搜索论文在1946年发表，但第一个没有错误的二分搜索程序在1962年才出现。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
int binaryFind(const vector<int> &a,int key)
{
	int low = 0, high = a.size() - 1;
	int mid = low + high / 2;
	while(low <= high)
	{
		if(a[mid] > key)
			high = mid - 1;
		else if(a[mid] < key)
			low = mid + 1;
		else if (a[mid] == key)
			return mid;
		mid = low + (high-low) / 2;
	}
	return -1;
}

　　选取不变式

基于二分搜索的思想，我们可以选择出二分搜索的不变式：目标元素key如果在数组x[0…N-1]中，那么key一定在[0，N-1]的范围内。

　　初始化

初始化的时候，low和high分别被初始化为0和N-1。如果key在数组x中，那么key一定在x[0..N-1]中，所以不变式为真。

　　保持

循环中，
1.若a[mid] > key，则key可能存在于a[0,..,mid-1]中。此时将数组缩减一半，key还存在于数组中，循环不变式成立。
2.若a[mid] < key，则key可能存在于a[mid+1,…,high]中。此时数组减小一半，key存在于数组中，循环不变式成立
3.若a[mid] == key，返回下标。循环不变式成立。

　　终止

循环终止时，low>high，key也不存在于数组中。