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

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

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

01

算法的正确性

正确性

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

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

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

02

循环不变式

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

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

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

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

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

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

03

证明插入排序的正确性

利用上一节的“循环不变式”,我们证明第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)表明整个数组已经排好序。

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

原文发布于微信公众号 - 人工智能LeadAI(atleadai)

原文发表时间:2017-09-22

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

发表于

我来说两句

0 条评论
登录 后参与评论

相关文章

来自专栏CDA数据分析师

提升R代码运算效率的11个实用方法

众所周知,当我们利用R语言处理大型数据集时,for循环语句的运算效率非常低。有许多种方法可以提升你的代码运算效率,但或许你更想了解运算效率能得到多大的提升。本文...

2178

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

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

2807
来自专栏大数据

概率数据结构简介

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

5406
来自专栏Python小屋

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

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

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

牛课堂算法直播题目

2978
来自专栏TensorFlow从0到N

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

第1篇介绍了插入排序算法,这里要提出一个问题:学习算法仅仅是积累一个又一个的算法实现吗? 当然不是。比算法本身更重要也更基础的,是对算法的分析:能够证明其正确...

3605
来自专栏TechBox

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

1343
来自专栏程序员宝库

LCS 算法:Javascript 最长公共子序列

作者:司徒正美 链接:https://segmentfault.com/a/1190000012864957 最长公共子序列(Longest Common Su...

60510
来自专栏ml

错排公式

错排公式 百科名片 pala提出的问题: 十本不同的书放在书架上。现重新摆放,使每本书都不在原来放的位置。有几种摆法? 这个问题推广一下,就是错排问题: n个有...

4129
来自专栏游戏杂谈

IEEE 754二进制浮点数算术标准

纳尼,不应该是0.1么,怎么变成0.09999999999999998呢?这就要从ECMAScript标准讲起了。

1302

扫码关注云+社区

领取腾讯云代金券