Loop invariant

第三版的算法导论相对于第二版做了不小的改动。其中之一是进一步强调了算法中 loop invariant 的重要性。

Loop invariant 在 Knuth 的 The Art of Computer Programming 的开头就提到过。简单的说,就是利用 断言(assertion)和 归纳法(induction)来证明算法的正确性。
其形式与数学归纳法相近,主要运用于由 while 循环构成的算法(这是由于循环过程和递归过程的相似性决定的)。首先是,该不变性必须能够帮助证明算法的正确性;接下来,只需要保证在初始情况、和每一次循环之后,这一不变性都能得以保持。这样便证明了整个算法的正确性。

相对于证明正确定,对读者来说,更重要的是这一方法非常适合于理解已有算法和发现新算法。有些算法的中间步骤有些繁杂,但只要把握住循环过程中的某种不变性,并把中间步骤理解成维持该不变性的操作,便能比较简单的掌握这一算法。

其实 loop invariant 只能证明程序的部分正确,要在加上终止的证明,才算是证明程序的完全正确。不管怎么说,无法停机的程序都不能说是正确的吧。

Advertisements
This entry was posted in Science. Bookmark the permalink.

One Response to Loop invariant

  1. rat says:

    为啥我看不懂呢

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s