智能类回归测试选择算法的安全性

可在www.sciencedirect.com在线获取理论计算机科学电子笔记351（2020）51-73www.elsevier.com/locate/entcs智能类回归测试选择算法的安全性Susannah Mansky苏珊娜·曼斯基1，2艾尔莎湖Gunter3美国伊利诺伊大学厄巴纳-香槟分校计算机科学系摘要回归测试选择（RTS）算法选择哪些测试要对修订的代码进行验证，从而减少检查新引入的错误所需的时间。RTS算法被认为是安全的，当且仅当所有被取消选择的测试将具有不变的结果。在本文中，我们提出了一个正式的RTS算法的安全性证明的基础上使用的Ekstazi[3]，Java库的回归测试。Ekstazi的算法将print语句添加到JVM代码中，以便收集测试在执行过程中使用的类名在一个节目上。当程序被改变时，测试只在它们使用的类改变时才被重写。他们的算法中的主要见解是，并不是所有类的使用都必须注意，因为许多类需要以前的使用，例如使用以前创建的对象时。我们在这里正式定义并证明安全的算法使用仪表化语义来收集更小位置集合中的触摸类。我们发现Ekstazi的当前集合位置集存在问题，使其不安全，然后提出修改后的集合这将使它等同于我们的安全集。本文给出的定理已经在定理证明器Isabelle over JinjaDCI[7]中形式化，JinjaDCI是Java和JVM子集的语义，包括动态类初始化和静态字段和方法。我们通过给出集合语义（Collection Semantics）的一般定义来检测JinjaDCI的JVM语义，在执行过程中检测的小步骤语义收集信息。我们还给出了RTS算法的正式一般定义，包括安全性的定义关键词：交互式定理证明，回归测试选择，小步语义，Java1介绍测试是编写代码的关键部分。在编写程序时，运行测试来证明这些程序的行为与预期的和记录的一样是很重要的。当一个程序被修改时，它的测试会被检查，以确保修改没有引入新的bug。这种重新运行的测试称为回归测试。[1]本材料是基于国家科学基金会资助的CCF-1439957和CCF 13-18191的部分工作。 任何意见、发现、结论或建议在本材料中的是作者的观点，并不一定代表NSF的观点。我们想感谢Milos Gligoric和Darko Marinov提供了激励问题，并对 初始化时间的重要性。 我们也感谢审稿人的时间，建议，和评论。2电子邮件地址：sjohnsn2@illinois.edu3电子邮件地址：egunter@illinois.eduhttps://doi.org/10.1016/j.entcs.2020.08.0041571-0661/© 2020作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。52S. Mansky，E.L.Gunter/Electronic Notes in Theoretical Computer Science 351（2020）51在实践中，一个代码体可能很大，并且有大量的测试写在上面。在某些情况下，重新运行每一个测试可能需要几个小时或几天，使得在每一个小的变化之后都运行它们是不切实际的。然而，大多数的变化甚至可能只会影响少量的测试。因此，已经开发了算法和方法来选择在代码更改后要验证哪些测试。选择要运行的测试（或者取消选择不应被忽略的测试）的过程称为回归测试选择（RTS）。如果RTS算法仅取消选择那些在修改后的程序下可以重现先前结果的测试，则该算法是安全的在Java中，所有代码都是在类的方法中编写的。因此，RTS的一种方法是让Java测试套件确定每个测试使用哪些类（“接触”），然后只有当它的一个接触类被更改时才重新测试。Ekstazi[3]是一个用于回归测试的Java库，它在RTS算法中使用了这种方法接触类可以以多种不同的方式派生，但Ekstazi的算法通过代码的插装来实现这一点的简单方法是对每个类的每次使用进行仪表化。然而，Ekstazi使用了一种更聪明的方法，认识到这些集合中的许多可能是冗余的。例如，获取一个对象的字段要求该对象之前已经创建，这意味着一个new已经在它的类上运行，所以getfield不需要触发类收集。他们的方法使用这些见解来减少收集点的数量。在本文中，我们提出了一个正式的RTS算法的安全性证明Ekstazi使用类似。我们的算法是为最小集合而设计的。 然后，我们证明了它的安全性，并展示了如何Ekstazi的算法可以修改是等价的，因此是安全的（并说明为什么前一组不安全）。通过对JinjaDCI的JVM语义的插装给出了该算法的定义。这些语义是在定理证明器Isabelle中编写的JVM子集的模型，在[7]中有很大程度的描述。插装是通过我们为所谓的集合语义给出的一般定义创建的，集合语义允许通过输入这种语义和集合函数来收集小步语义的信息。我们还给出了RTS算法的一般定义，其中包括安全性的定义。它的公理，包括安全性，进一步保证了测试的重复描述可以安全地基于程序的前一个版本的输出。4第2节概述了回归测试选择（RTS）、Ekstazi和JinjaDCI。第3节详细介绍了几个不同的类收集函数，用于使用类接触方法选择测试的RTS算法。第4节描述了集合语义，我们用集合函数来插装现有语义的方法，并使用这种方法用前面描述的类集合函数插装JinjaDCI（这些声明是集合语义定义的实例化第5节4这是RTS算法的一个重要特性，因为取消选择的测试在设计上是不重复的，所以在重新选择之前不要提供新的输出S. Mansky，E.L.Gunter/Electronic Notes in Theoretical Computer Science 351（2020）5153给出了RTS算法的一般Isabelle定义，包括安全性的正式定义，然后将其与集合语义定义相结合，以定义基于集合的RTS算法。使用该组合定义，将描述仪表化JinjaDCI JVM语义的集合语义的实例化扩展为基于集合的RTS算法实例化。第6节使用一般RTS定义和工具化语义来证明使用定义的类集合函数作为类接触RTS算法的基础的安全性。最后，第7节和第8节讨论了一些相关的工作，总结并提出了未来的发展方向。Isabelle的开发工作可以在网上找到，https://github.com/susannahej/rts网站。2背景我们将首先介绍本文中使用的相关主题和工具2.1RTS算法和Ekstazi在工业中，许多代码库非常大，与之相关的测试套件也是如此。 这些测试套件可能需要几天的时间才能完全运行。 回归测试选择（RTS）是在对代码库进行更改后选择哪些测试进行重新测试的过程，以减少重新测试所花费的时间。未运行的测试称为取消选择。如果RTS算法只取消选择结果不变的测试，则该算法被称为安全Ekstazi[3]是一个用于回归测试的Java库，它基于每个测试使用或引用的类在JVM字节码级别使用RTS我们称这些类为测试所涉及的类。当测试运行时，它在执行过程中涉及的类的名称将被收集。然后，当对代码库进行更改时，只有当它在以前运行中触及的一个或多个类被修改时，测试才会被重新命名。因此，例如，如果在一个大型代码库中只对非核心类进行了几次修改，通常只需要进行很少的测试。Ekstazi具有尽可能少的收集触发器），这为可能的收集不足留下了空间为了形式化地证明该算法静态指令和动态类初始化尤其是类收集算法可能会出现细微错误的地方。在2.2节中，我们将更详细地讨论包含这两个特性的JVM的语义。2.2伊莎贝尔和JinjaDCIIsabelle允许我们对语言和用它们编写的程序建模。它还允许证明这些语言和程序的许多有用属性，例如54S. Mansky，E.L.Gunter/Electronic Notes in Theoretical Computer Science 351（2020）51如在执行具有简化语义的程序期间收集的信息如何与该程序相关Jinja[4]是在定理证明器Isabelle中开发的一个框架，其目的是以统一的方式为Java和JVM字节码的子集提供形式化的语义。作者用Isabelle编写语义，因为这允许他们基于语义编写定义和证明。这些证明包括类型安全性、大步长和小步Java语义的等价性，以及编译器从Java语义到JVM语义的正确性。Jinja的两个扩展是JinjaThreads[6]和JinjaDCI[7];前者用线程扩展Jinja，而后者用静态字段和方法以及动态类初始化扩展它后者的特性是类在Java中的重要用途出于这些原因，这些功能对于像本文讨论的Ekstazi一样的触摸类集合RTS算法的安全性证明非常重要。另一方面，只要初始化的同步是正确的，线程就不应该对这些算法的安全性产生任何复杂性（如6.4节中进一步说明的）。因此，我们选择了JinjaDCI作为我们的语义模型，用于这里提供的证明使用像Isabelle这样的系统来构建语义框架的价值恰恰在于能够证明这些结果，这就是为什么我们选择使用这一框架：为了证明一个测试在两个不同的程序上的行为是相同的，我们需要一个语言的定义和一个允许在这个级别上进行元推理的框架。在Jinja的JVM指令名称是大写的，并采取适当的参数。例如，new被写为New，并接受一个参数：要实例化的类的名称C;getfield被写为Getfield，并接受两个参数：其值被获取的字段的名称F，以及在被传递的对象中定义该字段的类的名称C。2.2.1动态类在JVM中，类初始化方法是动态调用的。Java并不预先初始化类，而是等到实际使用该类时才初始化.当使用类C时，检查其初始化状态。如果未初始化，则在其上运行类初始化过程当使用一个类或它的一个子类时，将检查其状态。特别地，在支持的JVM指令子集中，如果类C未初始化，则在以下情况下调用类初始化过程• new、getstatic、putstatic或invokestatic引用之间的指令C，• C的一个• 在JVM启动时，如果C是指定的初始类。在完整的JVM中，该过程也会在某些引导和响应方法的调用时被调用，以及在初始化实例时在某些接口S. Mansky，E.L.Gunter/Electronic Notes in Theoretical Computer Science 351（2020）5155类初始化过程5（在类C上调用）的第一步是检查C如果状态为Error，则返回一个错误。否则，如果C需要初始化（并且尚未初始化），则检查其超类，并在必要时在其上运行过程。然后，如果该过程正常返回，则运行C如果C或它的任何超类的方法抛出一个未捕获的异常，那么C的初始化状态被设置为Error，它的初始化方法不会运行。 6在检查了已经初始化的超类或检查了Object类（没有超类）之前，不会运行类初始化方法。在这一点上，所有未初始化超类的初始化方法都是从上到下运行的，以C结束注意类的初始化过程与类的初始化方法是如何不同的后者是一个实际的方法，由类的定义隐式或显式定义，在类初始化过程中调用。注意，如果一个类在程序执行期间调用了初始化过程（初始化调用类），那么这个类在执行期间被触及。(This set包括但不一定限于实际初始化的那些类。 类可能调用初始化过程但无法运行它的初始化方法，如果它的超类的初始化方法之一返回错误。由于本文中描述的RTS算法通过收集测试所涉及的类的名称（即，这些类的定义可能与被监视的运行无关），初始化调用的类是将被收集的类的很大一部分特别地，除了这些，在运行中唯一涉及的其他类是那些调用由它们的超类之一定义的静态方法或字段的类。这些后者可以很容易地收集在这种呼吁的时候。收集被初始化调用的类可以在初始化过程开始时完成，也可以通过在可能调用该过程的点收集来完成在初始化检查时）。前者需要插装JVM的实际语义，因为初始化过程是动态调用的，而不是通过代码中的指令。我们在算法中采用了这种方法。后者可以通过向测试代码添加指令来实现，这是Ekstazi5这里描述的过程很简单，并假设没有线程的语义，如Jinja和JinjaDCI。JVM规范[5]和JinjaDCI中给出了这个过程的更精确的细节论文[7]。返回抛出的异常，任何进一步初始化该类的尝试都将在初始化状态检查期间导致错误，如第一步所述56S. Mansky，E.L.Gunter/Electronic Notes in Theoretical Computer Science 351（2020）512.2.2JinjaDCI本文描述的类收集算法是通过JinjaDCI的JVM语义来实现的。未插装的语义在[7]中有更详细的描述，但以下部分是与插装最相关的语义的简要总结在JinjaDCI中，就像在Jinja中一样，程序是类定义的列表。JinjaDCI JVM状态σ由堆、静态堆（存储有关静态字段和类的初始化状态的信息）、帧堆栈（每个活动方法一个帧）和可选异常组成。JinjaDCI JVM其帧堆栈非空。 帧包括初始化调用状态标记，指示其相对于初始化过程的当前状态。这个构造器可以由四个构造器之一构建，调用，抛出，没有ICS。 它们的用途如下：如2.2.1节所述，该过程首先创建一个要初始化的类列表，包括触发类C及其未初始化的超类。在该过程的这一部分期间，调用它的帧将其初始化调用状态标记设置为CallingClCs，其中Cs是到目前为止找到的未初始化类的列表（ Cl是最近添加的）。完成此列表后，将标记设置为CalledCl#Cs，并为Cl#C顺序。 如果这些方法中的任何一个抛出了未捕获的异常，设置为ThrowingCsJa，其中CsJ是其方法未运行的类的列表。 如果帧不在类初始化过程的中间，则标记为No ics。3类相关集合函数在本节中，我们将描述RTS算法所使用的集合函数，其安全性将在第6节中讨论。所有这些算法都收集在程序上执行测试的过程中所涉及的类的名称。然后，当程序被改变时，被触摸的类没有改变的测试被取消选择。我们使用了两种不同的一般方法来进行这种收集。每一项的要点如下：• 朴素的方法：在执行的每一步，收集每一个可能执行这一步的类.• 更聪明的方法：在执行的每一步，只收集那些可能会影响该步骤的类，因为步骤类型不能被安全地假定在其他步骤中收集。(That使用上下文保证的知识来减少收集类的频率。使用朴素集合函数的算法更容易被证明是安全的，因为它在执行的每一步都是安全的。一旦它的安全性得到证明，它就可以用来证明一个定义正确的智能收集函数的安全性，方法是显示它收集相同的类。出于这个原因，我们将给出这两个例子，使用第一个的安全性证明来证明第二个的安全性S. Mansky，E.L.Gunter/Electronic Notes in Theoretical Computer Science 351（2020）51573.1一个朴素的算法简单的方法是在每一步收集可能改变该步行为的每个类。如果使用对象，则算法收集名称对象的类及其所有超类。例如，如果一个静态方法被调用，它会收集被引用的类及其所有超类。如果做得足够彻底，很容易理解为什么这种方法收集了足够的类来形成安全取消选择算法的基础。因为对于每一步，可能改变这一步下面我们给出算法的细节。当一个类被收集时，它的超类也被收集.收集如下：(i) 在执行的每一步，收集错误类和帧堆栈中每个帧的当前类(ii) 另外，根据当前帧的初始化调用状态收集(a) 调用CCs：收集C(b) 调用（C#Cs）：收集C和定义C(c) 抛出Csa：收集堆上地址a处的对象的类(d) 无ics：根据当前指令收集• NewC 、 GetstaticC F D 、 PutstaticC FD 或 PutkestaticCMn7 ：collectC• GetfieldF C、PutfieldF C、CheckcastC、CheckkeM n或Throw8：如果正确提供，则收集调用或抛出对象的类;9否则，不收集任何内容• 对于任何其他指令，不收集任何信息注意，这个算法并不直接依赖于JVM的行为。虽然它的行为与第2.2.2节中描述的JVM的语义并行运行，但每一步的收集仅依赖于该步的初始状态。这在第4节中将是重要的，该节描述了如何将这种语义无关的算法与小步语义平滑地结合起来，以给出工具化的语义。然而，虽然这种方法收集了最小的被接触类集，但它也是通过不必要地一次又一次地收集相同的类来实现的这种洞察力导致了一种更聪明的方法。[7]纽的论证如第2. 2节所述。 GetstaticObjectivestatic8Getfield和Putfield的参数如2. 2节中Getstatic的描述。 Checkcast的参数是要强制转换的类C。Replike在JVM中，这些指令都期望在堆栈上的指定位置存在一个适当对象的地址。如果预期的对象不存在，则引发错误。注意，如果对象如果缺少，则实际上不会触及任何类，或者除了错误的类之外，不会检查指令的结果。58S. Mansky，E.L.Gunter/Electronic Notes in Theoretical Computer Science 351（2020）513.2更智能的算法更聪明的方法认识到正确程序的一些事情：(i) 如果使用对象，则意味着该对象是由新的指导。(ii) 直接触及类的指令（new和静态指令）将必然导致该类（及其超类）在指令解析之前被初始化。(iii) 任何帧的当前类将是该帧的当前方法的初始类或定义类;在前一种情况下，类在当前测试执行开始时初始化;在后一种情况下，(iv) 如 果 帧 的 初 始 化 调 用 状 态 为 Called （ C#Cs ） ， 则 在 某 些 时 候 它 是CallingCCs。从这些观察中可以得出结论，指令对类的多次使用实际上可以保证该类以前已经被使用过，因此已经被收集。通过不在任何可以保证这一点的地方收集，实际上必须收集类的地方的数量大大减少。结果将是收集相同的类集合，但是每个类的收集次数将减少很多，这意味着增加的开销更少。经修订的收款方法如下：• 在类初始化过程被调用时收集类（即，帧的初始化调用状态为“为某些C调用CC”）• 在getstatic、putstatic或invokestatic指令上：· 如果字段/方法不存在，则收集引用的类及其所有超类· 如果字段/方法确实存在，则收集被引用类和声明类之间的所有类（包括被引用类，但不包括声明类）• 收集错误类及其超类请注意，当对类C调用类初始化过程时，在过程开始时收集C，而不是C的（回想一下2.2.1节中类初始化过程和类的初始化方法之间的区别这是必要的，因为在过程中，C但是，即使在这种情况下，也必须收集C，因为对C的更改可能包括更改其超类的名称。在Java中，运行一个程序（或测试）实际上是运行一个类的静态方法。 这个类是最初的类，在运行其静态方法之前初始化S. Mansky，E.L.Gunter/Electronic Notes in Theoretical Computer Science 351（2020）5159这个算法是通过不收集任何保证类已经被以前的使用收集过的地方来构造的。此外，这些先前的使用中的每一个仍然是收集点，或者被其自己的先前使用所覆盖，一个收集点 因此，可以看出，上面收集了相同的类就像朴素算法那样。因此，只要朴素算法是安全的，这个更聪明的算法也是安全的 我们将在第6节中正式证明这些观察结果。然而，下面是一些非正式的推理，涉及天真算法收集类的每个地方。首先，在这种方法中，错误类的收集只发生一次，而不是在每个步骤中。简单的算法只需要在每一步收集这些类，因为它的设计方式使每一步都是安全的。对于这个算法，证明安全性必然涉及确认类在执行期间的某个点被收集，因此在开始时收集一次实际上，即使在那时也不一定需要收集这些类，因为它们将被初始化。在这里，预先收集这些类只是作为Jinja处理错误类的方式的工件（通过预先实例化它们）。第二，正如上面的观察列表所指出的，每个帧的当前类是声明该帧正在处理其执行的方法的类。除了初始帧之外，每个帧都是由一个fixke或fixestatic指令创建的。在任何一种情况下，声明被调用方法的类都被其他情况收集。初始帧初始方法被执行，因此在该点被收集第三，Called和Throwing初始化调用状态不需要收集任何东西，因为前者由Calling处的收集覆盖（其被保证为在先前执行步骤中的init调用状态），而后者由其对现有对象（由新指令创建）的使用覆盖最后，当静态指令运行时，在声明类的初始化状态之前检查正在使用的字段或方法的存在。因此，如果字段或方法找不到（如果找到了字段或方法，则在声明它的类上调用初始化过程。声明类将按照前面的收集规则在过程开始时被收集，其所有超类也是如此（通过在此过程调用期间初始化，或者在之前初始化它们的任何过程调用期间初始化）。因此，在被引用类及其超类中，只有被引用类和声明类之间的类不会通过过程收集，因此必须在此时收集新的C总是导致初始化C和它的超类，所以它不需要收集任何东西。其他指令根本不需要收集任何类。这是从本节开始时给出的观察结果得出的，因为所有其他收集指令都使用由新指令创建的对象（这反过来又在相关类的初始化之前）。综上所述，如果类的名称在其类的开头收集60S. Mansky，E.L.Gunter/Electronic Notes in Theoretical Computer Science 351（2020）51初始化过程，那么只有当它能够改变行为但没有初始化或检查初始化状态时才需要收集它。唯一可能发生这种情况的地方是那些引用类以访问由其超类之一声明的字段或方法3.2.1Ekstazi在Ekstazi的算法中，就像在更聪明的算法中一样，只有某些使用才会触发收集，这取决于这样一个事实，即某些使用必须在该类的另一个使用之前。然而，与上面描述的算法不同，这些算法是通过JVM语义的插装来执行的，Ekstazi的算法在类使用之前将print语句添加到代码中。更智能的算法部分地工作，因为语义而不是代码被插装，这意味着可以插装类初始化过程以代码插装不允许的方式收集类（因为对类初始化过程的调用在运行时动态发生，而不是通过代码中的指令）。因此，Ekstazi的收集功能需要从我们的一些调整，以实现相同的效果。这些调整相当于将初始化开始时的收集替换为在可能运行初始化过程的任何位置之前的收集。即使假设是语义而不是代码的插装，在Ekstazi中，多个测试可以在同一个JVM上运行，这意味着某些类可能已经在任何特定测试开始时初始化了。在这种情况下，有必要在所有可以调用初始化的地方进行收集，因为实际调用只会发生在尚未初始化的类在同一个JVM中运行多个测试确实会引入状态污染的问题：静态字段的值可能会被一个测试更改并被另一个测试使用，这可能会影响后者本文不考虑国家污染的影响。同样值得注意的是，由于语义的不完整性，Ekstazi无法收集Jinja方法的两个地方：反射调用和接口调用。（Jinja或其扩展都没有建模。根据JVM规范，类初始化过程是在“调用某些相关方法”时调用的。因此，如果收集发生在类初始化过程的开始（如在更智能的算法中），则不需要在这些调用中收集，否则需要在那里收集（如在Ekstazi中）。对于接口，invokeinterface指令不会导致调用初始化因此，有必要在一个上下文中使用此指令，不管语义或代码插装。我们把这一补充留给今后的工作。11总之，这就是Ekstazi算法应该做的(i) 通过print语句收集以下指令涉及的类[11]由于接口的行为很像不能被实例化的类，包括它们以类的方式被初始化，我们不相信如果以同样的方式处理，增加接口会给这里给出的证明带来任何问题。 也就是说，在更智能的算法集合中，在Ekstazi的算法中，当初始化过程被调用时，它将被收集。在调用接口方法之前以及在收集扩展它的类时收集S. Mansky，E.L.Gunter/Electronic Notes in Theoretical Computer Science 351（2020）5161//testclassT{public static void main（.）{//静态方法调用;在声明类CC.M（）时调用初始化过程;}}classD{static{ throw e;}//类初始化方法}class//类初始化方法默认为空}//C//当在C上调用初始化过程时，在运行C的init方法之前在D上调用init过程staticvoid M（）{}}//修改C//直接超类被更新;init过程现在将在Dpublic}Fig. 1. Ekstazi没有收集足够在此之前添加：• new，getstatic，putstatic，invokestatic，invokeinterface指令• 引用相应的方法(ii) 收集所有错误类（或者更确切地说，将它们全部视为所有测试的接触类）在第6.3节中，我们将证明这种方法的安全性。Ekstazi这些收集太晚了，使它不安全。例如，考虑图1中给出的代码。当使用C的原始代码运行测试时，Ekstazi将收集类D，因为它的初始化方法正在运行，但不是C，因为D的初始化方法抛出的错误另一方面，我们的智能算法将在调用其初始化过程时收集C。测试在原始代码下失败，在更改后的代码下成功，因此应再次运行。然而，唯一的变化是C类，这意味着Ekstazi不会取消测试。4集合语义类似于第3节中描述的类收集算法的信息收集的添加可以通过在步骤的正常行为之上添加相关信息的集合来检测相关语言的语义来建模一种方法是直接修改相关语言的现有语义，在状态中添加一个额外的片段来跟踪信息62S. Mansky，E.L.Gunter/Electronic Notes in Theoretical Computer Science 351（2020）51正在收集。然而，这种方法的结果在语义没有直接证明的数学等价行为的原始语义。证明为了使用其结果，需要这种等价性。由于结果包括一个保证，证明了结果的工具化语义保持在原来的，证明等价性是必不可少的有用性的新的语义。此外，插装的语义需要手动保持等价。一个更好的方法是创建一个函数，它接受一个语义和一个集合函数，并产生一个仪表化的语义，我们将其称为集合语义。这允许一个关于函数的一般定理，该函数显示原始语义和工具化语义之间的行为等价性。然后，在任何输入上，这种等价都是直接的，并且在前者上证明的任何结果都可以立即应用于后者。此外，对原始语义的任何改变都将被反映在插装的语义中，而无需任何额外的排序。这样一个函数在Isabelle中最好通过使用locale来定义，这是一种定义组件集合的方法，这些组件上有一组公理。然后，这个关 于 l o c a l e 的 更多细节请参见第4.3节。一旦使用第3节中给出的朴素和智能算法实例化，就可以评估和比较所产生的语义的行为，允许我们证明它们作为测试取消选择机制的安全性我们通过首先将语义本地化定义为基础来定义CollectionSemantics本地化4.1语义语言环境我们首先给出一个语义的一般定义。定义4.1语义是一对：• 一种小步长函数small，它接受一个程序和一个状态，并返回一个集合下一个国家，以及• 一组端态，endset，最后一个公理是endset final：小P σ={}。请注意，这个定义指定了小步风格的语义。这使得收集函数更加语义无关：它只需要基于一个状态进行收集，假设一个步骤。给定一个Semantics，一个big-step语义函数big是使用endset从small派生出来的：big只是将small应用于输入，直到到达endset中的一个状态，然后返回该结束状态。4.1.1运行示例：语义实例语义语言环境可以用JVMexec函数实例化，它很小，endset是具有空帧堆栈或异常堆栈的状态集S. Mansky，E.L.Gunter/Electronic Notes in Theoretical Computer Science 351（2020）5163回想一下2.2.2节，exec在这个集合中的任何状态上都不返回下一个状态，满足语义公理endset final。4.2CollectionSemanticsLocale给定的语义定义，它是然后可能到延伸到CollectionSemantics。定义4.2CollectionSemantics是与三元组配对的语义• 一个集合函数collect，它接受一个程序和两个状态（之前和之后），并返回一个集合，• 一个函数combine，用于合并两个集合并返回另一个集合，• 组合函数的标识，收集ID，其中，combine是关联的，collect_id充当combine下的左标识和右标识。在上面，一个“集合”可以是从集合到整数再到文件的任何东西CollectionSemantics的small和collect部分被用来定义一个小步长插装语义csmall，然后用endset扩展成一个插装大步长语义cbig。 前者只是返回一组结果对，通过对输入应用small，然后对输入和输出应用collect返回。 后者返回将csmall应用于输入的结果，其次数与达到结束状态所需的次数相同，使用combine组合跨步骤收集的信息。请注意，如果未执行任何步骤，则生成的集合为标识集合ID。 由于csmall返回的状态与small返回的状态相同，因此cbig返回的状态也与big返回的状态相同。 然后，定义的任何证明实例将立即能够使用导出的cbig和其输出与导出的big相同的结果。4.2.1运行示例：CollectionSemantics第4.1.1节中给出的Semantics实例可以扩展为CollectionSemantics实例，并具有第3节中描述的朴素和智能类集合函数。 由于这些函数返回类的集合，所以组件combine和collect id分别是set union操作符和空集。 很容易看出，结合性公理和左恒等式和右恒等式是成立的。4.3使用区域设置在Isabelle中，定义由一组固定项（“组件”）和一组公理组成，可以使用区域设置给出。一旦给出了这些成分和公理，就可以发展依赖于它们的理论，包括定义和引理。人们可能会根据组件写一个定义，然后在给定公理的情况下证明关于该定义的事情这种方法64S. Mansky，E.L.Gunter/Electronic Notes in Theoretical Computer Science 351（2020）51用于将上述语义和集合语义的定义转换为区域设置，以及第5节中给出的定义。区域可以通过给出正确类型的具体定义来实例化，以匹配其组件，然后证明该组件的实例满足公理所要求的要求。一旦这样做了，就可以使用locale的理论，包括它包含的任何派生定义和关于它们的任何理论，以及证明从公理遵循的任何引理。5正式定义回归测试选择现在我们将给出RTS算法的正式的、一般的定义然后，我们将把这个定义与第4节中的CollectionSemantics结合起来，得到一个基于集合的RTS算法的定义。5.1RTS安全区域设置下面定义了一个安全的通用回归测试选择算法。定义5.1RTS保险箱是一个五元组：• 一组有效的程序progs，• 一组有效的测试测试，• 输出函数out，它接受一个程序并进行测试，然后返回一组程序输出，• 等价关系equiv out在程序输出对上，以及• 取消选择关系取初始程序、程序输出和修改后的程序，它满足以下公理：• 存在安全：对所有P，PJ，t，o 1，若P，PJ∈progs，t∈tests，o1 ∈outPt，且p∈ Po1 PJ，则p ∈o 2 ∈outPJt. 相当于O1O2，• equiv out equiv：equiv out是等价关系，• equiv out：如果equiv outo1o 2和P o1PJ，则P o2PJ。有效程序和测试的集合为安全公理提供了一个范围：算法只需要在这些给定的集合上是安全的。输出函数提供给定程序和测试的某种输出，例如语言的语义输出，用于运行程序测试。输出上的等价关系提供了一种直接比较输出的方法，以确定它们在安全性背景下是否被视为充分相似的结果述取消选择[12]请注意，这是可取的，而不是缩小范围，因为唯一相关的程序和测试是那些可以运行的程序和测试-那些满足通常由编译器强制执行的格式良好条件的程序和测试S. Mansky，E.L.Gunter/Electronic Notes in Theoretical Computer Science 351（2020）5165关系是算法的核心，它选择不运行的测试一对程序，加上一个输出。正如安全性公理中所给出的，这些将用原始程序、新程序和对原始程序运行测试的输出然后，取消选择将应用于产生给定输出的测试。此函数采用测试输出而不是测试，因为取消选择将基于实现的输出，因为可能有多个输出。我们在这里使用的安全属性是我们称之为存在安全的属性。此版本的考虑到非确定性语义来设计安全性：如果测试可以产生多于一个的结果，则它仅保证如果测试的原始输出导致其取消选择，则在改变的程序下至少有一个等效的结果。在这个定义下，如果一个简单的测试（即，在同一个程序下可以产生通过和失败的结果）被取消选择，这个公理保证它在改变的程序下仍然是可验证的。我们之所以选择这种安全性的定义，是因为我们在这里描述的算法并不是为了识别需要进行安全性测试的危险性。因此，这是一种安全承诺，这是预期和期望在这里。除了安全性之外的两个公理要求equiv out实际上是输出上的等价关系，并且是足够细粒度的，等价输出与函数是不可区分的。当结合起来时，这些公理足以证明以下内容：引理5.2安全传递性：如果一个非空的程序序列Ps都在progs中，testt在tests中，o0是Ps和t中第一个程序的输出，并且o0在序列中的每个顺序程序对下被取消选择，则在 P s 和 t 中 的 最 终 程 序 下 有一个输出等于o0。这个引理保证了在基于给定输出的取消选择之后， 继续使用该输出用于将来的取消选择决策是安全的，直到再次选择该测试。 这一点很重要，因为RTS算法的意图是在取消选择的测试被选中之前不会再次运行该测试，这意味着在此之前不会有更新的输出可供使用如第4.3节所述，RTS保险箱可以转换为现场。5.2CollectionBasedRTS区域设置在定义了CollectionSemantics（第4.2节）和RTS safe（第5.1节）之后，我们能够定义两者的组合，CollectionBasedRTS。这给出了RTS算法的一般形式，该算法使用在执行期间收集的信息来做出选择决策。定义5.3CollectionBasedRTS是CollectionSemantics的三元组; RTS安全，其输出返回一组状态集合对;以及对：• 一个函数maketestprog，它接受一个程序和一个测试，并返回一个修改后的程序，该程序包括运行测试的能力，以及• 一个函数collect start，它接受一个程序并返回一个起始集合，66S. Mansky，E.L.Gunter/Electronic Notes in Theoretical Computer Science 351（2020）51它满足了公理cbig：P t。好吧输出P t={（σJ，collJ）|coll.（σJ，coll）∈cbig（maketestprogP t）σcollJ= combinecoll（collect startP）}.CollectionSemantics 前者是一个通用的执行函数，允许在执行中的任何点启动。 后者只是运行测试，从给定的测试和程序中导出执行的开始状态。 因此，后者可以被看作是前者的一个特殊例子。CollectionBasedRTS函数maketestprog接受一个程序和一个测试，就像可能给out一样，并返回一个程序输入到cbig。函数collect start为每个程序返回一个集合，表示应该预先收集的有关该程序的信息。这表示RTS算法根据程序本身考虑的任何信息，并且out函数将自动包含这些信息。公理形式化了ou