Jamzy Wang

life is a struggle,be willing to do,be happy to bear~~~

算法正确性证明(循环不变式)

2012-01-14

原创声明:本作品采用知识共享署名-非商业性使用 3.0 版本许可协议进行许可,欢迎转载,演绎,但是必须保留本文的署名(包含链接),且不得用于商业目的。

Problems and Properties

Problem specifications have two parts:

  • the set of allowed input instances
  • the required properties of the algorithm’s output.

Two common traps in specifying the output requirements of a problem

  • One is asking an ill-defined question > Asking for the best route between two places on a map is a silly question unless you define what best means. Do you mean the shortest route in total distance, or the fastest route, or the one minimizing the number of turns?

  • The second trap is creating compound goals > The three path-planning criteria mentioned above are all well-defined goals that lead to correct, efficient optimization algorithms. However, you must pick a single criteria

Demonstrating Incorrectness

The best way to prove that an algorithm is incorrect is to produce an instance in which it yields an incorrect answer. Such instances are called counter-examples Good counter-examples have two important properties:

  • Verifiability > you must be able to: (1)calculate what answer your algorithm will give in this instance (2)display a better answer so as to prove the algorithm didn’t find it.

  • Simplicity > Good counter-examples have all unnecessary details boiled away. They make clear exactly why the proposed algorithm fails.

Induction and Recursion

Failure to find a counterexample to a given algorithm does not mean “it is obvious” that the algorithm is correct. A proof or demonstration of correctness is needed > A computer scientist is a mathematician who only knows how to prove things by induction.

This is partially true because computer scientists are lousy at proving things, but primarily because so many of the algorithms we study are either recursive or incremental. > Mathematical induction is usually the right way to verify the correctness of a recursive or incremental insertion algorithm.

使用循环不变式证明算法的正确性

对于循环不变式(Loop Invariant)必须证明3条性质:

初始化:在循环的第一轮迭代前是正确的; 保持:如果在循环的某一次迭代开始之前是正确的,那么在下一次迭代开始之前,也是正确的; 终止:当循环结束,不变式给了我们一个有用的性质。

循环不变式类似数学归纳法,为了证明某个某条性质,需要证明一个基本情况和一个归纳步。上面第3条的终止性不同于通常使用的数学归纳法的做法,在归纳法中,归纳步是无限地使用的,这里当循环终止时,停止归纳。

下面举两个例子说明:

插入排序(incremental insertion algorithm)

1
2
3
4
5
6
7
8
9
10
11
insertion_sort(item s[], int n)
{
    int i,j; /* counters */
    for (i=1; i<n; i++) {
        j=i;
        while ((j>0) && (s[j] < s[j-1])) {
            swap(&s[j],&s[j-1]);
            j = j-1;
        }
    }
}

证明过程如下:

  • The basis case consists of a single element, and by definition a one-element array is completely sorted.
  • In general, we can assume that the first n − 1 elements of array A are completely sorted after n − 1 iterations of insertion sort.
  • To insert one last element x to A, we find where it goes, namely the unique spot between the biggest element less than or equal to x and the smallest element greater than x. This is done by moving all the greater elements back by one position, creating room for x in the desired location.

递归算法证明(recursive algorithm):

Problem: Prove the correctness of the following recursive algorithm for incrementing natural numbers, i.e. y → y + 1:

1
2
3
4
5
6
Increment(y)
    if y = 0 then return(1) else
    if (y mod 2) = 1 then
        return(2 · Increment(   y/2
        ))
    else return(y + 1)

证明过程如下:

参考

  • Introduction to Algorithms

  • The Algorithm Design Manual

Comments