理论计算机科学电子笔记164（2006）115-128www.elsevier.com/locate/entcs当基于模型的测试失败时伯恩哈德·K Aicherniga，b，1 和克里斯乔治a，2a联合国大学国际软件技术研究所澳门特区中国奥地利格拉茨科技大学软件技术学院摘要Armando Haeberer在将科学哲学的成果转化为软件测试方面做出了巨大贡献。他指出，确认理论的标准方法的局限性，其中观察结果来自理论和假设，也存在于软件测试中。他批评了从代数规范中生成测试用例的经典方法，但也提供了一种基于Gaviour的bootstrap方法的替代方法。然而，人们在他的贡献之后所期望的争论从未真正发生过。这是特别令人惊讶的，因为大多数基于模型的测试方法遵循他批评的方法。本文旨在通过从一个新的角度看待他的发现来展开辩论。我们使用细化的概念来澄清测试中涉及的基本问题，并讨论实际后果。关键词：形式化方法，基于规范的测试，测试用例生成，科学哲学，理论确认，假设演绎确认，自举确认，代数规范，精化。1引言基于正式规范（模型）的测试成为一个活跃的研究领域，特别是在Gaudel指出“测试也可以是正式的”之后 这种日益增长的兴趣的原因是规范允许黑盒测试的自动化它们可以被结构化地分析以生成测试用例，并且它们提供了一些元素来预测测试的结果。因此，今天，大多数规范语言都带有测试用例生成方法，例如VDM [14]，Z，B [24]，CSP [26]，Lotos [18]或RAISE [13]。然而，这个领域没有考虑到它植根于认识论的更深层次的基础1电子邮件地址：bka@iist.unu.edu2电子邮件地址：cwg@iist.unu.edu3 本文同时使用了形式规范和模型这两个术语。1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.09.009116B.K. 艾希尼格角George/Electronic Notes in Theoretical Computer Science 164（2006）115Armando Haeberer [25]认识到科学哲学的结果与软件测试有关。特别是，关于科学假设如何被有限观测证实（或反驳）的争论，转化为从正式模型生成测试用例的问题。卡尔纳普发展了一个逻辑框架，即陈述观点，来讨论所涉及的问题。这些问题之一是，陈述假设的理论语言涉及有限的量化，但观察的世界是有限的。如何用有限的观察、有限的理论来证实他与波普尔的辩论是众所周知的，Dijkstra 然而，Haeberer等人向计算机科学界报告了另一个重要结果[9，10，21]。ClarkeGaviour在[19，20]中指出，从假设和背景理论中推导出预期观察结果的经典方法存在根本性问题，所有拯救这种假设演绎方法的尝试都失败了。这是特别令人担忧的，因为今天大多数基于模型的测试方法本质上都是假设演绎的-包括代数测试方法，因为它最初是由Gannon，Mc Mullin和Hamlet [ 16 ]和Bo u g 'e et a l提出的。[6，7，8]以及由Bernot、Gaudel和Marre [5，17]开发和实施的新产品。因此，Haeberer批评了这种代数测试用例生成方法，并提出了几个反例，这种测试方法失败。在这些示例中，生成的测试用例报告了假阴性：一些软件模块被拒绝，尽管在观察上与通过测试的其他模块等同。Hae- berer建议应用Gavinour的bootstrap测试方法来克服这些问题。然而，就我们目前所知，人们期望随后进行的辩论从未真正发生过。本文旨在通过从一个新的角度看待他的发现来展开辩论。我们使用细化的概念来阐明测试中涉及的基本问题，并讨论实际后果。本文其余部分的结构如下。在这一介绍之后，第2节介绍了确认理论的假设演绎方法以及Gadminour接下来，在第3节中，我们将哲学讨论映射到编程（和测试）理论。然后，在第4节中，我们讨论了具体的反对Haeberer的经典代数测试方法。在第5节中，我们问，如果Gavanour的Bootstrap方法可以作为一种替代？最后，第六节得出结论。第二章假设演绎法假设演绎法（hypothetico-deductive method，HD）的本质是，如果证据可以从一个理论中推导出来，那么它就被视为证实了该理论证据是预测出来的，如果预测是正确的，证据就证实了理论。因此，例如，一个具体化公理是一个理论的一部分，而这个理论也应该是一个实现的理论。公理的一个实例，如果在该实现的测试中为真，则确认B.K. 艾希尼格角George/Electronic Notes in Theoretical Computer Science 164（2006）115117理论认为，实施是正确的。这里的更正式地说，假设演绎图式（以简单形式）是一个三元组其中ST是背景理论，H是我们希望证实的假设，E是证据，(i) ST和H相互一致(ii) ST，HE(iii) STbE第一个条件是显而易见的。 第二个是高清的心脏，并说，假设的背景包含并因此预测了证据。第三，防止可以从背景中推断出的证据被用来证实无关的东西。[ 10 ]第10(i) E永远不能证实ST的任何后果。(ii) 如果H被E关于ST所证实，那么Hφ也是如此，其中φ是与HST相一致的任何句子。(iii) 如果E为真且不是重言式，且φ是任何一致的句子，使得Ebφ则φ被E关于一个真理论所证实（即（φ<$E））。Haeberer等人认为第一个困难是可以容忍的，但认为其他两个的结合导致了一种站不住脚的方法。不幸的是，他们的例子没有提到这些困难，也没有进一步的论点。实际上，代数测试方法的反例还有其他（技术）原因，我们将在第4节中看到。但首先，我们通过将这两个哲学障碍转化为一个众所周知的编程理论来仔细研究它们。3当测试用例太弱时为了在软件测试环境中讨论HD及其困难，我们将其转换为统一编程理论（UTP）的设计理论[22]。事实上，我们将把程序的意义以及它的测试用例定义为一阶逻辑中的谓词。这将表明HD的问题与细化（和抽象）有关。UTP中的设计是具有前置和后置条件的特定形式的谓词设计（谓词）的自由变量，称为字母表，表示程序执行之前（未修饰变量名）和之后（修饰变量名）的状态变量。此外，特殊的布尔变量ok和okJ表示程序的成功启动和终止。形式上，我们定义定义3.1 [设计]设（前置条件）P和（后置条件）Q是不包含ok或okJ的谓词。JP<$Q=df（ok<$P）<$（ok（1999年）118B.K. 艾希尼格角George/Electronic Notes in Theoretical Computer Science 164（2006）115设计是一个谓词，它与执行之前和之后的观察有关，可以用这种形式表达。蕴涵在设计上建立了一个精化顺序（实际上是一个格）因此，更具体的实现意味着更抽象的规范。显然，这给出了众所周知的性质，即前提条件在细化下被削弱，而后置条件被加强（变得更具确定性）：定理3.2（设计的改进）[（P1-Q1） （P2）] i [P2⇒P1] 和[（P2-Q1） 问2]对于设计中常见运算符的定义，如顺序组合，条件，选择等，我们来看看[22]。我们认为测试用例是为给定输入定义预期输出的规范因此，我们将测试用例定义为设计的子理论。定义3.3 [测试用例，确定性]设i为输入向量，o为期望输出向量，两者都是值列表，分别与变量列表v和vJ具有相同的长度。在这样的向量上的相等是以明显的方式逐点定义的。JT（i，o）=df v=i<$v=o虽然对于确定性程序来说是足够的，但是从规范中导出的测试用例必须考虑非确定性。定义3.4 [测试用例，非确定性]有时测试用例必须考虑非确定性，因此我们定义非确定性测试用例如下：T（i，c）=JHdfv=ic（v）其中c是状态空间上的一个条件，定义了一组可能的预期结果。第一作者[1，2，3]以前的工作表明，精化是理解测试用例、规范和实现之间关系的关键。Refinement是一种观察顺序关系，通常用于从规范到实现的逐步开发，以及支持软件组件的替换。由于我们将测试用例视为（特殊形式的）规范，因此很明显，正确的实现应该细化其测试用例。因此，测试用例是实现的抽象，当且仅当实现通过测试用例。这个观点可以提升到规范的层面。当测试用例是从一个规范中正确地导出时，那么这些测试用例应该是该规范的抽象。形式上，我们定义：定义3.5设T是一个测试套件（测试用例的结合），S是一个规范，I是一个实现，都是设计，[一 ⇒ S] 和 [S [美国]B.K. 艾希尼格角George/Electronic Notes in Theoretical Computer Science 164（2006）115119H我们定义• T作为关于S的正确测试套件，• T中的所有测试用例都是关于S的正确测试用例，• 实现I通过测试套件T，• 实现I符合规范S。读者会注意到，这恰好代表了一阶逻辑中的假设演绎方法。测试用例T是预测的观测值，并且在这里通过暗示从规范S推导出来。该规范代表待确认的假设。在这种情况下，HD的第二个困难，即每一个更强的假设都可以被证实，在实践中并不是一个困难。它仅仅意味着S的所有精化也被确证了。这与我们的测试理论是一致的，即所有的细化都应该通过从规范中导出的测试。第三个困难更严重。HD的测试用例推导方法允许测试用例在后置条件中太弱。这导致测试用例无法检测到所有错误。例3.6考虑一个规格S=df（xs，xs，J）n（xs，xs，J）用于对输入列表xs进行排序的排序算法。然后，我们可以导出一个测试用例ST（[3，4，2]，[2，3，4]）然而，下面更抽象的非确定性测试用例也是一个有效的抽象S T（[3，4，2]， sorted（xsJ））这个测试用例太弱了，因为它可能会确认一个错误的实现，排序但丢失了输入列表的元素。这表明，演绎，这里的含义，可能会导致不充分的测试用例太弱。在前置后置条件的上下文中，必须小心不要错误地削弱后置条件。然而，请注意，弱化后置条件可能是获得更高效测试神谕的一种策略。例如，在对排序算法进行了几次测试之后，测试人员可能会决定专注于检查顺序，假设排列条件已经得到充分确认。显然，应该非常谨慎地采取这种战略。接下来，我们将重点放在测试抽象数据类型实现的通用代数测试方法上。我们将再次看到，正是实现关系（即公理化的细化）导致了基本问题。120B.K. 艾希尼格角George/Electronic Notes in Theoretical Computer Science 164（2006）115我4针对代数规范的在代数测试方法中，测试用例是从代数规范生成的 这种方法最初是由Gannon，McMullin和Hamlet [16]和Boug'eeeta l提出的。[6 ，7 ，8]，以及由Bernot，Gaudel和Marre [5，17]提出的进一步发展和完善。它已成功地应用于测试过程[4]，功能[12]和面向对象[15，11]程序。最近，我们将其应用于测试用RAISE规范语言编写的可执行模型[13]。在这种方法中使用的（代数）规范由签名和正条件方程作为公理组成，其中签名声明排序和排序函数符号。在这种情况下，一个被测试的程序P在规范SP=（Ax，Ax）下必须提供一些过程或函数来执行规范中的操作给定一个基项t，我们让tP表示用P计算t。 这里，测试是任何基础方程（t1=tJ···JJ1tk）→t=t。一个程序P对这样一个基本公式的测试实验包括：（1）计算ti和tJ，并比较1≤i≤k的结果;（2）如果这些测试中的每一个都是阳性的，则评估t和tJ并比较它们的结果;否则可以放弃该测试实验给定一个条件方程排序规范SP和一个测试程序P，P被测试SP，测试上下文是一对（H，T），其中H是P上的一个假设，T是一组测试。一般来说，假设程序只能对可观察的排序执行上述比较。通常，可观察排序是P语言编写时预先定义的排序对于不可观察排序的术语，该方法建议将它们包装在可观察的上下文中。两个不可观测项被认为是相等的，如果否，可观察的上下文可以区分它们。理想的测试环境是（Hmin，ExhaustSP）。Hmin指出，对于每一个可观察的排序，P提供了一个正确的等式实现，并且P的行为通过可观察的上下文在观察上等价于一个有限生成的n-代数。ExhaustSP表示穷举测试集，是SP公理的所有基础实例的集合。如果这些公理涉及到不可观察的种类，那么它们的结果还必须包含在每一个可能的观察语境为了减少一组测试到一个实用的大小，选择假设。根据对计划的某些了解、规范的某些覆盖标准以及最终的成本考虑，可以制定和组合各种选择假设除了他的哲学反对意见，因为这种方法是HD，Haeberer还有其他几个反对意见。应该指出的是，这些问题是众所周知的，并在文献中有记载（例如，见关于甲骨文问题的讨论在这一节中，我们简要地讨论了他的反对意见，从我们的实际观点，以便在下一节看到，如果他的替代Bootstrap方法会做得更好。B.K. 艾希尼格角George/Electronic Notes in Theoretical Computer Science 164（2006）1151214.1扩大执行首先，公理可能涉及抽象或隐藏排序之间的等式，并且这样的等式可能没有实现：数据库的设计者不太可能包含一个函数来测试两个数据库是否相等。这是一个众所周知的问题，通常被称为Oracle问题。甘农等人在其结论[16]中已经指出了这个问题“系统中的主要原则是，在具体实施中。必须为每个新类型提供相等函数，因为泛型相等很少实现用户想要的内容。如果规范使用隐藏函数（即，仅在规范中使用的函数），每个函数都必须出现在要执行的测试的实现中。使用“抽象生成器”风格的规范可以在很大程度上避免这个问题，但除此之外，一般的答案是抽象等式可以根据这些类型的观察者来定义。必须加上平等的定义，但定义的问题不应太大。测试用例的运行时间可能很长，但是任何测试具有大型数据对象的软件的方法都必须处理这个问题。其次，可能存在未实现的隐藏功能。例如，排序程序的任何规范都可能涉及像“permuts”这样的关系但在这种情况下，oracle似乎只有两种选择：要么使用同一问题的现有可信实现，要么必须使用指定。如果规范涉及未实现的隐藏函数，那么除了实现它们之外别无选择。4.2实施的扩展将影响其开发或实施这是从前面的反对意见得出的。首先，我们注意到，可测试性设计在其他工程分支以及软件工程中是标准的：它决不是本质上不好的实践。第二，在软件中可能比在其他工程学科中更容易，通常可以使用继承等机制添加额外的功能，而不会影响正在扩展的代码4.3隐藏函数的错误实现可能会生成假阴性这是[9]中一个例子的本质（见下面的例子4.1这是一个例子，说明如何在不改变结果的情况下改变涉及隐变量的公理，但实际上问题更普遍。任何错误定义的扩展都可能导致测试失败，而显然，这并不意味着程序被扩展。如果程序实际上是正确的，则结果是假阴性。打个比方：电路的理论可能会给出某个点的电压预测，但实现的硬件可能不会包括任何内容，122B.K. 艾希尼格角George/Electronic Notes in Theoretical Computer Science 164（2006）115用于检查电压的测试探头可能放置在错误的位置，或者电压表可能有故障。这样的问题通常不会被认为是无效的技术，失败也不会总是意味着实施中的错误。在突变测试领域还有另一个类似的例子，测试中的程序被稍微改变（通常是以模仿常见错误的方式程序员）。如果现有的测试用例集对变异的程序给出了与原始程序相同的结果，则表明该测试用例集可能不充分。例如，可能变异的代码没有被执行。但也可能有其他的解释：变异的代码可能实际上等同于原始代码，或者变异可能是在无法访问的代码中。因此，人们不会立即假设结论（这里是一组测试用例的不足）。 一个更好的分析是，代数测试方法检测突变，公理，但问题在于规格：改变公理对输入输出规格没有任何区别，规格的质量有问题。我们可以更进一步，认为代数测试方法的一个优点是能够发现规范的问题顺便说一句，这个例子可以简化为没有任何隐变量的例子，只涉及一个公理o（x1，x2，x3，x4）=x2<$x3<$x4其中输入是xi，i= 1， 2， 3， 4。 有趣的是， o并不依赖于x1，而且这个指定似乎很可能是错误的。如果有一种技术能发现这一点就好了！例4.1设S=（λ，Ax）是包含一个隐排序HBool和一个可观测排序Bool的回路的以下代数规范。Op={ 0B， 1B：布尔，0H， 1H：HBool，·BBH：布尔×布尔→HBool，•HHH：HBool×HBool→HBool，+HBH：HBool×Bool→HBool，+HBB：HBool×Bool→Bool，a、b、c、d、e：布尔×布尔×布尔×布尔→HBool，o：布尔×布尔×布尔×布尔→布尔}B.K. 艾希尼格角George/Electronic Notes in Theoretical Computer Science 164（2006）115123程序P1var w1，w2，w3，w4：Boolfunction+BBH（x，y：Bool）：HBoolfunction+HBH（x：HBool;y：Bool）：HBoolfunction+HBB（x：HBool; y：Bool）：Bool函数·HHH（x：HBool; y：HBool）：HBool函数·BBH（x，y：Bool）：HBool函数a（x，y，z，t：Bool）：HBoolreturn x+BBH yfunction b（x，y，z，t：Bool）：HBoolreturny·BBH z函数c（x，y，z，t：Bool）：HBool返回a（x，y，z，t）·HHHb（x，y，z，t）函数d（x，y，z，t：Bool）：HBool返回b（x，y，z，t）+HBHtfunction e（x，y，z，t：Bool）：HBoolreturn c（x，y，z，t）·HHHd（x，y，z，t）function z（x，y，z，t：Bool）：Bool返回e（x，y，z，t）+HBBt开始输入（w1，w2，w3，w4）输出（z（w1，w2，w3，w4））端程序P2var w1，w2，w3，w4：Boolfunction+BBH（x，y：Bool）：HBoolfunction+HBH（x：HBool;y：Bool）：HBoolfunction+HBB（x：HBool; y：Bool）：Bool函数·HHH（x：HBool; y：HBool）：HBool函数·BBH（x，y：Bool）：HBool函数a（x，y，z，t：Bool）：HBoolreturn x+BBH yfunction b（x，y，z，t：Bool）：HBoolreturny·BBH zfunction c（x，y，z，t：Bool）：HBoolreturn1H函数d（x，y，z，t：Bool）：HBool返回b（x，y，z，t）+HBHtfunction e（x，y，z，t：Bool）：HBoolreturn c（x，y，z，t）·HHHd（x，y，z，t）function z（x，y，z，t：Bool）：Bool返回e（x，y，z，t）+HBBt开始输入（w1，w2，w3，w4）输出（z（w1，w2，w3，w4））端Fig. 1. 规范S的两个实现。Ax=AxHBA{a（x1，x2，x3，x4）=x1+BBHx2，b（x1，x2，x3，x4）=x2·BBHx3，c（x1，x2，x3，x4）=a（x1，x2，x3，x4）·HHHb（x1，x2，x3，x4）d（x1，x2，x3，x4）=b（x1，x2，x3，x4）+HHHx4e（x1，x2，x3，x4）=c（x1，x2，x3，x4）·HHHd（x1，x2，x3，x4）o（x1，x2，x3，x4）=e（x1，x2，x3，x4）+HBBx4}公理AxHBA是布尔代数中隐藏和可观察排序的定律。在图1中给出了S这两个程序只在函数c中有区别。在程序P2中，函数c总是返回1H，这表示被称为与门卡住的故障。根据代数测试技术设计的示例测试用例是以下基础项：c（0B， 0B， 0B， 0B）+HBB0B=（a（0B， 0B， 0B， 0B）·HHHb（0B，0B， 0B， 0B））+HBB0B程序P1通过此测试用例。然而，正如预期的那样，P2没有通过测试，因为它的评估结果是1B = 0B124B.K. 艾希尼格角George/Electronic Notes in Theoretical Computer Science 164（2006）115这是错误的这个例子的有趣之处在于，两个实现的输入输出行为是等效的。因此，由P1和P2计算的真值表是相同的，但是由代数测试方法产生的测试用例拒绝P2。B.K. 艾希尼格角George/Electronic Notes in Theoretical Computer Science 164（2006）1151254.4该方法不处理非确定性程序Haeberer等人扩展了他们的Bootstrap方法来处理非确定性程序，我们没有理由认为经典的代数测试方法不能进行类似的扩展。本质上，对于给定的输入，存在一个明确定义或由其特征谓词定义的预期输出的集合，并且该集合的任何成员都被接受为测试用例的成功4.5不完整的细化检查Haeberer的反例的基本原则[23]）。同样，测试用例可以被看作是抽象的（或者是测试用例的细化）。显然，从代数规范导出的基项方程必须在规范中成立，并且也应该在实现中然而，这种断言性的细化是不完整的。例如，在规范中存在隐藏函数，而这些RAISE方法不需要实现隐藏函数，建议使用此扩展来证明此类精化[27]。然而，在黑盒测试中，这并不总是可能的，因为被测实现的源代码可能不可用。因此，可能会发生测试用例未能显示细化，尽管实现在观察上等同于正确的实现。其结果似乎是假阴性。然而，由于代数测试方法将其一致性关系建立在公理化的基础上，因此我们不能谈论该方法的失败。 代数检验者只需要记住，在某些情况下，他的公理检验比观察等价更严格。同样的情况也可能发生在基于状态的规范中，如果使用正向模拟由于众所周知的是，正向模拟是不完整的，再次假阴性可能发生4.5Bootstrap测试是一种替代方法吗？我们记得假设演绎法涉及从背景理论加上我们的假设中预测证据，然后确认实际证据与预测的一样这符合标准的软件工程实践，例如在项目早期编写验收测试的标准建议，需求的基础（无论这些需求是正式的还是用自然语言表述的）。这种验收测试是根据要求理论进行的预测。[4]是吉姆·伍德科克（Jim Woodcock）向我们指出了前向模拟的不完全性和基于模型的测试之间的关系。126B.K. 艾希尼格角George/Electronic Notes in Theoretical Computer Science 164（2006）115bootstrap方法的工作原理是相反的。它首先采用证据，然后从中推导出理论假设（实例）。因此，例如，从我们的排序程序生成其输入的排序版本的证据中，我们可以确认（再次找到积极的证据）输出是输入的一种类型的假设。这种方法在科学中很常见。例如，从行星轨道的观察中，开普勒首先假设轨道是椭圆形的，太阳在焦点上，牛顿后来假设引力的平方反比定律也被同样的观察所证实。正如Haeberer所指出的，当证据与理论发生冲突时，通常被拒绝的是理论。这花了很长时间，但我们最终接受了证据，并拒绝了太阳系的托勒密理论，尽管我们更喜欢优雅和简单的圆圈。但是在软件测试中，这样的冲突通常会导致我们拒绝程序，因为它不能确认它的理论，需求。因此，Haeberer提出了一种自举方法的逆转：我们想要确认程序，而不是它的理论。但在另一个相关的意义上，它似乎也是相反的。我们构造程序是为了让它具有某些属性：需求。一开始，我们有理论，但没有证据。如果我们不能或不应该从理论中预测测试用例，我们如何编写验收测试？自举方法还有其他需要满足的条件，我们在这里非正式地说明。我们假设我们有一个理论T，一个假设H，一个有待检验的关于这个理论的（不）方程，以及一些证据E，它由一组变量的一组值组成。我们假设H和T是相互一致的，并且H可以被E无效。要使ESTT，H，EESTT被视为引导模式，必须：(i) 利用T的某个子理论Tx，可以从E中的值计算出H的所有本质变量的值。(ii) 这些值满足H。(iii) 方程K中不存在本质变量是使得H，TK和K，TH。(iv) 方程K中不存在本质变量是使得理论H<$Tx和K等价。方程的条件3背后的直觉是，否则，如果变量y对H是必不可少的，但对K不是必不可少的，则y将由H和T确定，因此将不由证据确定。我们希望H不强于证据所证明的条件4背后的直觉是，否则基于与H无关的证据的虚假反驳是可能的。对引导模式的描述有很多变化，但基本思想是相同的。 实际问题也是一样的：自举模式涉及的条款，特别是一个（内）方程的基本变量和存在的（内）方程具有特定的属性，这是B.K. 艾希尼格角George/Electronic Notes in Theoretical Computer Science 164（2006）115127理论上的证明。可以计算吗？如果没有，实际的方法是什么？应该注意的是，Haeberer给出的处理是针对一种受限的形式主义：存在方程逻辑。据我们所知，将它扩展到其他形式主义仍然有待探索。6结论Armando Haeberer他通过将测试理论与认识论联系起来来展示问题。这是他介绍的假设演绎的方法，导致主要观察本文提出：细化及其双重抽象可能会导致问题时，不小心应用于测试。我们发现，由于应用HD，测试用例可能变得过于抽象（弱），无法可靠地确认规范。HD的另一个基本局限性与某些精化证明方法的不完备性有关。这一问题需要进一步研究和讨论。如果提出的问题存在，并且是众所周知的，则需要重新考虑现有的测试框架。本文的目的就是要展开这样的讨论。在试图描述Haeberer的哲学反对意见时，这绝不是说反对意见可以被驳回：存在着诸如充分处理隐藏功能同时保持稳健性的实际问题。我们怀疑可能有一些规范风格可以改善一些问题，但这需要探索。也不清楚引导测试能有多大帮助，因为到目前为止，还没有自动化。一种可能的技术可能是约束求解。另一个有趣的问题是，人们可以在多大程度上将这两种方法结合起来。类似于模拟技术，在需要向前和向后模拟的情况下，在假设演绎方法失败的情况下，可以使用引导测试。我们非常遗憾Armando于2003年去世，不能继续参加这些讨论，他在哲学和软件工程方面的背景将是无价的。他担任我们的同事和我们研究所所长的时间太短了。我们必须始终意识到他的结论：我们忽视了我们所做的事情的基础，这是危险的。确认我们非常感谢玛丽-克劳德·高德尔对本文初步版本的详细评论。128B.K. 艾希尼格角George/Electronic Notes in Theoretical Computer Science 164（2006）115引用[1] 艾 希 里 希 湾 K. ， Test-design through abstraction ： a systematic approach based on the refinementcalculus，Journal of Universal Computer Science 7（2001）. 710-735[2] 艾希里希湾K.，精化演算中的突变测试，计算的形式方面杂志15（2003），pp. 280-295。[3] 艾希里希湾K.和p. A. Pari Salas，通过OCL突变和约束求解生成测试用例，在：K.- Y. Cai，A. Ohnishi和M.Lau，editors，QSIC 2005，Proceedings of the Fifth International Conference on Quality Software，Melbourne，Australia，September 19-21，2005（2005）.六四比七十一[4] Barbey，S.和D. Buchs，Testing Ada abstract data types using formal specifications. 第一届欧洲空间-Ada-欧洲国际研讨会，计算机科学讲义887（1994），第11页。76比89[5] Bernot，G.，M.- C. Gaudel和B. Marre，《基于正式规范的软件测试：一个理论和工具》。，SoftwareEngineering Journal 6（1991），pp. 387-405[6] 布乌盖湖，“M o d ′ e lista t i o n d e l a n t i o n d e t e t e t e p r g r amm es，a pp li c a t i o n ` a l a p ro duct i o n d e j e u x t e s t，”Ph. D. Thesis，UniversitédeParis6（1982）.[7] 布乌盖湖， AContribut iontheryofpramtesting，TheoreticalComp ut erSc i ence37（1985），pp. 151-181.[8] 博乌盖湖，N. 乔凯湖 Friborg和M。-C. Gaudel，Te stsetgene rati on fromalgebraicp e fi cati onsusinglogic programming. Journal of Systems and Software 6（1986），pp. 343-360[9] Cengarle ， M. 诉 和 A.M. Haeberer， Towards an epistemology-based methodology for verificationandvallidatin te sting g，technicacalreport，Ludw i g-M aximili ans-U ni versi t？t？t？t？Mu？nchen，unpublisheddraftofMarch 2，2000.[10] Cengarle，M. V.和A. M. Haeberer，一种基于规范的黑盒测试的正式方法，在：在快速移动场景中建模软件系统结构研讨会论文集，2000年6月13-16日，Santa Margherita Ligure，意大利，2000年。[11] 陈 洪 ， T. Tse 和 T.Chen ， TACCLE ： A Methodology for Object-Oriented Software Testing at theClass and Cluster Levels ， ACM Transactions on Software Engineering and Methodology 10（2001），pp.56比109[12]Claessen，K. J. Hughes，Quickcheck：a lightweight tool for random testing of Haskell programs，in：第五届ACM SIGPLAN函数式编程国际会议（2000年），pp。268-279。[13] 丹 湖 ， 澳 - 地 和 B.K. Aichernig， Combining algebraic and model-based test case generation ， in ：Proceedings of First International Colloquium on Theoretical Aspects of Computing ， Guiyang ，China 20-24 September 2004，Lecture Notes in Computer Science 3407（2004），pp. 250-264。[14] Dick，J.和A. Faivre，Automating the generation and sequencing of test cases from model-basedspecifications，in：J. Woodcock and P. Larsen，editors，Proceedings of FME268-284。[15] 东河，巴西-地和p.Frankl，ASTOOT方法测试面向对象程序，ACM软件工程与方法学汇刊3（1994），pp.103-130[16] Gannon ， J. ， P. McMullin 和 R.Hamlet ， Data abstraction implementation ， specification andtesting，ACM Transactions on Programming Languages and Systems 3（1981）.211-223[17] Gaudel，M. C.的方法，测试也可以是形式化的，见：TAPSOFT82比96[18] Gaudel， M.C. 和 p.R. James ， Testing algebraic data types and processes ： a unifiing theory，Formal Aspects of Computing 10（1998），pp.436-451[19] Gaviour，C.，Hypothetico-deductivism is hopeless，Philosophy of Science 47（1980），pp. 322-325[20] Gaviour，C.，[21] Haeberer ， A. M. 和 T. S. E. Maibaum ， Scienti fic rigour ， an answer to a pragmatic question ： alinguistic framework for software engineering，in：Proceedings of the 23rd International Conferenceon Software engineering，Toronto，Ontario，Canada（2001），pp. 463-472.[22] 霍尔角和H.纪峰，B.K. 艾希尼格角George/Electronic Notes in Theoretical Computer Science 164（2006）115129[23] Jacobs，B.，在coalgebraic specification断言和行为细化，电子笔记在理论计算机科学47（2001），页。1-36.[24] Legeard ， B. ， F. Peureux 和 M. Utting ， 来 自 Z 和 B 的 自 动 边 界 测 试 ， 在 ： L.- H. Eriksson 和 P.A.Lindsay， editors ， Proceedings of FME 2002 ： Formal Methods-Getting IT Right ， InternationalSymposium of Formal Methods Europe ， July 2002 ， Copenhagen ， Denmark ， Lecture Notes inComputer Science 2391（2002），pp. 21-40.[25] M ai baum，T.， InmemoriamArmandoMart'ınH ae ber er r，in：B. K. AichernigandT. Maibaum，editors，Formal Methods at the Crossroads：From Panacea to Foundational Support，Lecture Note
