利用QuickCheck生成随机类型良好的轻量级Java程序

可在www.sciencedirect.com在线获取理论计算机科学电子笔记342（2019）3-20www.elsevier.com/locate/entcs利用QuickCheck生成随机类型良好的轻量级Java程序塞缪尔·达席尔瓦·费托萨a，1罗德里戈·热拉尔多·里贝罗b，2安德烈·劳伯·杜波依斯a，3aProgramadeP´osGraduapuricpuricaoemComputapuricpuricao/PPGC佩尔松-RS，巴西bProgramadePosGraduapucpuaoemCipuchadaComputapucpuao/PPGCCUniversidade Federal de Ouro PretoOuro Preto - MG，巴西摘要目前，Java是最常用的编程语言之一，被许多大型项目采用，其中应用程序达到了手动测试和人工检查不足以保证软件开发质量的复杂程度。 即使在使用自动化单元测试时，此类测试也很少覆盖所有有趣的代码案例，这意味着一旦代码根据相同的规则集一遍又一遍地测试，就永远不会发现bug。本文讨论了在FeatherweightJava，一个著名的面向对象的演算，使用QuickCheck，一个基于属性的测试Haskell库的上下文中关键词：随机程序生成，基于属性的测试，轻量级Java。1介绍Java是当今最流行的编程语言之一[24]。它是一种通用的、并发的、强类型的、基于类的面向对象语言。自1995年由Sun Microsystems发布以来，Java一直在不断发展，在其新版本中添加了功能和编程工具。在Java最近的一个主要版本中，添加了诸如lambda表达式、方法引用和函数接口等新特性，1电子邮件：samuel. inf.ufpel.edu.br2电子邮件：rodrigo@decsi.ufop.br3电子邮件：dubois@inf.ufpel.edu.brhttps://doi.org/10.1016/j.entcs.2019.04.0021571-0661/© 2019作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。4S. da Silva Feitosa等/理论计算机科学电子笔记342（2019）3核心语言，创建一个融合了面向对象和函数式风格的编程模型[13]。考虑到Java语言在大型项目中的应用越来越多，许多应用程序已经达到了测试、代码复查和人工检查不再足以保证质量的复杂程度。这个问题增加了对采用静态分析技术的工具的需求，旨在探索应用程序中的所有可能性，以保证不存在意外行为[6]。通常，考虑到某些问题的大小，由于可计算性问题，这个任务很难完成。为了克服这种情况，有可能对问题的形式子集进行建模，应用一定程度的抽象，仅使用感兴趣的属性，促进对问题的理解，并允许使用自动工具[11]。因此，一个重要的研究领域涉及语言的形式语义和类型系统规范，这使得形式证明和建立程序属性成为可能。此外，解决方案可以通过机器检查，提供使用非正式方法无法达到的置信度。我们应该注意到，如果没有形式语义学，就不可能确定地陈述或证明任何关于语言的东西。例如，我们在这种情况下，这项工作提供了Java程序的测试生成器的规范，使用Featherweight Java [14]（FJ）的类型规则来生成良好类型的程序。FJ是Java的一个小的核心演算，其主要核心方面有严格的语义定义。使用FJ作为起点的动机是它是紧凑的，因此我们可以以一种可以扩展新功能的方式来建模我们的测试生成器，并且它的最小语法，类型规则和操作语义非常适合为编译器和程序建模和证明属性。据我们所知，目前还没有针对FJ的类型良好的测试生成器。这项工作的目的是填补这一空白，指定一个生成器的FJ程序使用QuickCheck， Haskell的一个基于属性的测试库。我们意识到使用自动化测试不足以确保正确性，但它可以在使用之前暴露错误。更正式的方法，如在证明助手中形式化语义。具体而言，我们作出以下贡献：• 我们在Haskell中实现了一个FJ的解释器4，它可以作为研究面向对象上下文中新功能• 我们提供了一个类型导向的启发式[20]来构造随机程序。我们猜想我们的规范对于FJ类型系统是合理的，即它只生成良好类型的程序。• 我们使用QuickCheck作为一个轻量级的方式来检查是否所有生成的程序都是良好的类型，并测试我们的解释器对类型的合理性证明，以验证所提出的方法。本文的其余部分组织如下：第2节总结了FJ。4我们的解释器和测试套件的源代码可以在www.example.com上https://github.com/sfeitosa/fj-qc。S. da Silva Feitosa等/理论计算机科学电子笔记342（2019）35第三节介绍了在FJ的背景下生成良好类型的随机程序的过程。第4节显示了使用QuickCheck测试FJ的类型安全属性的结果。第5节讨论相关工作。最后，我们在第6节中提出最后的评论。2轻量级爪哇Featherweight Java（FJ）[14]是Java的最小核心演算，在这个意义上，尽可能多的Java功能被省略，同时保持语言及其类型系统的基本特性。然而，这个片段足够大，可以包含许多有用的程序。 FJ中的程序由以下声明组成： 一组类和一个要计算的表达式，对应于JavaFJ之于Java就像λ-演算之于Haskell。它提供类似的操作，提供类、方法、属性、继承和动态转换，其语义接近JavaFeatherweight Java项目更倾向于简单性而不是表达性，并且只允许五种方法来创建术语：对象创建，方法调用，属性访问，铸造和变量[14]。下面的例子展示了如何在FJ中对类进行建模有三个类，A、B和Pair，具有构造函数和方法声明。classAextendsObject { A（）{super（）;}}classBextendsObject { B（）{super（）;}}类Pairextends Object{ Objectfst;对象snd;publicintfindDuplicate（intfindDuplicate）this.fst=fst;this.snd=snd;}对setfst（对象newfst）{返回新Pair（newfst，this.snd）;}}在下面的例子中，我们可以看到不同类型的术语：new A（），new B（）和new Pair（...） 是对象构造函数，而.setfst（...）是指方法调用。newPair（newA（），newB（））。setfst（newB （））;FJ语义提供了一个没有副作用的纯功能视图。换句话说，内存中的属性不受对象操作的影响[23]。此外，接口、重载、对基类方法的调用、空指针、基类、抽象方法、语句、访问控制和异常在该语言中不存在由于该语言不允许副作用，因此可以仅使用FJ语法来形式化评估，而不需要辅助机制来对堆进行建模[23]。接下来，我们介绍FJ的原始描述[14]。6S. da Silva Feitosa等/理论计算机科学电子笔记342（2019）32.1辅助和辅助功能FJ的抽象语法如图1所示，其中L表示类，K定义构造函数，M表示方法，e表示可能的表达式。元变量A、B、C、D和E可以用来表示类名，f和g表示字段名，m表示方法名，x和y表示变量，d和e表示表达式。在本文中，我们将C写为可能为空的序列C1，...，Cn（类似于f，x等）。 空序列用y·表示，序列<$x的长度用#<$x表示。 我们用Γ来表示一个环境，它是一个从变量到类型的有限映射，记为x：T，我们让Γ（x）表示类型C，使得x：C ∈ Γ。我们通过在序列上使用集合运算符来稍微滥用他们的意思和往常一样。语法L：：=class声明C类扩展{Cf;K M}K：：=构造函数声明C（Cf）{super（f）; this.f =f;}M：：=方法声明Cm（C x）{returne;}e：：=表达式x变量e.实地访问e. m（e）方法调用新C（e）对象创建(C) 电子铸件Fig. 1. FJ的语法定义一个类表CT是一个从类名到类声明L的映射，它应该满足一些条件，比如每个类C都应该在CT中，除了Object，它是一个特殊的类;并且在子类型关系中没有循环因此，程序是类表和表达式的对（CT，e图2显示了子类型化的规则，当C是D的子类型时，我们写C<：D。C<：CC<：D D<：EC<：ECT（C）= class C extends D{. 个文件夹C<：D图二.类之间的子类型关系作者还提出了一些辅助定义，用于类型化和归约规则。 这些定义见图3。字段查找的规则S. da Silva Feitosa等/理论计算机科学电子笔记342（2019）37演示如何获得给定类的场 如果类是Object，则返回一个空列表。否则，对于给定类及其所有超类中声明的所有字段，它返回一个序列C f，将每个字段的类型与其名称配对。 方法类型查找（mtype）的规则显示了如何获得类C中方法m的类型。mtype的第一条规则返回一对，写为B→B，由参数类型B和结果类型B组成，当方法m包含在C中时。否则，它返回使用超类调用mtype的结果。方法体查找规则中使用了类似的方法，其中mbody（m，C）返回一对（x，e），由一系列参数x和表达式e组成。mtype和mbody都是部分函数。字段查找字段（对象）=·CT（C）=C类扩展D{Cf;K M}场（D）=D g场（C）=D g，Cf方法类型查找CT（C）=C类扩展D{Cf;K M}Bm（B x）{returne;} ∈Mmtype（m，C）=B→BCT（C）=classsCextendsD{Cf;KM}m∈/Mmtype（m，C）=mtype（m，D）方法体查找CT（C）=C类扩展D{Cf;K M}Bm（B x）{returne;} ∈Mmbody（m，C）=（x，e）CT（C）=classsCextendsD{Cf;KM}m∈/Mmbody（m，C）=mbody（m，D）图三. 辅助定义。2.2打字和简化规则本节介绍如何使用FJ的打字规则来保证类型的可靠性，即，良好类型的术语不会被卡住，并且简化规则显示了如何为FJ语法处理每个求值步骤。图4在左侧显示了表达式的类型规则，在右侧，它首先显示了8S. da Silva Feitosa等/理论计算机科学电子笔记342（2019）3检查方法和类是否格式良好的规则，然后是该演算的归约规则。我们在这里省略了同余规则，这些规则可以在原始论文[14]中找到。表达式的类型判断具有形式Γe：C，意味着在环境Γ中，表达式e具有类型C。处理序列时的缩写与前一节类似类型规则是语法指导的，每一种表达形式都有一条规则，只是造型有三条规则。规则T-Var根据上下文Γ产生变量x的类型。 如果变量x不包含在Γ中，结果是unfined。 同样，结果是当目标类或方法在给定类中不存在时，调用函数fields、mtype和mbody时，将unfind。 规则T字段对子表达式e0应用类型判断，这将导致类型C0。然后它获得类C0的字段，匹配结果列表中f i的位置，以返回相应的类型Ci。 规则T-Invk也对子表达式e0应用类型判断，这导致类型C0，然后它使用mtype来获得形式参数ty pes<$D并返回ty peC。形式参数types是用于检查实际参数是否为m的任意类型，如果是，则返回类型为C。规则T-New检查实际参数是否构造函数形式参数的子类型，通过使用函数字段获得。强制转换有三个规则：一个是向上强制转换，其中主体是目标的子类;一个是向下强制转换，其中目标是主体的子类;另一个是愚蠢强制转换，其中目标与主体无关。即使考虑到Java方法类型规则检查方法声明M在类C中出现时是否格式良好。它在方法体上使用表达式类型判断，上下文Γ用来自实际参数的变量及其声明类型和特殊变量this的C类型进行扩充。类类型的规则检查类是否是良构的，通过检查构造函数是否将super应用于超类的字段并将该类中声明的字段替换，以及类中的每个方法声明是否是良构的。只有三个计算规则，指示哪些表达式可以在主程序中使用。第一个规则R-Field正式定义了如何评估属性访问。与类型规则T-Field类似，它使用函数fields，并匹配结果列表中字段fi的位置i，返回值vi，它引用实际参数列表中位置i第二个规则R-Invk展示了方法调用的求值过程，首先它通过函数mbody获得C类的方法体表达式m，然后在体表达式中执行实际参数和特殊变量this的替换，类似于λ-演算的beta归约。最后一个规则R-Cast指的是cast预处理，如果主题类C是目标类D的子类型，则返回相同的子表达式newC（e）。有S. da Silva Feitosa等/理论计算机科学电子笔记342（2019）39►►►−→表达式分型Γx：Γ（x）[T-Var]¯ ¯Γe0：C0场（C0）= C fΓ e0.fi：Cimtype（m，C0）=D<$→C【T型力场】<$e0：C0<$$>e：C<$Γe0.m（<$e）：C场s（C）=D<$fC：D：【T-Invk】e：C<$C<$：D<$【T-新】新的C（E）：CTu0：D D <：CΓΓ（C）e0：C[T-UCast]方法分型e0：D C：D C = DΓ（C）e0：CΓ e0：DC：D D： C愚蠢的警告Γπ（C）e0：C[T-DCast][T-SCast]x<$：C<$，this：Ce0：E0 E0<：C0class C extends D{.}若m∈（m，D）=D<$→D0，则nC<$=D<$anddC0=D0C0m（C<$x<$）{returne0;}在C中OK类类型K=C（D<$g，C<$f）{super（<$g）;this.{f=f;}场s（D）=D<$gM<$OKinCclassCextendsD{C<$f;KM<$评价场s（C）=C<$f好的（新的C（v））。fivimbody（m，C）=（x<$，e0）[R场]（newC（v<$））.m（d<$）−→[d<$$> →x<$，newC（v<$）<$→this]e0[R-Invk]C：D(D) (newC（v<$））−→新的C（v<$）[R-Cast]见图4。 分类和评价规则。还有五个全等规则5（图4中省略），它们负责所提出的小步语义的中间评估步骤FJ演算的目的是成为一个起点，为各种业务功能的研究面向对象的编程在Java类语言，是紧凑的，足以使严格的证明可行。除了评估规则之外10S. da Silva Feitosa等/理论计算机科学电子笔记342（2019）3[5]文中省略的同余规则见[14]第407页。S. da Silva Feitosa等/理论计算机科学电子笔记342（2019）311和类型检查规则，作者提出了FJ的类型可靠性证明作为另一个重要贡献，这将在接下来的部分中由我们的测试套件进行探索。3程序生成为编程语言创建测试的任务非常耗时。首先，因为它应该尊重编程语言的要求，以便产生一个有效的测试用例。第二，如果测试用例是由一个人创建的，那么它会受到人类想象力的限制，其中可能会忽略一些模糊的角落案例。如果编译器编写者正在生成测试用例，他们可能会有偏见，因为他们可以对他们的实现或语言应该做什么做出假设。此外，当语言发展时，以前的测试用例可能是一个问题，考虑到如果语言语义改变，一些旧测试的有效性可能会改变[1]。考虑到所提出的问题，有一个不断增长的研究领域探索随机测试生成。然而，生成好的测试程序并不是一件容易的事情，因为这些程序应该具有编译器接受的结构，尊重一些约束，这可以像具有正确语法的程序一样简单，也可以更复杂，例如静态类型编程语言中的类型正确程序[22]。为了在FJ的上下文中生成随机程序，生成步骤具有两个不同的阶段。首先，需要随机生成类来组成类表。其次，应该使用类表生成表达式。因此，本节描述了通过使用QuickCheck库[4]来生成良好类型的术语和格式良好的类的建议的类型导向过程。QuickCheck是Haskell的自动化测试工具。它定义了一种正式的规范语言，允许使用它来指定测试中的代码，并检查某些属性是否在大量随机生成的测试用例中保持。这个库为Haskell语言的构造函数提供了几个测试用例生成器，但它留给用户定义用户定义类型的生成器的定义。该库提供了组合子，帮助程序员在这个过程中。本文推广了文[22]中的方法，考虑到FJ具有一个名义型系统而不是结构型系统，从而产生随机程序。通过这种方式，每个类型规则都被解释为一个生成规则，用于表达式生成和类表生成。它们中的每一个的生成过程解释如下。3.1式生成我们首先采用面向目标的过程定义生成FJ表达式的过程，该过程接收任意类表、环境和所生成表达式的期望类型作为输入这个所需的类型应该表示类表中包含的类名。表达式生成器的目的是生成所需类型的良好类型的术语，该术语可以包含12S. da Silva Feitosa等/理论计算机科学电子笔记342（2019）3从给定环境释放变量。为了生成给定类型的表达式，只能使用类型规则的子集。例如，规则T-Var只能在生成方法体表达式时使用，因为方法的形式参数表示环境中的自由变量，规则T-Field只能在类表中的某个类具有所需类型的属性时使用，等等。所采用的表达式生成方法是通过倒读图4中的表达式类型规则获得的，即：为了生成一个表达式，它是一个规则的结果，首先需要生成在其前提中的表达式，然后将它们组合起来。这样，生成术语的目标可能涉及递归地生成子目标。通过使用类型化规则，我们可以确保生成的术语是类型良好的。假设一个类表包含第2节中所示的三个类A、B和Pair，一个空的环境Γ，我们想生成一个Object类型的表达式。 键入规则可以使用问号进行格式化？ 作为该表达式的占位符，表示第一个生成步骤，如下所示：你呢？ ：对象（1）通过查看类表，通过规则T-Field，我们可以生成Object类型的表达式，访问类Pair的属性fst或snd，T-New6可以用于创建Object的新实例，规则T-UCast7可以在类表上强制转换任何类，因为Object是所有类的超类。让我们看看第一个，键入规则T-Field显示了生成术语的另一个步骤，如下所示。你呢？1：配对fields（Pair）={ Object fst，Object snd}I 'm sorry. 1）.fst：Object【T型力场】（2）问号？1表示将作为子目标生成的子表达式。在这个意义上，我们可以注意到访问字段fst的子表达式？1，它应该具有类型Pair，正如其前提所述为了生成子目标的表达式，我们必须再次查看类表以生成Pair类型的项。有两种方法可以做到这一点，通过实例化类Pair或调用方法.setfst（...）. 让6Object类被认为是一个独特的类名，其定义没有出现在类表中。7在表达式生成中不使用规则T-DCast和T-SCast，S. da Silva Feitosa等/理论计算机科学电子笔记342（2019）313如下所示场s（Pair）=D<$f你呢？2：C¯C：D：【T-新】新的Pair（？2）：配对场（对）={对象fst，对象snd}[T场]r（new Pair（？2））.fst：Object（三）可以注意到，生成器递归地应用于每个占位符。我们表示？2作为占位符序列，类似于前面的部分处理类型或变量序列时占位符？2表示为类Pair构造函数传递的实际参数，其中每个子表达式应根据函数字段返回的类型生成。使用规则T-Invk生成表达式的过程是类似的，在这个意义上，它应该生成一个表示对象实例化的子表达式，它包含给定的方法，并应该生成实际的参数，其中每个参数都应该具有根据mtype的预期类型。所讨论的生成规则能够生成FJ中的每一个良好类型的表达式，因为如果表达式存在类型派生，则该表达式是良好类型我们定义了一个算法，通过使用QuickCheck库应用生成规则递归地生成表达式。为了防止非终止生成，算法的每次递归调用都使用一个大小参数，该参数在后续调用中会减小。当size为零时，只能使用T-Var和T-New规则，这避免了过度的递归。生成表达式的算法首先为每个类型规则创建一个候选表达式列表。一个类型规则的候选列表可以是空的，这表明不可能为该规则生成所需类型的表达式，因此它被忽略。在生成所有候选列表之后，算法使用QuickCheck函数之一来为每个列表随机选择一个候选。在选择的候选项上，我们再次应用函数oneof，得到一个候选表达式，它将被我们的递归生成规则使用。我们选择这种方法是为了保证每个非空类型规则的平均分布。3.2类表生成生成类表的过程更加详细，因为首先我们没有任何信息可以开始。我们所拥有的只是类表应该满足的一组条件，例如：（1）CT（C）= class C. 对于每个C∈dom（CT）;（2）Object∈/dom（CT）;（3）对于每个类名C（Object除外）（4）CT诱导的亚型关系中不存在圈，即C∈dom（CT）。关系：是反对称的。我们首先定义三个生成器，一个用于类名，一个用于变量名，另一个用于类型。我们的类名生成器只是随机选择一个字母，它可以很容易地适应生成不同的名称。14S. da Silva Feitosa等/理论计算机科学电子笔记342（2019）3长度这个过程类似于变量名，除了它是由一个大写字母生成的。类型的生成器随机选择一个存在于类表或Object中的类名。之后，我们继续生成类表，使用非重复类名列表。对于该列表中的每个元素，我们的生成器生成一个类并将其插入类表中。生成类的第一步，在我们有了它的名字之后，是定义它的基类。这里使用类型生成器如果类表为空，类型生成器返回Object，否则，它返回一个已经生成的类。这个简单的过程确保类层次结构中没有循环假设在第一步中生成了一个类名Z和一个基类Object然后，类类型规则用于接下来的步骤，如下所示：K = C（？一个？2）{super（）; this. ？2 =？2;}场s（Object）=·M<$OKinCclassZextendsO object{？一个？2;KM<$[C OK]（4）}填充类组件的过程分为两个部分。第一个是上面演示了，其中随机生成属性列表。最初，生成器选择一个随机数n来定义类应该有多少个字段。 然后为占位符生成一个大小为n的类型列表？1和为占位符生成大小为n的非重复变量名列表？二、正如我们在生成规则中所注意到的，函数fields是用基类Object调用的，返回一个空序列。然后，相应地格式化构造函数。所描述的过程已经生成了一个极简类，考虑到它有一个类名、一个基类、它的属性和一个构造函数。在进行类生成的第二部分之前，生成器算法将这个最小类添加到类表中。这是允许方法体表达式通过特殊变量this使用类属性所必需的。 然后我们moveetomethodgeneration，whi cpearsin thegenerationruleasMOKinC. As如前几节所述，使用f<$M表示可能使用的方法列表。第二部分总结了类生成与方法生成的关系进程开始生成一个随机数n，它表示将为给定的类C生成n个方法。方法由其签名和其主体表示为了生成签名，需要生成方法名、返回类型和形参（类型和名称）。此步骤根据方法类型规则执行，如下所示：？4：？3，this：C e0：E 0E 0<：？1class C extends D{...}ifmty pe（？2，D）=D<$→D0，那么ten？3=Dnd？1=D0？一个？2（？三个？4）{return e0;}（五）在这一步中，它是随机产生一个返回类型来分配在占位符？1，已经在类表中定义了，并且用一个大写字母来组成方法名？二、由于FJ不允许方法重载，为了避免类层次结构中具有相同名称的方法，生成器将类名附加在S. da Silva Feitosa等/理论计算机科学电子笔记342（2019）315- -►方法名的结尾。然后，生成一个随机大小的形式参数列表。类型列表放在？3、不重复的名单是放在哪的？四、当我们为每个类生成独占方法名时，函数mtype（？2、D总是不确定的。这意味着生成的方法没有重写基类中的方法方法生成的最后一步是生成方法体表达式。例如，假设我们正在为类Z生成方法，它有一个Object作为基类，并且在类表中只定义了最小类Z在上述过程中产生的可能签名如下：a：对象，b：对象，this：Z？：E0 E0<： Zclass Z extends Object.mtype（mZ，Object）=unfined（Object a，Object b）{return？;}中的内容。（六）那么，占位符呢？应该用一个随机生成的表达式填充，这个过程在上一节中解释这里重要的区别是上下文被形式参数的变量和类型以及特殊变量this所扩充，其类型是正在生成的类。结果表达式应该是生成的返回类型的子类型当前的设计展示了一个生成格式良好的类表和类型良好的表达式的过程，它代表了Java程序的主要方法下一节将展示我们如何使用生成的程序来测试一些类型可靠性属性。由于FJ代码代表一个有效的Java程序，因此随机生成的源代码可以用于对原始语言进行测试4语义属性在介绍了FJ语言语义和随机测试是如何生成的之后，我们演示了QuickCheck[4]如何帮助使用随机生成的程序测试语义的某些属性，包括FJ原始论文中提出的类型可靠性。考虑到测试需要额外的编程，测试代码本身包含错误的风险是自然的[21]。为了减少我们实现中的错误风险，我们已经通过使用我们的解释器和测试生成器使用QuickCheck对其进行了测试。我们检查以下内容：• 我们的定制生成器只生成格式良好的类表。• 我们的自定义生成器根据随机生成的类表只生成类型良好的表达式。• 如果所有生成的表达式都是强制转换安全的。QuickCheck库提供了一种将属性定义为Haskell函数的方法。因此，测试这个属性涉及到当所有输入的数量是无限时，在有限数量的输入这样，测试只能重新-16S. da Silva Feitosa等/理论计算机科学电子笔记342（2019）3通过找到反例或不确定其有效性来反驳该属性。如果找到反例，可以使用它来帮助修复bug。考虑到这一点，我们开始定义一个函数来检查生成的类表是否格式良好，如以下代码所prop_genwellformedct：：Boolprop_genwellformedct =对于所有（genClassTable）$\ct->数据。名单所有（I（c，cl）->classTypingclData.MAP。 （Data.MAP。（tct）上面的代码使用了QuickCheck函数forAll，它模仿了通用的quantifier函数，生成用户定义数量的类表实例，并通过运行函数classTyping来测试给定类表中所有生成的类是否格式良好。我们还定义了一个函数来测试生成的表达式是否是良好类型的，如下面的代码所示。 这个函数首先生成一个类表ct的实例。之后，它随机选择类表中的类型t。然后，它使用产生的ct和空的环境来生成表达式类型T。最后，通过使用函数typeof，它检查表达式是否具有类型t。prop_genwelltypedexpr：：布尔prop_genwelltypedexpr =对于所有（genClassTable）$\ct-> forAll（genTypeCT）$\t->forAll（genExpressionctData.MAP。emptyt）$\e ->either（const False）（\（T类型类st==t'）（typeo f Dat a.MAP。（ycte）作为对生成器的最后一次检查，下面的函数测试生成的表达式是否是强制转换安全的，即，主题表达式是目标类型的子类型。prop_gencastsafeexpr：：Boolprop_gencastsafeexpr=forAll（genClassTable）$\ct-> forAll（genTypeCT）$\t->forAll（genExpressionctData.MAP。空yt）$\e->情况辰（Castce）->case（typeofData.MAP。电子邮件 （e）右t（T类型类st_->错误_->True由于这些检查，我们发现并修复了生成器和解释器实现中的一些编程错误。虽然测试我们已经使用我们的测试套件作为一个轻量级的方式来检查的属性，erties的保存和进展中提出的FJ文件。非正式（非机械化）证明也被建模为Haskell函数，用于QuickCheck。定理2.4.1（[14]的第406页）给出了保持（主语归约），指出<我们的函数建模如下：S. da Silva Feitosa等/理论计算机科学电子笔记342（2019）317prop_preservation：：Boolprop_preservation=for All（genClassTable）$\ct-> forAll（genTypeCT）$\t->forAll（genExpressionctData.MAP。空yt）$\e->either（const False）（\（TypeClasst子类型tct）（case（eval只是etypeofData.MAP。emptycte_->throwError（不详））正如我们在代码中看到的，在生成ct的实例、类型t和类型t的表达式e之后，函数eval然后，使用函数typeof来获得e'的类型最后，使用子类型化函数来检查表达式在缩减步骤之后是否保持类型关系。类似地，我们建模（如下）一个函数的进展性质（定理2.4.2，p。407[14]），它指出一个良好类型的表达式不会卡住。prop_progress：：Boolprop_progress =对于所有（genClassTable）$\ct-> forAll（genTypeCT）$\t->forAll（genExpressionctData.MAP。emptyt）$\e -> isValuecte||也许（False）（const True）（eval'（ct e）此函数还生成类表、类型和该类型的表达式。然后它检查表达式是否为值，或者它可以通过函数eval我们对所提供的函数进行了数千次成功的测试。作为一种衡量测试质量的方法，我们检查我们的测试套件覆盖了多少代码库。这些统计数据由Haskell Program Coverage（HPC）工具提供[12]。每个模块（分别是求值器、类型检查器、辅助函数和total）的代码覆盖率结果如图5所示。图五. 测试覆盖率结果。图6展示了HPC的另一个结果，显示了我们的计算器的一段代码，突出显示了不可访问的代码。在这里我们可以注意到，要达到突出显示的代码，需要：（1）在类c的字段中找不到字段f;（2）子表达式e的错误处理函数eval这两种情况都表示卡住状态，只能执行如果我们有一个类型不好的表达式。正如类型可靠性证明[14]所述，一个类型良好的表达式不会卡住。类似地，图7显示了类型检查器的一段代码，突出显示了不可访问的代码。我们注意到，突出显示的代码只有在以下情况下才会执行：（1）我们有一个18S. da Silva Feitosa等/理论计算机科学电子笔记342（2019）3图第六章求值时无法访问代码图第七章类型检查器上无法访问的代码类型上下文中的未定义变量;（2）代码使用了当前表达式类中不存在的字段;（3）无法获得子表达式e在任何情况下，我们都有一个类型不好的程序。最后，图8显示了我们的辅助函数的一段代码，其中突出显示的代码可以在两种情况下到达：（1）类c不存在于类表中;（2）在基类上执行字段只有当我们有一个类型不好的程序时，才会发生图八、辅助函数上的不可达代码虽然没有100%的代码覆盖率，我们的测试套件能够验证FJ论文中存在的主要安全属性，通过随机生成的程序的大小增加。通过分析测试覆盖率结果，我们可以观察到测试用例未到达的代码由程序语义上的卡住状态或类型不好的表达式的错误控制5相关工作基于属性的测试是一种通过自动生成测试数据来验证代码是否符合可执行规范的技术，通常是随机和/或S. da Silva Feitosa等/理论计算机科学电子笔记342（2019）319彻底的方式[2]。然而，为测试编译器生成随机测试数据本身就是一个挑战，因为很难为编译器提供有效的测试数据生成器，并且很难提供一个规范来决定编译器的正确行为[22]。因此，近年来，在编译器和编程语言工具中发现bug的随机测试受到了一些关注测试工具Csmith[25]是C语言的程序生成器，支持大量的语言功能，用于发现编译器中的一些bug，如GCC，LLVM等。Le等人[18]开发了一种方法，用于C编译器的分布式测试。Lindig [19]创建了一个测试GCC编译器的C函数调用约定的工具，该工具随机生成函数类型。也有其他语言的随机生成的案例测试[8]。这些项目与我们的项目之间的主要区别在于，我们的生成器是通过使用类型规则的正式规范创建的。此外，我们使用基于属性的测试来检查类型可靠性证明。更具体地说，Daniel等人[5]生成随机Java程序来测试Eclipse和NetBeans中的重构引擎Klein等人[15]生成随机程序来测试面向对象的库。Allwood和Eisenbach [1]还使用FJ作为基础来定义主流编程语言的测试套件，测试他们的方法能够获得多大的覆盖率。这些项目与我们的项目密切相关，因为它们在面向对象的上下文中生成代码。我们方法的不同之处在于，我们通过在生成过程中使用类型规则的形式化规范来生成随机完整的类和表达式，这些类和表达式都是良构的和良类型的。另一个不同之处是，他们都没有在他们的方法中使用基于属性的测试Palka、Claessen和Hughes[22]的工作使用QuickCheck库生成λ-terms来测试GHC编译器。我们的项目采用了他们生成术语的方法，在这个意义上，我们也使用了QuickCheck和类型规则来生成类型良好的术语。与他们的方法不同，通过读取生成的类表，我们生成了一个候选表达式列表，这消除了回溯的需要。此外，QuickCheck的使用帮助我们完善了语义和实现，并允许测试类型安全属性。也有一个从类型系统的定义自动随机测试生成的分类。Fetscher等人的工作。[10]提出了一种通用方法，用于在PLT Redex [9]的上下文中随机生成良好类型的表达式。Lampropoulos等人的作品[16，17]提出了不同的方法来自动生成随机表达式使用QuickChick[7]，现有的工具，基于属性的测试在Coq。这些方法与我们的方法不同，因为作者提供了根据正式规范自动生成术语的工具，通常通过注释类型规则，而在我们的工作中，我们专注于高级编程语言的特定20S. da Silva Feitosa等/理论计算机科学电子笔记342（2019）36结论在本文中，我们提出了一种在Featherweight Java环境下构造随机程序的类型导向启发式方法，并使用基于属性的测试来验证它。QuickCheck提供的轻量级方法允许对不同的语义设计和实现进行实验，并快速检查任何更改。在这项工作的发展过程中，我们已经改变了我们的实现多次，无论是作为纠正错误和精简演示的结果。确保我们的更改是一致的，这仅仅是重新运行测试套件的问题。将类型可靠性属性编码为Haskell函数提供了一个干净简洁的实现，不仅有助于修复bug，还有助于提高对所呈现语义属性含义的作为未来的工作，我们打算使用Coq提供正式认证的证据，证明FJ语义确实具有安全属性，并探索我们的测试套件中使用的方法，用于FJ的其他扩展，除了使用其他工具，如QuickChick具有相同的目的。确认这项工作得到了巴西CAPES的部分支持。工艺编号：88882.151433/2017-01。引用[1] 特里斯坦岛R.奥尔伍德和苏珊·艾森巴赫。用羽毛挠爪哇痒痒。电子笔记理论Comput. Sci. ，238（5）：3[2] 罗伯托·布兰科，戴尔·米勒，阿尔贝托·莫米利亚诺。通过正在进行的证明重建工作进行基于属性的测试。