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

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

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

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

2719
来自专栏ml

错排公式

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

3949
来自专栏游戏杂谈

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

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

732
来自专栏大数据

概率数据结构简介

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

4246
来自专栏有趣的Python

py编程技巧-2.5-如何在一个for语句中迭代多个可迭代队象(并行&串行)?

实际案例: 某班学生期末考试成绩,语文,数学,英语分布存储在三个列表当中 同时迭代三个列表,计算每个学生的总分 某年级有四个班,某次考试每班英语成绩分布存储在...

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

牛课堂算法直播题目

2708
来自专栏TechBox

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

1182
来自专栏CDA数据分析师

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

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

3836
来自专栏懒人开发

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

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

983

扫码关注云+社区