中国统计网

登录

首页

分类浏览

专题

专栏作者

问答

线下活动

企业招聘

app下载

投稿

注册




讨厌算法的程序员 2 - 证明算法的正确性
头像 黑猿大叔 新手入门
新手入门

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


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



算法的正确性

image.png

正确性


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


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


image.png

插入排序


证明如下:


  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)表明整个数组已经排好序。


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

 

作者:黑猿大叔(中国统计网特邀专栏作者)
链接:http://www.jianshu.com/p/1fffff56d260
來源:简书

 


我要评论
验证码
  • 0
暂无评论

关注公众号

中国统计网微信公众号

微信公众号:cntongji

今日热议

专栏作者

  • 黄成明
    统计网特邀认证作者
    黄成明 ,零售数据分析研究者,拥有15年的销售及数据分析经验,历经美国强生公司、妮维雅公司、雅芳公司和鼎盛时期的诺基亚公司。目前是数据化管理的咨询顾问和培训师。他独立研发了基于周销售权重指数的零售管理模型,可以有效地进行目标管理、销售预测、客流预估、促销评估、销售预警等。
  • 傅一平
    统计网特邀认证作者
    浙江移动大数据中心 数据管理部经理 博士 毕业于浙江大学 10多年数据从业经验,专注于大数据采集、处理、建模、管理、变现及产业等研究
  • tommy
    统计网特邀认证作者
    数据落地应用探索者
  • 秦路
    统计网特邀认证作者
  • 数据海洋
    统计网特邀认证作者
    数据应用的实践者!
  • 数据小兵
    统计网特邀认证作者
    数据分析知名博主,SPSS自学教练,博客www.datasoldier.net
立即下载
版权所有: 统计网. Copyright © 2016 itongji.cn All Rights Reserved. 备案号:ICP备15042641号-3