讨厌算法的程序员 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 条评论
登录 后参与评论

相关文章

来自专栏TensorFlow从0到N

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

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

2785
来自专栏大数据

大数据图:循环点阵

本文的内容最初由Marko Rodriguez和Bobby Norton在Aurelius博客上共同撰写。

1955
来自专栏Grace development

一道看似简单的面试题

这样看似简单的一个面试题, 实际牵出了很多基础知识,本章在为大家补习基础知识的情况下来解答这道题。先亮出答案

362
来自专栏用户2442861的专栏

几种常见计算机图像处理操作的原理及canvas实现

即使没有计算机图形学基础知识的读者也完全不用担心您是否适合阅读此文,本文的性质属于科普文章,将为您揭开诸如Photoshop、Fireworks、GIMP等软...

651
来自专栏冰霜之地

高效的多维空间点索引算法 — Geohash 和 Google S2

每天我们晚上加班回家,可能都会用到滴滴或者共享单车。打开 app 会看到如下的界面:

1675
来自专栏NewbieWeb

ThreeJS简易魔方自动还原实现(一)层先法

在ThreeJS四步制作一个简易魔方中介绍了怎么实现一个可以转动的简易魔方,接来下准备介绍下怎么让这个简易魔方具备自动还原的功能。

803
来自专栏量化投资与机器学习

CNN预测股票走势基于Tensorflow(思路+程序)

前言 我们希望找出跟随价格上涨的模式。通过每日收盘价,MA,KD,RSI,yearAvgPrice 本次推文研究只是展示深入学习的一个例子。 结果估计不是很好。...

1.7K7
来自专栏PPV课数据科学社区

一小时掌握R语言数据可视化

ggplot2是R语言最为强大的作图软件包,有着自成一派的可视化理念,数据可视化是数据分析的重要一步,让我们通过由浅入深的掌握数据可视化的精髓。 请尊重原创,转...

34912
来自专栏一心无二用,本人只专注于基础图像算法的实现与优化。

超像素经典算法SLIC的代码的深度优化和分析。

     现在这个社会发展的太快,到处都充斥着各种各样的资源,各种开源的平台,如github,codeproject,pudn等等,加上一些大型的官方的开源软件...

31810
来自专栏专知

手把手教你构建ResNet残差网络

4082

扫码关注云+社区