从问题单的价值到测试的可证明性

上一篇 / 下一篇  2020-09-19 22:22:36 / 个人分类:测试杂谈

前面几篇文章探讨了问题单价值问题,价值要么是测试主动发现的,要么是被用户发现而变成损失。如果是被用户发现的,那么自然就要面对软件是否正确被发布的问题。

测试无法穷举覆盖,无法发现所有的问题,可以肯定的是问题必然会在软件发布到现网后才暴露。既然软件中肯定会遗留问题,那为什么还要发布呢?当然是在证明了软件的正确性后才发布的,只不过这种证明方式不是数学上的而是科学上的。

《整洁架构》中提到,Dijkstra(发明最短路径算法的那位牛人)很早就得出的结论:编程是一项难度很大的活动。一段程序无论复杂与否,都包含了很多的细节信息。如果没有工具的帮助,这些细节的信息是远远超过一个程序员的认知能力范围的。而在一段程序中,哪怕仅仅是一个小细节的错误,也会造成整个程序出错。他认为采用数学推导方法,借鉴数学中的公理、定理、推论和引理,形成一种欧几里得结构。Dijkstra认为程序员可以像数学家一样对自己的程序进行推理证明。换句话说,程序员可以用代码将一些已证明可用的结构串联起来,只要自行证明这些额外代码是正确的,就可以推导出整个程序的正确性。但这个过程并没有发生:

1)大部分人不会真正按照欧几里得结构为每个小函数书写冗长复杂的正确性证明过程。(没有必要证明几块砖头不同的摆法的正确性,通常情况下只要能填进去就行了。况且编译器为我们做了很多工作)

2)没有几个程序员会认为形式化验证是产出高质量软件的必备条件。(软件工程比形式化证明更重要,特别是大型的软件系统工程能力更重要,严谨数学反而不适用)

3)形式化的、欧几里得式的数学推导证明并不是证明结构化编程正确性的唯一手段。(这一点很关键,说明还有其他的方式——科学而非数学)

   科学和数学在证明方法上有着根本性的不同,科学理论和科学定律通常是无法被证明的,譬如我们并没有办法证明牛顿第二运动定律F=ma或者万有引力定律F=Gm1m2/r的二次方是正确的,但我们可以用实际案例来演示这些定律的正确性,并通过高精度测量来证明当相关精度达到小数点后多少位时,被测量对象仍然一直满足这个定律。但我们始终没有办法像用数学方法一样推导出这个定律。而且,不管我们进行多少次正确的实验,也无法排除今后会存在某一次实验可以推翻牛顿第二运动定律与万有引力定律的可能性。这就是科学理论和科学定律的特点:它们可以被证伪,但是没有办法被证明。(本质上这是一种自然现象的公式化表示,就好比钻木取火,它需要利用至少两个自然现象:一是摩擦产生热量;二是物质在加热到一定程度后就会燃烧。我们没有办法从数学上推到出来摩擦会产生热量的公式,这是一种跳跃式的变化。)

   定理诞生前的一次次试验好比测试执行一个个用例;失败的用例需要修改设计或代码,这好比调整试验的条件或约束;针对遗漏的问题补充测试用例好比提高科学试验的精确度。试验的结果得到一个公式,而用例的执行结果得到一个结论——这段程序或这个模块是正确的(因为根据当前的认知能力已经没有办法证伪了,当然也无法完全排除错误的可能)。当得到多个被证明正确的软件模块后,通过科学的工程化方法将模块组织起来,再次通过一组高层级的用例证伪,如此循环直到将软件组织成最终发布的状态以及无法证伪为止。这时我们可以大声宣布:软件可以发布了。这就是软件的科学证明过程。


TAG: 问题单 测试 价值 证明 证伪 正确性

 

评分:0

我来说两句

我的栏目

日历

« 2024-03-27  
     12
3456789
10111213141516
17181920212223
24252627282930
31      

数据统计

  • 访问量: 2895
  • 日志数: 5
  • 建立时间: 2020-04-19
  • 更新时间: 2020-09-29

RSS订阅

Open Toolbar