明盒验证

　　明盒正确性验证是用 基于数学的方法证实一个过程与其规范相符。正像一个长除算法的正确性不是依赖除法而是用乘法来验证的一样，过程的正确性验证也不是依赖细化过程来实现的，而是采用其他形式的手段。在净室设计中广泛用到的明盒验证方法被称为函数理论正确性验证。运用函数理论方法，每个控制结构都会与它的预期函数规范相比较。当所有的子控制结构被验证时，整个过程也就被验证了。通常在小组评审中实现验证。

　　正确性定理(Linger, Mills andWitts 1978)为每个明盒控制结构定义了正确性问题，如表4.4所示。不同的控制结构中问题的数目不同：顺序结构是1个、分支结构是2个、而循环结构是3个。由于任何大小的过程都潜在地含有无限多条执行路径，所以不可能通过跟踪路径来验证。不过，过程包含的结构却是有取胜的。通过在有取胜的步骤里验证每个结构，就可以在有阴的步骤里验证每个结构，就可以在有限的步骤里实现系统化的过程验证。正确性问题可应用于多种层次，从口头的证明到详细的书面证明。严格的层次划分决定于风险和回报，这是个商业性问题。经验表明小组评审时进行口头的证明对开发高质量软件是非常有效的。

　　表 明盒控制结构的正确性问题

　　在表中，分析了对应的控制结构中的执行路径后，就可以确定正确性问题了.对顺序结构，惟一的路径是h跟随g，所以正确性问题就是：这些功能结点必须执行这个结构的预期函数?.

　　对ifthen结构，当p真，惟一的路径是g;正确性就是g必须执行?.当p假，惟一的路径为do nothing,正确性就是doing nothing必须执行?.也就是说，?必须在p为假时已经完成.对ifthenelse的分析是类似的，只有p为假时有区别：当p为假时，惟一的路径是h，正确性为h必须执行?.

　　循环结构的正确性难以直接证明.不过，可通过验证一个等价的相对简单的ifthenelse结构来完成对一个可终止的循环的正确性检验，这种ifrhenelse结构是通过对循环的执行路径的变换而得到的.例如，考虑在图4.5的第一个以图形形式显示的whiledo结构.在图下的第二个图的中间，创建了一个等价的ifthenelse，其中用whiletest(p)作为断言.对ifthenelse的真分支，先执行g ，然后是whiledo结构，和原来的whiledo的执行一样.对假分支，什么也不做.也和原来的whiledo的执行一样.因此，这个新ifthenelse结构和上面的whiledo结构是等价的.但我们要求真分支上的whiledo结构与?等价，因此将它替换为?，得到图4.5的第三个图的结构.这样，whiledo的正确性问题就变成了ifrhenelse和顺序结构的正确性问题.通过分析irthenelse的执行就可以解决whiledo的正确性问题.真路径要求g和其后的?必须执行?，假路径是空操作执行?.

　　为解释在条件为真时的正确性问题，考虑如下while do :

　　[read remaining records from file,if any ]

　　while

　　[records remain]

　　do

　　[read next record]

　　enddo

　　正确性问题是：当徨测试为真时，g和其后的?能完成?吗?它被表达为如下：

　　当[records remain]为真，

　　[read next record]和其后的[read remaining records from file,if any ]完成[read remaining records from file,if any]

　　回答为是.因为对于一个初始为不空的文件(由真什断言保证).[read next record](表示为g)就会读取一些数据，然后文件可能为空，也可能不空，而[read remain record](表示?)的功能是读非空文件或对空文件什么也不做.这样如果文件的初始化状态是一样的，新的结构(g和随后的?)就有着和预期函数[read remaining records from file,if any ]有着同样的效果.

　　注意除了whiledo的真假问题以外，第三个问题是循环能否终止，基于循环的单调性最终要导致终止条件为假.例如　，这里的循环从文件中读取连续的记录保证了文件被读完时会终止.对于dountil和dowhiledo的分析是类似的.

原文转自：http://www.ltesting.net