讨厌算法的程序员 2 - 证明算法的正确性

第1篇介绍了插入排序算法,这里要提出一个问题:学习算法仅仅是积累一个又一个的算法实现吗?

当然不是。比算法本身更重要也更基础的,是对算法的分析:能够证明其正确性,能够理解其效率。这也是自行设计新算法的基础。如果学了一堆算法的实现,而不能判断算法的优劣,或者靠死记硬背记住了各个算法的复杂度等性能指标,那么随着时间的流逝,这一切都是要还给课本的。

算法的正确性

正确性

当我们设计或者实现完成一个算法后,如何证明它是正确的呢?

对于程序员来说,司空见惯的做法是,我们会找几个测试用例,也就是事先定义好的输入输出,然后把输入送进程序里跑一下。如果算法能自动结束,且输出和预期一致,我们就认为算法是ok的。

可是我们无法穷举输入,如何能确定未来的某一输入就一定会有正确的输出呢?靠测试用例是无法保障算法的正确性的。

循环不变式

下面介绍能够证明算法正确性的“循环不变式”。

它的英文名是loop invariant,就是正确的算法在循环的各个阶段,总是存在一个固定不变的特性。找出这个特性并证明其固定不变,从而推断出算法是正确的。

具体的说,必须证明循环不变式满足下面三个性质:

  • 初始化:循环的第一次迭代之前,不变式为真;
  • 保持:循环的某次迭代之前不变式为真,下次迭代之前其仍然为真;
  • 终止:循环终止时,不变式依然成立。

这个过程类似于数学归纳法,为了证明某条性质成立,需要证明一个基本情况和一个归纳步。第一步“初始化”可以对应“基本情况”,第二步“保持”对应于“归纳步”。而第三步“终止”也许是最重要的,因为我们将用终止时循环不变式来证明算法的正确性。

这里定义循环不变式的窍门就是:结合导致循环终止的条件一起定义循环不变式。

证明插入排序的正确性

利用上一节的“循环不变式”,我们证明第1篇中介绍的插入排序的正确性。

对于插入排序,一开始我们就注意到其在玩扑克牌中的应用,这里面有一个关键的认知:我们手中已经摸到的牌始终是排好序的,也就是我们找到的循环不变式:A[1 ‥ j-1]在循环的三个阶段均为有序。无论在循环前,循环中,还是循环后,它都是不变的。

INSERTION-SORT(A)
1 for j = 2 to A.length
2   key = A[j]
3   // Insert A[j] into the sorted sequence A[1..j-1].
4   i = j - 1
5   while i > 0 and A[i] > key
6       A[i + 1] = A[i]
7       i = i - 1
8   A[i + 1] = key

插入排序

证明如下:

  1. 初始化:首先证明在第一次循环迭代之前(当j = 2时),循环不变式成立。此时,A[1 ‥ j-1]中仅由一个元素A[1]组成,“有序性”当然是成立的。从上图中(a)中,有序数组中只有5一个元素;
  2. 保持:其次处理第二条性质:证明每次迭代保持循环不变式。在循环的每次迭代过程中,A[1 ‥ j-1]的“有序性”仍然保持。上图中所有的黑色块左侧子数组永远都是有序的;
  3. 终止:最后研究在循环终止时发生了什么。导致外层for循环终止的条件是j > A.length=n,此时j = n + 1。在循环不变式的表述中将j用n+1代替,那么A[1 ‥ j-1]的“有序性”,就是A[1 ‥ n]有序,这就证明了最终的整个数组是排序好的。上图中(f)表明整个数组已经排好序。

以后,我们还会用到循环不变式来证明其他算法的正确性。

本文参与腾讯云自媒体分享计划,欢迎正在阅读的你也加入,一起分享。

发表于

我来说两句

0 条评论
登录 后参与评论

相关文章

来自专栏落影的专栏

程序员进阶之算法练习(三十)附基础教程

BAT常见的算法面试题解析:程序员算法基础——动态规划程序员算法基础——贪心算法工作闲暇也会有在线分享,算法基础教程-。

2513
来自专栏大数据

概率数据结构简介

在处理大型的数据集时,我们常常进行一些简单的检查,如稀有项(Unique items)的数量、最常见的项,以及数据集中是否存在某些指定的项。通常的做法是使用某种...

5506
来自专栏章鱼的慢慢技术路

牛课堂算法直播题目

2988
来自专栏CDA数据分析师

开工大吉:几个让你月薪3万+的excel神技能

来源:运营圈信息流广告 职场中经常会用到哪些函数? IF函数、SUMIF函数、VLOOKUP函数、SUMPRODUCT函数...... 小编总结了8个在工作中常...

3996
来自专栏一个爱吃西瓜的程序员

每天学习一点儿算法--二分查找

算法是什么? 算法就是完成一组特定任务的方法。 比如将大象放进冰箱需要三步: 打开冰箱 将大象放进冰箱 关闭冰箱 这就是一种算法。 如果用计算机语言来叙述...

3406
来自专栏C语言及其他语言

【每日一题】问题 1102: 明明的随机数

题目描述 明明想在学校中请一些同学一起做一项问卷调查,为了实验的客观性,他先用计算机生成了N个1到1000之间的随机整数(N≤100),对于其中重复的数字,只...

2869
来自专栏Python小屋

Python使用scipy进行多项式计算与符号计算

在扩展库numpy和scipy中都有poly1d,用法一样,实际上是同一个库,scipy是基于numpy的。有图为证 ? 本文代码主要演示如何使用poly1d进...

4916

与机器学习算法有关的数据结构

可能你对经常使用的统计分类包中的功能不满足你的需求而感到不爽,或者你已经有了一个新的数据处理方法。所以,你决定改动现有封装好的算法,开始编写你自己的机器学习方法...

2807
来自专栏TechBox

数据结构与算法系列之时间复杂度前言时间复杂度算法的空间复杂度

1343
来自专栏懒人开发

(1.1)James Stewart Calculus 5th Edition:Four Ways to Represent a Function

一个曲线,在竖直方向,如果对应的一个x值和曲线相交不止一次,就不是一个函数。(其实可以理解成,上面说的,每个 A集合的元素,都有且有一个B集合中的元素和他对应)

1103

扫码关注云+社区

领取腾讯云代金券