理论计算机科学电子笔记187（2007）125-143www.elsevier.com/locate/entcsUTP中的精化与测试用例生成伯恩哈德·K Aichernig1奥地利格拉茨科技大学软件技术学院冀丰河2号华东师范大学中国上海摘要本文提出了一个测试理论，融入霍尔和他的统一编程理论（UTP）。我们给测试用例一个指称语义，将它们视为指定谓词。这种测试用例的重新表述允许通过细化将测试用例与规范和程序相关联。有了这样一个集成测试用例的细化顺序，我们开发了一个基于故障的测试理论。基于故障的测试使用旨在证明不存在一组预先指定的故障的测试数据。一个著名的基于故障的技术是突变测试。在突变测试中，首先，通过改变（突变）源代码将错误注入程序。然后，设计了能够检测这些错误的测试用例。 假设其他故障也会被发现。在本文中，我们将变异技术应用于规范和程序。利用我们的测试理论，提出了两种新的用于检测注入（预期）故障的测试用例生成法则：一种是基于设计规格说明的语义层，另一种是基于代数性质一种编程语言。关键词：形式化方法;基于规范，基于模型，基于故障的测试;变异测试;精化;统一编程理论;编程代数。1引言编程理论探索了软件工程成功实践的基础原则因此，编程理论不应该缺少测试理论。了解软件测试的基本原理，可以使在一种语言或应用领域获得的经验迅速推广到新的应用和技术的新发展。这是贡献1 电子邮件地址：aichernig@ist.tugraz.at2 电子邮件地址：jifeng@sei.ecnu.edu.cn1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.08.048126B.K. Aichernig，J.He/Electronic Notes in Theoretical Computer Science 187（2007）125在Hoare He我们贡献的理论旨在补充现有的知识体系传统上，编程理论专注于语义问题，如正确性，精化和编程语言的代数属性。一个补充的测试理论应该关注过错的双重概念。以故障为中心的测试方法（也称为基于故障的测试）的主要思想是设计测试数据来证明不存在一组预先指定的故障。正是基于错误的测试理论的这种根本不同的哲学为编程理论增加了更深的维度。而不是通过测试进行验证，无论如何，这是一种值得怀疑的努力，在这里我们关注的是伪造。它是伪造的，因为测试人员通过设计测试用例来发现预期的错误，从而获得对系统的信心。如果证伪失败了，那么某种错误就不存在了。吸引人的一点是，程序细化在我们的测试理论中起着关键作用然而，由于集中在错误上，我们感兴趣的是那些精炼不成立的情况--同样是伪造而不是证实。关注错误会产生一些有趣的问题：设计师或程序员犯的错误会导致可观察到的失败吗？我的测试用例是否检测到此类故障？我如何找到一个测试用例来发现某个错误？可以发现这种故障的等效测试用例是什么？最后，也是最重要的一点：如何自动生成能够揭示某些故障的测试用例？所有这些问题都在本文中得到解决。这些问题以前曾得到解决，但很少在系统和科学的基础上得到解决。我们假设读者对UTP的设计理论有一定的了解本文中的所有定理都得到了形式证明。证明将出现在本文的扩展期刊版本中。本文件的结构如下。在这个一般性介绍之后，第2节对[11]的设计理论进行了非常简短的介绍，并定义了我们所说的错误设计。接下来的两个部分包括本文的主要贡献。第3节包含测试用例的构建，将发现设计中的预期错误。这种测试用例生成技术在设计的语义层上工作。在第4节中，提出了一种纯代数（面向语法）的测试用例生成技术。它是基于一个小的，但不平凡的，编程语言的代数属性。最后，在第5节中，我们讨论了结果以及相关的工作，并提出了未来的研究方向的展望2个房间计算机科学家的词汇表中有很多用来命名不需要的东西的术语：bug、error、defect、fault、failure等等。在这里，我们采用IEEE计算机协会推荐的标准术语：第2.1章有人犯了错 一个好的同义词是错误。 当人们在编码过程中犯错误时，我们称这些错误为bug。故障B.K. Aichernig，J.He/Electronic Notes in Theoretical Computer Science 187（2007）125127是错误的表现。因此，这是一个错误的结果。故障是由故障引起的错误行为。执行错误时可能发生故障在这项工作中，我们的目标是在软件设计过程中可能出现的错误的基础上生成测试用例。此类错误的示例可能是缺少或未理解的要求、错误实现的要求或简单的编码错误。为了表示这些错误，我们将在形式规范中引入故障。这些故障将通过故意改变设计而引入，从而导致可能导致故障的错误行为。在这里，我们将自己限制在基于模型（面向模型）的规范中。更准确地说，我们使用UTP的设计演算来为规范分配精确的语义。设计是一种特殊形式的谓词，带有前置和后置条件部分，以及字母表。字母表是一组变量，声明了对象空间。设计谓词的自由变量是字母表的一个子集，表示程序执行前（未修饰变量名）和执行后（修饰变量名）此外，特殊的布尔变量OK和OKJ表示节目的成功开始和终止。形式上，我们定义定义2.2设计设P和Q是不包含ok或okJ的谓词。PQ=df（okP）（okjQ）设计是一种关系，它的谓词是（或可以是）以这种形式表达的。每一个程序都可以被表达为一个设计。这使得设计理论成为一种表达规范、程序和测试用例的工具。下面介绍一些基本的编程结构。定义2.3赋值给定一个程序变量x和表达式eX ：=e=df（wf（e）xJ=eyJ=y···zJ=z）其中wf是定义表达式e的良构性的谓词（e可以被评估）。定义2.4条件PbDQ=df（wf（b）<$（b<$P <$$>b<$Q））其中wf是定义布尔表达式b的良构性的谓词。在进一步的讨论中，我们将保持简化的假设，即所有的程序表达式都是格式良好的（定义的），因此wf=true。序贯复合的定义是显而易见的，通过变量v的中间状态v0的存在。在这里，存在量化隐藏了中间观察v0。此外，P的输出字母表（outαP）和Q的输入字母表（所有变量都用虚线表示，inαJQ）必须相同。128B.K. Aichernig，J.He/Electronic Notes in Theoretical Computer Science 187（2007）125定义2.5顺序组合P（vJ）;Q（v）=df<$v0·P（v0）<$Q（v0），条件是αP=inαJQ={vJ}非决定性的、恶魔般的选择被定义为逻辑或：定义2.6（恶魔的选择）PHQ=dfPQUTP提供了一系列的定理和引理来表达这种编程结构的基本代数性质（见[11]）。蕴涵在设计上建立了一个精化顺序（实际上是一个格）因此，更具体的实现意味着更抽象的规范。定义2.7（细化）D1±D2=df<$v，w，··· ∈A·D2<$D1，对所有具有字母A的D1，D2.或者，使用方括号来表示字母表中所有变量的泛量化，我们写[D2<$D1]，或者简单地用精化演算风格D1±D2。显然，这给出了众所周知的性质，即前提条件在细化下被削弱，而后置条件被加强（变得更具确定性）：定理2.8（设计的改进）[（P1-Q1） ⇒ （P2）]i[P2⇒P1]和[（P2-Q1） 问2]根据定义2.1，故障代表错误。这些错误可以在整个开发过程中引入到所有创建的工件中。因此，故障出现在细化层次结构中从需求到实现的不同抽象级别上。显然，早期引入的错误是最危险的（也是最昂贵的），因为它们可能在实现中未被检测到;或者正式地，错误的设计可能被正确地细化到实现中。精化是讨论某些故障的作用和后果以及最适合表示故障的设计谓词的中心概念。定义2.9（设计错误）给定一个（预期的）设计D，和一个（非预期的）设计Dm，在创建过程中发生了错误（m代表突变）。然后，我们将设计Dm中的设计错误定义为与D的语法差异，如果D /±Dm(or（D±Dm））。我们称Dm为D的错误设计或错误突变。B.K. Aichernig，J.He/Electronic Notes in Theoretical Computer Science 187（2007）125129因此，并不是所有的错误都会导致故障。在这里，作为一个故障，这个故障的可能（外部）观察必须存在。例如，错误地将冗余条件添加到设计中并不会导致错误的设计（因为精化成立）。然而，改变字母表会导致错误的设计。（在类型检查期间检测到）。还请注意，在定义中使用了术语“预期”（非预期），而不是“正确”（不正确）。这是必要的，因为后者只是相对于一个给定的规范来定义的，但是错误从一开始就可能已经存在于这样的规范中。3设计缺陷在本节中，我们通过细化将测试用例与设计和程序联系起来。 这是可能的，因为我们通过将测试用例视为指定谓词来赋予它们指称语义。其结果是一种基于非细化的测试用例生成技术。3.1作为设计我们认为测试用例是对给定输入定义期望输出的规范。因此，我们将测试用例定义为设计的子理论。定义3.1（测试用例，确定性）设i为输入向量，o为期望输出向量，两者都是值列表，分别与变量列表v和vJ具有相同的长度此外，值列表上的相等性应该被定义。td（i，o）=dfv=i<$vJ=o虽然对于确定性程序来说是足够的，但是从规范中导出的测试用例必须考虑非确定性。因此，我们将测试用例的概念概括如下：定义3.2（测试用例，通用）tH（i，c）=df v=i<$c（vJ）其中c是后状态空间上的条件，定义了可能无限的预期结果向量集。第一作者[1]以前的工作表明，精化是理解测试用例、规范和实现之间关系Refinement是一种观察顺序关系，通常用于从规范到实现的逐步开发，以及支持软件组件的替换。由于我们将测试用例视为（一种特殊形式的）规范，因此很明显，正确的实现应该细化其测试用例。因此，测试用例是实现的抽象，当且仅当实现通过测试用例。这个观点可以提升到规范的层面。当测试用例130B.K. Aichernig，J.He/Electronic Notes in Theoretical Computer Science 187（2007）125如果测试用例是从规范中正确导出的，那么这些测试用例应该是规范的抽象。形式上，我们定义：定义3.3设T是一组测试用例，S是一个规范，I是一个实现，所有这些都是设计，不 ± S±I，对于所有t∈T我们定义• T作为关于S的正确测试集，• 实现I通过了T中的测试用例，• 实现I符合规范S。在基于故障的测试中，寻找一个例如，在经典的突变测试中，D是一个程序，Dm是D的突变体。然后，如果Dm中的突变表示故障，则应包括测试用例t以检测故障。因此，我们可以定义一个基于故障的测试用例如下：定义3.4（故障检测测试用例）设t为输入输出测试用例（可能是非确定性的）。此外，D是一个设计，D是它的错误版本。那么，t是一个故障检测测试用例，t±Dm（t/±Dm）我们说t检测Dm中的故障。或者，我们可以说测试用例区分D和Dm。用突变测试的语言来说，t杀死了突变体Dm。所有检测到某个故障的测试用例形成一个故障检测等价类。请注意，我们的定义仅依赖于设计的晶格性质。因此，只要使用适当的细化定义，我们的基于故障的测试策略可以扩展到其他基于格的测试模型。3.2故障检测等价类测试用例生成中的一个常见技术是等价类测试-将输入域（或输出范围）划分为等价类。动机是减少测试用例，通过识别等价行为的输入集。这种策略背后的基本原理是一个统一性假设，假设一个等价关系的行为的程序。关于形式规格的一个著名的等价类测试技术是DNF划分：将形式规格重写为其析取范式（参见[9]）。通常，DNF分区应用于关系规范，导致关系的不相交分区（注意，在DNF分区中不保证输入域的不相交性）。 我们称这种关系划分为测试等价类。B.K. Aichernig，J.He/Electronic Notes in Theoretical Computer Science 187（2007）125131定义3.5（检验等价类）给定一个设计D=（p<$Q），我们定义一个用于检验D的检验等价类T<$作为形式T<$=d<$;D的设计，使得[d<$p]。该定义使用断言运算符b=df（v=vJ）bD，导致如果条件成立（跳过），则对变量v没有效果的设计，否则表现为中止（中止=真）。注意，这里测试等价类是表示输入输出关系的设计。它通过谓词d定义，谓词d本身表示输入值上的等价类。鉴于上述定义，设计显然是其测试等价类的细化：定理3.6给定一个设计D = p<$Q和它的一个等价类。 然后，T±DQ显然，DNF划分可以应用于设计谓词。然而，在下文中，我们关注故障检测测试等价类。这些是测试等价类，其中所有测试用例都能够检测到某种错误。定义3.7（代表性测试用例）测试用例t=tH（i，c）是测试等价类T=d;D的代表性测试用例，其中D=pQ，当且仅当d（i） ∧ p（i） ∧ [Q（i）c]Q这个定义确保了代表性测试用例的输出条件不弱于其测试等价类规范。下面的定理提供了一个测试等价类的显式构造，它表示一组能够检测设计中特定故障的测试用例。定理3.8（故障检测等价类）给定一个设计D = p<$Q，其故障设计Dm= pm<$Q m，则D/±Dm。为了简单起见，我们假设Q<$（p<$Q）。然后，将测试等价类T=dfd; D，其中d =<$p m vJ·（Q mQ）能够检测到Dm中的故障。Q这种构造背后的合理性是这样一个事实：对于一个能够区分设计D和它的错误兄弟DM的测试用例，两者之间的细化必须不成立。对于设计，人们可以观察到两个可能违反细化的地方（情况），即前置条件和后置条件。T的域表示这两类测试输入。第一类是测试输入，用于正确的设计，但导致错误的设计中止。第二类是产生不同输出值的公共输入状态。这两个条件是从否定前置条件和后置条件的精化律（定理2.8）中推导出来的。132B.K. Aichernig，J.He/Electronic Notes in Theoretical Computer Science 187（2007）125我们已经开发了一个约束求解器，用于根据定理3.8[3]从突变的OCL规范4程序故障到目前为止，我们关于测试的讨论主要集中在设计的语义模型上。 在本节中，我们将从语义转向语法。动机是将我们自己限制在一个设计的子类中，这些设计是可以用某种编程语言表达的，或者至少是可以用某种编程语言实现的。因此，我们将程序定义为用编程语言的有限符号（语法）表示的谓词。从编程语言运算符的谓词语义中，可以推导出代数定律（参见[11]）。在下文中，我们将使用这种程序代数作为一种手段，在纯粹的语法基础上对程序中的错误进行推理。 其结果是一个测试用例生成算法的基于故障的测试，工程上的编程语言的语法。我们定义语法如下：程序名：：=true| 变量列表|编程语言布尔表达式 D语言程序|程序设计|编程语言 H程序|递归标识符| μ递归标识符程序运算符的语义遵循第2节中的定义。最后一个递归语句具有标准的最小定点解释。4.1有限范式代数法则，表达了语言中操作符的熟悉属性，可以用来将限制符号中的每个表达式简化为一个更受限制的符号，称为范式。范式在程序代数中扮演着重要的角色：它们可以用来比较两个程序，也可以给编程语言一个代数语义。我们的想法是使用一个标准形式来决定两个程序，原始程序和错误的程序（也称为突变体）是否可以通过测试用例来区分。当两者的正规形式相等时，则错误不会导致一个（可观察到的）错误。这解决了突变测试中的等效突变体问题。此外，规范形式将用于推导故障检测等价类的纯代数（语法）的基础上。我们的范式就是为此目的而设计的：与[11]中的范式相反，我们推B.K. Aichernig，J.He/Electronic Notes in Theoretical Computer Science 187（2007）125133条件向外。所有的定律都得到了正式的证明。下面的赋值法线取自[11]。定义4.1（赋值范式）赋值的范式是总赋值，其中程序的所有变量都以某种标准顺序出现在左边。x，y，.，z：=e，f，. ，g赋值v：=g或v：=h（v）将用于表示总赋值;因此向量变量v是所有变量的列表，g，h表示表达式的列表。一个非全赋值可以通过以下方式转换为全赋值：（1 ）将恒等赋值（a，. ：= a，. ），（2）变量与其关联表达式的重新排序。消除范式之间的顺序组合的定律是（v：=g;v：=h（v））=（v：=h（g））（L1）其中h（g）通过将g中的表达式替换为v中的相应变量来计算。由于我们的语言包括非确定性，我们将条件转换为受保护命令的非确定性选择。（PcDQ）=（c<$P）H（<$c<$Q）（L2）这一定律源于有条件和非确定性选择的定义。有了这个消元规则，我们就能够定义一个非确定性的标准形式。定义4.2（非确定性范式）非确定性范式被定义为保护总数分配的非确定性选择。（g1） ：= f1）H（g2） ：= f2）H. H （g nv ：=fn）.设A是一组有保护的全赋值，那么我们将范式写为 A.以前的赋值范式可以很容易地用这个新范式表示为单位集v：=g = .{（true）}最容易消除的操作符是选择本身..（A）H（ B）= .（AB）}（L3）和条件...（一）dD（B）=（{（（d b）P）|（b <$P）∈ A}）H（L4）.（ {（（<$d c）Q）|（c <$Q）∈B}）134B.K. Aichernig，J.He/Electronic Notes in Theoretical Computer Science 187（2007）125顺序组合减少了..（A）;（ B）= .{（（b <$（P; c））<$（P; Q））|（b <$P）∈ A <$（c<$Q）∈ B}（L5）为了降低L5定律中的P;c，我们需要一个附加定律（v：=e）;b（v）=b（e）（L6）程序常数true不是赋值，一般不能表示为保护赋值的有限析取。将其引入语言需要一个新的范式。定义4.3（非终止范式）非终止范式是一个表示为析取的孟加拉国其中b是非终止的条件，P是非确定性范式。任何终止的前一范式P都可以表示为伪差而常数true为真核 v：=v新范式之间的其他算子可以通过以下定律（b）H（c）=（b）（c）（P）（H）（Q）（L7）（b）dD（c）=（（bd））（PdDQ）（L8）（b）P;（c）Q=（b）（P;c）（P;Q）（L9）右手边的每个算子的出现次数可以通过前面部分的定律进一步减少。同样，为了简化（P;c），需要一个额外的定律;这次是为了之前的非确定性范式。.（A）;c ={（g（P; c））|（g<$P）∈ A}（L10）上面的代数定律允许我们语言中的任何非递归程序被简化为有限范式.b{（g iv：= e i）|1 ≤i≤ n}我4.2正规形B.K. Aichernig，J.He/Electronic Notes in Theoretical Computer Science 187（2007）125135在前一节中，我们已经证明了精化（或非精化）是我们测试理论的核心。对于一般设计，136B.K. Aichernig，J.He/Electronic Notes in Theoretical Computer Science 187（2007）125规范形式程序中的错误是由它们的精化法则启发的接下来，我们为我们的程序范式提出这些精化律。对于确定性的赋值，精化问题变成了一个简单的等式问题。两个赋值范式相等，当且仅当总赋值中的所有表达式都相等。（v：=g）=（v：=h）i =[g=h]（L11）允许检测非确定性正常形式的精制突变体的定律是：.R±（A）iP：P∈A·（R±P）（L12）（（g1P1）H. H（g n<$P n））± （bQ）i [i·（（giPi）（bQ））]（L13）[（g<$v：= f）<$（b<$v：= h）]i <$[b ⇒ （g（f=h））]（L14）第一定律使得非确定性范式可以被分解成它的分量保护赋值，然后由第二定律单独决定。接下来，它是如何展示这种范式促进基于故障的测试用例的生成。4.3基于范式的测试用例生成所提出的规范形式已被开发，以促进自动生成的测试用例，能够检测预期的故障。代数精化律解决了等价突变体（更准确地说，精化突变体）的问题上述定律也是我们下一个测试用例生成定理的灵感来源：它计算检测给定故障的测试等价类定理4.4设P是一个程序，Pm是这个程序的一个错误变异，其范式如下P=cPm=d.{（a j = f j）|1≤j≤ m}J.{（b kv：= h k）|1 ≤k≤ n}K然后，将测试等价类的每个代表性测试用例T=dfd;P，其中d=（<$c<$d）（<$cbkK（aj（fjJh（k）能够检测到Dm中的故障。Q我们给出了一个非正式的论证，而不是给出正式的证明：为了检测错误，测试等价类的域必须包含这些输入值，其中精化不成立。我们有两种不细化的(1)Pm不终止而P终止：（2）两者都终止但结果不同.B.K. Aichernig，J.He/Electronic Notes in Theoretical Computer Science 187（2007）125137≥(i) 这些测试用例必须添加到突变体不终止，但原始程序终止的地方。这就是（<$cd）成立的时候。(ii) 在终止的情况下，根据L12和L13两个定律，所有被保护的命令的组合都必须被测试，以确定突变的命令对原始命令的改进。那些细化测试失败的地方，对测试等价类有贡献。L14法则告诉我们，在两个受保护的命令之间保持i <$[b k<$（a j<$（f j=h k））]。否定这一点，给出了v，vJ·b k<$（<$a j<$（f j/= h k））。由于我们只对定义了输出的测试用例感兴趣，因此我们添加了约束<$c。 我们看到这个条件是我们测试域的核心因为我们必须证明非-因此，对于P（j）的所有非确定性选择，这必须成立。最后，Pm的每个非确定性选择都可能导致非细化（k）.例4.5考虑下面的例子，程序Min用于计算两个数x，y的最小值。M in =dfz：=xx≤yDz：=y在突变测试中，假设程序员会犯小错误。一个常见的错误是混合运算符。m中的突变体M模拟了这样的错误。m中的M=dfz：=xx yDz：=y它们的标准形式可以很容易地推导出来：米={添加身份分配}x，y，z：=x，y，xx≤yDx，y，z：=x，y，y={L2}（（x≤y）<$x，y，z：=x，y，x）H <$（x≤y）<$x，y，z：=x，y，y）M中的M={添加身份分配}x，y，z：=x，y，xx≥yDx，y，z：=x，y，y={L2}（（x≥y）<$x，y，z：=x，y，x）H（<$（x≥y）<$x，y，z：=x，y，y）根据定理4.4，我们有138B.K. Aichernig，J.He/Electronic Notes in Theoretical Computer Science 187（2007）125D=（<$false<$false）<$k∈{1，2}（<$false <$bk<$j∈{1，2}（<$aj<$（fj/=h k）=（x≥y<$（x > y<$false）<$（x≤y<$x∨（y））（xy（x >yx/=y）（x≤yfalse））=x > yxy注意，x=y的情况已经被正确地从故障检测等价类中排除，因为这样的测试用例不能区分程序的两个4.4递归理论和直觉都告诉我们，递归程序不能表示为有限范式。递归的非决定性程度不能用有限析取来表示，因为它依赖于初始状态。克林氏定理告诉我们，递归程序的范式是最小上.程序逼近无穷级数的界S0，S1，. 其中每个AP-近似是其前身的精化，因此Si±Si+1。定理4.6（Kleene）如果F是连续的，则 .μX·F（X）=Fn（true）n其中F0（X）=dftrue，Fn+1（X）=dfF（Fn（X））Q通过下降链的最小上界分布的算子称为连续算子。幸运的是，我们语言中的所有运算符都是连续的，因此可以应用这种范式转换。不幸的是，这种无限范式永远无法完整地计算;然而，对于每个n，有限范式可以很容易地计算。因此，我们的完整编程语言的范式定义如下定义4.7（无限范式）递归程序的无限范式是一个理论上表示为有限范式下降链的最小上界的程序。形式上，是形式.S，其中S =<$（c n<$Q n）|n∈ NS是近似值的下降链，Q是非确定性范式，即受保护命令的析取。B.K. Aichernig，J.He/Electronic Notes in Theoretical Computer Science 187（2007）125139对于测试用例生成，同样，必须检查原始和突变之间的细化。幸运的是，[11]中的以下定律告诉我们，我们可以分解问题。...（S）±（T）ii：i∈N·Si±（T）（L15）在我们的测试用例生成方法中，处理递归程序的中心思想是近似程序和突变体的正常形式，直到可以检测到非细化。对于等价突变体，上限n将决定何时停止搜索。一个例子可以说明这一点。例4.8假设我们想找到一个指向数组A [1.]中最小元素的索引t。n]，其中n是数组的长度，n > 0。用于找到这样的最小值的程序可以用我们的编程语言表示如下：MIN= df k：= 2;t：= 1;μX·（（B;X）k≤nDk，t：=k，t）B=df（t：=k;k：=k+ 1）A[k] n）k，t：=k，t）接下来，计算近似链中的第一个元素。根据KleeneS1=dfF（true）=（k≤n）<$（（k > n）<$k，t：=k，t）第一个近似值仅在没有输入迭代时描述精确的行为。第二个近似描述的行为已经更恰当，考虑到一个迭代。注意非终止条件140B.K. Aichernig，J.He/Electronic Notes in Theoretical Computer Science 187（2007）125<会变得更强S2=dfF（S1）=（k+1≤n<$A [k] n<$A [k] n<$A [k]≥A[t]）<$（k，t：=k+ 1，t））H（false）（（k > n）k，t：=k，t）=（k n）(((k=n<$A[k] n）k，t：=k，t））从前三个近似可以看出，我们的范式近似将计算路径表示为受保护的命令。随着近似的进行，越来越多的路径被包括在内。显然，整个程序的范式近似，包括k和t的初始化，可以很容易地通过在S1，S2，.中将k替换为2，将t替换为1来获得。.接下来，我们将说明我们的基于故障的测试技术，该技术首先引入一个突变，然后尝试近似突变，直到细化不成立。一个常见的错误是把循环终止条件搞错了。我们可以通过以下突变体来建模：MINm=dfk：= 2;t：= 1;μX·（（B;X）k nDk，t：=k，t）它的第一个近似值给出了Sm1=dfF（true）=（k n）<$（（k≥n）<$k，t：=k，t）通过应用定理4.4来寻找可以区分两个第一近似的测试用例，我们认识到这样的测试用例不存在，因为S1±Sm1。测试等价类域谓词d1（k，t）的计算结果为假：d1（k，t）=（定理4.4）（<$（k≤n）<$k n）<$（<$（k≤n）<$k≥n<$（<$（k > n）<$false））=B.K. Aichernig，J.He/Electronic Notes in Theoretical Computer Science 187（2007）125141false错误=false142B.K. Aichernig，J.He/Electronic Notes in Theoretical Computer Science 187（2007）125∼⊥有必要考虑突变体的第二近似：Sm2=dfF（Sm1）=（k+1 n）=伪n（k≥n<$k≤n）=（k=n）通过替换初始值（k= 2和t= 1），具体的故障检测测试等价类为：T2=（n= 2）;MIN结果令人惊讶。计算测试等价类表示每个包含两个元素的数组都可以作为测试用例来检测错误。人们可能已经预料到，过早离开循环的错误只能被揭示出来，如果最小值是最后一个元素（A[2]
下载后可阅读完整内容，剩余1页未读，立即下载
