《架构整洁之道》之结构化编程

一、可推导性

Dijkstra很早就得出的结论是:编程是一项难度很大的活动。一段程序无论复杂与否,都包含了很多的细节信息。如果没有工具的帮助,这些细节的信息是远远超过一个程序员的认知能力范围的。而在一段程序中,哪怕仅仅是一个小细节的错误,也会造成整个程序出错。

Dijkstra提出的解决方案是采用数学推导方法。他的想法是借鉴数学中的公理、定理、推论和引理,形成一种欧几里得结构。Dijkstra认为程序员可以像数学家一样对自己的程序进行推理证明。换句话说,程序员可以用代码将一些已证明可用的结构串联起来,只要自行证明这些额外代码是正确的,就可以推导出整个程序的正确性。

二、goto是有害的

三、功能性降解拆分

既然结构化编程范式可将模块递归降解拆分为可推导的单元,这就意味着模块也可以按功能进行降解拆分。这样一来,我们就可以将一个大型问题拆分为一系列高级函数的组合,而这些高级函数各自又可以继续被拆分为一系列低级函数,如此无限递归。更重要的是,每个被拆分出来的函数也都可以用结构化编程范式来书写。

一词为理论基础,在20世纪70年代晚期到80年代中期出现的结构化分析与结构化设计工作才能广为人知。

通过采用这些技巧,程序员可以将大型系统设计拆分为模块和组件,而这些模块和组件最终可以拆分为更小的、可证明的函数。

四、形式化证明没有发生

大部分人不会真正按照欧几里得结构为每个小函数书写冗长复杂的正确性证明过程。

没有几个程序员会认为形式化验证是产出高质量软件的必备条件。

形式化的、欧几里得式的数学推导证明并不是证明结构化编程正确性的唯一手段。

五、科学来救场

科学和数学在证明方法上有着根本性的不同,科学理论和科学定律通常是无法被证明的,譬如我们并没有办法证明牛顿第二运动定律F=ma或者万有引力定律F=Gm1m2/r的二次方是正确的,但我们可以用实际案例来演示这些定律的正确性,并通过高精度测量来证明当相关精度达到小数点后多少位时,被测量对象仍然一直满足这个定律。但我们始终没有办法像用数学方法一样推导出这个定律。而且,不管我们进行多少次正确的实验,也无法排除今后会存在某一次实验可以推翻牛顿第二运动定律与万有引力定律的可能性。

这就是科学理论和科学定律的特点:它们可以被证伪,但是没有办法被证明。

最终,我们可以说数学是要将可证明的结论证明,而与之相反,科学研究则是要将可证明的结论证伪。

六、测试

Dijkstra曾说过”测试只能展示Bug的存在,并不能证明不存在Bug”,换句话说,一段程序可以由一个测试来证明其错误性,但是却不能被证明是正确的。测试的作用是让我们得出某段程序已经足够实现当前目标这一结论。

软件开发虽然看起来是在操作很多数学结构,其实不是一个数学研究过程。恰恰相反,软件开发更像是一门科学研究学科,我们通过无法证伪来证明软件的正确性。

结构化编程范式促使我们先将一段程序递归降解为一系列可证明的小函数,然后再编写相关的测试来试图证明这些函数是错误的。如果这些测试无法证伪这些函数,那么我们就可以认为这些函数是足够正确的,进而推导整个程序是正确的。

七、小结

结构化编程范式中最有价值的地方就是,它赋予我们创造可证伪程序单元的能力。

这就是为什么现代编程语言一般不支持无限制的goto语句。更重要的是,这也是为什么在架构设计领域,功能性降解拆分仍然是最佳实践。

无论在哪一个层面上,从最小的函数到最大的组件,软件开发的过程都和科学研究非常类似,它们都是由证伪驱动的。软件架构师需要定义可以方便地进行证伪(测试)的模块、组件以及服务。为了达到这个目的,他们需要将类似结构化编程的限制方法应用在更高的层面上。

文章目录
  1. 一、可推导性
  2. 二、goto是有害的
  3. 三、功能性降解拆分
  4. 四、形式化证明没有发生
  5. 五、科学来救场
  6. 六、测试
  7. 七、小结