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

2012-01-14

## 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.

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

• 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.

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

• Introduction to Algorithms

• The Algorithm Design Manual