[科普中国]-形式程序测试

简介

形式程序测试是指在程序测试中采用形式化方法。形式程序测试可以从形式语义方面设计测试程序，测试程序是否有操作语义、指称语义、代数语义错误。形式程序测试是建立在严格数学基础上，比一般程序测试更科学，更严谨。

形式化方法定义形式概念分析是德国 Will 教授1982 年在数据格理论上通过数据集中对象与属性之间的二元关系建立概念层次结构，生动简洁地体现了概念之间的泛化和特化关系，再运用格代数理论进行研究的分析方法。软件形式化方法是指建立在严格数学基础上的软件开发方法1。形式化方法模型的主要活动是生成计算机软件形式化的数学规格说明。形式化方法使软件开发人员可以应用严格的数学符号来说明、开发和验证基于计算机的系统。 形式化方法的本质是基于数学的方法来描述目标软件系统属性的一种技术。不同的形式化方法的数学基础是不同的，有的以集合论和一阶谓词演算为基础（如Z和VDM），有的则以时态逻辑为基础。形式化方法需要形式化规约说明语言的支持。这样的形式化方法提供了一个框架，可以在框架中以系统的而不是特别的方式刻划、开发和验证系统。如果一个方法有良好的数学基础，那么它就是形式化的，典型地以形式化规约语言给出。这个基础提供一系列精确定义的概念，如：一致性和完整性，以及定义规范的实现和正确性。形式化方法模型的主要活动是生成计算机软件形式化的数学规格说明。形式化方法使软件开发人员可以应用严格的数学符号来说明、开发和验证基于计算机的系统。这种方法的一个变型是净室软件工程（cleanroom software engineering），这一软件工程方法目前已应用于一些软件开发机构。

软件形式化方法的分类根据说明目标软件系统的方式，形式化方法可以分为两类：

面向模型的形式化方法。面向模型的方法通过构造一个数学模型来说明系统的行为。

面向属性的形式化方法。面向属性的方法通过描述目标软件系统的各种属性来间接定义系统行为。

根据表达能力，形式化方法可以分为五类：

基于模型的方法：通过明确定义状态和操作来建立一个系统模型（使系统从一个状态转换到另一个状态）。用这种方法虽可以表示非功能性需求（诸如时间需求），但不能很好地表示并发性。如：Z语言，VDM，B方法等。

基于逻辑的方法：用逻辑描述系统预期的性能，包括底层规约、时序和可能性行为。采用与所选逻辑相关的公理系统证明系统具有预期的性能。用具体的编程构 造扩充逻辑从而得到一种广谱形式化方法，通过保持正确性的细化步骤集来开发系统。如：ITL（区间时序逻辑），区段演算（DC），hoare 逻辑，WP演算，模态逻辑，时序逻辑，TAM（时序代理模型），RTTL（实时时序逻辑）等。

代数方法：通过将未定义状态下不同的操作行为相联系，给出操作的显式定义。与基于模型的方法相同的是，没有给出并发的显式表示。如：OBJ， Larch族代数规约语言等；

过程代数方法：通过限制所有容许的可观察的过程间通信来表示系统行为。此类方法允许并发过程的显式表示。如：通信顺序过程（CSP），通信系统演算 （CCS），通信过程代数（ACP），时序排序规约语言（LOTOS），计时CSP(TCSP），通信系统计时可能性演算（TPCCS）等。

基于网络的方法：由于图形化表示法易于理解，而且非专业人员能够使用，因此是一种通用的系统确定表示法。该方法采用具有形式语义的图形语言，为系统开发和再工程带来特殊的好处。如 Petri图，计时Petri图，状态图等。

程序测试程序测试(program testing)是指对一个完成了全部或部分功能、模块的计算机程序在正式使用前的检测，以确保该程序能按预定的方式正确地运行。常见测试方法如下：

灰盒测试灰盒测试，确实是介于白盒测试与黑盒测试之间的，可以这 样理解，灰盒测试关注输出对于输入的正确性，同时也关注内部表现，但这种关注不象白盒那样详细、完整，只是通过一些表征性的现象、事件、标志来判断内部的运行状态，有时候输出是正确的，但内部其实已经错误了，这种情况非常多，如果每次都通过白盒测试来操作，效率会很低，因此需要采取这样的一种灰盒的方法。

白盒测试白盒测试，又称结构测试。他的前提是可以把程序看成在一个透明的白盒子里，测试者完全知道程序的结构和处理算法。这种方法按照程序内部逻辑设计测试用例，检测程序中的主要执行通路是否能按照预定要求正确工作。

白盒测试根据软件的内部逻辑设计设施用例，常用的技术是逻辑覆盖，即考察用测试数据运行被测程序是对程序逻辑的覆盖程度。主要的覆盖标准有：语句覆盖、判定覆盖、条件覆盖、判定/条件覆盖、组合条件覆盖和路径覆盖。

黑盒测试黑盒测试根据关键需求说明书所规定的功能来设计测试用例，它不考虑软件的内部结构和处理算法。常用的黑盒测试技术包括等价类划分、边值分析、错误推测和因果图等。

回归测试回归测试是软件测试的一种，旨在检验软件原有功能在修改后是否保持完整。回归测试过程：

识别出软件中被修改的部分；从原基线测试用例库“T”中，排除所有不再适用的测试用例，确定对新版本依然有效的测试用例，创建新的基线测试用例库“TN”；依据一定的策略从TN中选择测试用例测试被修改的软件；如果必要，生成新的测试用例集“T1”，用于测试TN无法充分测试的软件部分；用T1执行修改后的软件。