在JVM上实现具有流敏感和结构类型的Whiley语言

可在www.sciencedirect.com在线获取理论计算机科学电子笔记279（1）（2011）47-59www.elsevier.com/locate/entcs在JVM上实现具有流敏感和结构类型詹姆斯·诺布尔2新西兰惠灵顿维多利亚大学工程与计算机科学学院摘要动态类型语言是灵活的，对程序员来说负担很少。相比之下，静态类型导致软件更高效，错误更少。然而，静态类型系统传统上要求每个变量都有一个类型，并且类型之间的关系（例如子类）要显式声明。Whiley语言的目标是在动态类型和静态类型之间找到一个最佳点。这是通过结构子类型化和以对数据流敏感的方式对变量进行类型化来实现的。 Whiley编译到JVM，这带来了一些挑战。 本文讨论了Whiley类型系统在JVM上的实现关键词：流敏感，结构子类型，Java，JVM1引言静态类型的编程语言（例如Java、C#、C++等）导致程序更高效，错误更少[11，2]。静态类型在编程过程中强加了一些规则。例如，它确保至少提供一些关于可接受的功能输入的文档。相比之下，动态类型化的语言更灵活，这有助于减少管理费用并提高生产力[37，47，34，7]。此外，近年来，动态类型语言已经有了很大的转变[38]。为了弥合静态语言和动态语言之间的鸿沟，人们做了许多尝试。Scala [45]，C#3.0 [6]，OCaml [43]以及最近的Java 7都采用了局部类型推断（以某种形式）来减少语法开销。诸如渐进类型[46，50]、软类型[11]和混合类型[20]之类的技术使程序的某些部分处于静态类型的过渡位置，而其他部分则是静态类型。1电子邮件：djp@ecs.vuw.ac.nz2电子邮件：kjx@ecs.vuw.ac.nz1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.11.00548D.J. Pearce，J.Noble/Electronic Notes in Theoretical Computer Science 279（1）（2011）没有或者，类型推断可以用于（在某些情况下）为动态语言编写的程序“事后”重建类型Whiley是一种静态类型的语言，在大多数情况下，它具有动态语言的外观和感觉。这是通过一个非常灵活的系统来实现的，该系统利用了以下特征：• 流敏感类型，从流敏感程序分析（例如[22，30，14]）中采用，并允许变量在不同点具有不同类型。• 结构子类型，其中数据类型之间的子类型是隐式的，并且基于它们的结构。总的来说，与传统的名义类型相比，这些方法有很多优点，在传统的名义类型中，类型被命名，子类型关系被显式声明。1.1贡献本文的贡献是：(i) 我们讨论了在Whiley语言中使用的对流水线敏感的结构化类型系统。(ii) 我们详细介绍了这些功能在JVM上的实现，并确定了一些挑战。Whiley语言的开源实现可以从www.example.com免费获得http://whiley.org。最后，Whiley类型系统的详细形式化2Whiley在这一节中，我们提出了一系列的例子，显示惠利的主要特点。在下面的部分中，我们2.1隐式声明大多数当代静态类型语言都要求显式地定义变量（FORTRAN是一个例外）。与动态类型语言相比，这对程序员来说是一个额外的负担，特别是当变量的类型可以从赋值表达式中推断出来时。在Whiley中，局部变量通过赋值声明：int maximum（[int]）项目）：v = 0对于i项：v = v + items[i]return v/|项目|在这里，items是一个int的列表，而|项目|返回其长度。可变v用于累加列表中所有元素的和变量v声明D.J. Pearce，J.Noble/Electronic Notes in Theoretical Computer Science 279（1）（2011）49因为this的类型是int，所以v在赋值后的类型是int2.2联合类型可空引用在Java等语言中被证明是一个重要的错误来源[29]。问题是，在这样的语言中，可以将可空引用视为非空引用[40]。已经提出了许多解决方案，使用静态类型系统严格区分这两种形式[18，17，41，35]。Whiley这些允许变量保存不同类型的值，而不仅仅是一种类型。下面的例子说明：null| public int findDuplicate（String s，String s）：...[string] split（stringstr， charc）：idx= indexOf（str，c）如果idx =int：//匹配一个在下面的出现=str[0... idx] above=str[idx..] return[below，above]否则：return [str]//没有出现这里，indexOf（）返回字符串中字符的第一个索引，如果没有则返回null类型null| int是一个union类型，这意味着它要么是int， 要么是null。在上面的例子中，Whiley这是因为类型null| int不能被当作int。相反，我们必须首先执行运行时类型测试，以确保它是一个int。W h i l e y 在已知为真时自动将idx重新输入为int，从而避免任何笨拙和不必要的语法（例如，[4，35]中所要求的铸件2.3流量敏感型下面的代码显示了Whiley中的一个简单层次结构的定义，以及一个返回这三种类型的面积的函数将圆定义为{int x，int y，int radius}将正方形定义为{int x，int y，int dimension}将矩形定义为{int x，int y，int width，int height将形状定义为圆形|平方|矩形实面积（形状）：50D.J. Pearce，J.Noble/Electronic Notes in Theoretical Computer Science 279（1）（2011）ifs=Circle：return PI* s.radius* s.radiuselseif s= Square：return s.dimension * s.dimensionelse：return s.width * s.height形状是一个联合类型-圆形，方形或矩形（它们本身都是记录类型）。代码使用运行时类型测试“s = Circle“来区分不同种类的Shape。这类似于Java的instanceof或Ei el的反向赋值。与Java不同，Whiley在if语句的true分支上将s重新类型化为Circle类型，因此在访问Circle特定的字段半径之前不需要显式地将s转换为Circle。类似地，在假分支上，Whiley将s重新键入为联合类型Square|矩形，然后在下一个if中设置为Square或Rectangle。在大多数静态类型语言中实现这些XML将更加麻烦和冗长。在现代面向对象语言中，如Java，表达式仍然必须显式地重新类型化。 例如，在一个测试之后，比如s instanceof Circle，我们必须引入一个新的变量，比如c，类型为Circle作为s的别名，当我们想访问作为一个圆的s时，就使用c2.4结构亚型静态类型语言，如Java，对递归数据类型采用名义类型这导致了僵化的等级制度，往往难以扩展。相反，Whiley使用记录的结构子类型[10]来提供更大的可扩展性。例如，下面的代码定义了一个Border记录：将Border定义为{int x，int y，int width，int height}Border的任何实例都具有与Rectangle的实例相同的结构。因此，只要需要边界，就可以提供矩形，反之亦然-即使边界定义是在矩形之后很久才写的，即使矩形没有提到边界。Whiley中对结构类型而不是名义类型的关注在创建实例的方式中也很明显：bool contains（int x，int y，Border b）：返回b.x = xx（b.x + b.width）&&b.y= y y（b.y +b.高度）int x，int y，int n，int nrect= {x：1，y：2，width：10，height：3}return contains（x，y，rect）在这里，函数example（）创建一个记录实例，字段x，y，width和高度，并为每个值分配一个初始值。尽管没有名字，D.J. Pearce，J.Noble/Electronic Notes in Theoretical Computer Science 279（1）（2011）51例如Border或Rectangle，它可以自由地传递到期望此类类型的函数中，因为它们具有相同的结构。2.5值语义在Whiley中，所有的复合结构（例如列表、集合和记录）都有值语义。这意味着它们是按值传递和返回的（就像在Pascal或大多数函数式语言中一样）-但与函数式语言（和Pascal一样）不同的是，复合类型的值可以就地更新。值语义意味着对变量值的更新只能是对该变量的更新，而信息从过程中流出的唯一方式是通过该过程的返回值。此外，Whiley没有与面向对象语言中的堆相比的通用可变堆。考虑以下情况：int f（[int]xs）：ys =xsys[0]= 1...Whiley的语义规定，如上所述将xs分配给ys后，对ys的子更新不会删除xs。参数也是通过值传递的，因此xs在f（）内部更新，这不会影响f也就是说，更改只能通过显式返回值从函数中传递出来。Whiley还提供了关于基本类型的子类型的强保证（即，整数和实数）。在Whiley中，ints和reals表示无界整数和有理数，这确保了int≤real具有真子集语义（即每个int都可以用实数表示）。这对于例如Java是不正确的，其中有int（resp. long）不能用float表示的值（分别是双）[26，§5.1.2]。2.6渐进式构造当一个结构被逐段构建时，静态类型语言中出现了一个常见的模式。通常，这些片段存储在局部变量中，直到所有片段都可用，并且最终可以创建结构。在动态语言中，更常见的是在创建结构时将片段分配给结构，因此，在任何给定点，结构的部分完整版本都是可用的。这减少了语法开销，也为代码重用提供了机会例如，可以将部分结构传递给可以对可用内容进行操作的函数。在像Java这样的语言中，这样做需要创建一个单独的（中间）对象。在Whiley，结构也可以被逐段构建。 举例来说BinOpparseBinaryExpression（）：v = {}//空记录v.lhs = parseExpression（）v.op = parseOperator（）v.rhs =parseExpression（）52D.J. Pearce，J.Noble/Electronic Notes in Theoretical Computer Science 279（1）（2011）返回v在第一次赋值之后，v是一个空记录。然后，在第二个之后，它具有类型{Exprlhs}，在第三个之后，它具有类型{Exprlhs，Op op}，在第四个之后，它具有类型{Exprlhs，Expr rhs，Opop}。这也说明了Whiley2.7结构更新静态类型系统通常需要更新复合类型，如列表和记录，以尊重元素或字段类型。Whiley的值语义还允许对结构进行灵活的更新，而不会出现通常在面向对象语言中出现的别名问题。例如，在Java中不允许将浮点数赋给int数组的元素。为了解决这个问题，程序员通常要么克隆有问题的结构，要么使用类型转换（或类似方法）来解决类型在Whiley，总是允许更新列表和记录。 举例来说定义点为{int x，int y}定义实点为{real x，real y}public int maximum（int p，int w，int h）：p.x=p.x/ wp.y= p.y/h返回p这里，在p.x被赋值之后，p的类型被更新为{real x，inty}，并且{real x，realy}在p.y被赋值之后。类似地，对于列表，我们可以这样写：[real]normalise（[int] items，intmax）：for i in 0..|项目|：items[i]= items[i]/最大返回项这里，通过赋值将项目的类型更新为[real]。因此，Whiley利用原始类型，例如Java中的List3在JVMWhiley语言编译为Java字节码，并在JVM上运行。在本节中，我们将概述Whiley的数据类型如何D.J. Pearce，J.Noble/Electronic Notes in Theoretical Computer Science 279（1）（2011）533.1NumericsWhiley以类似于Clojure的方式在JVM上表示数字[28]。更具体地说，ints和reals是使用自定义的Biglets和BigRational类来表示的，这些类会自动调整大小以防止过流。Whiley要求整数真正被当作实数的子类型。举例来说real f（intx）：ifx >=10：x = 9.99return x在if语句之后的control-parallel连接中，x持有int或real。由于实值在JVM上被实现为BigRationals，我们必须从false分支上的BigRational中强制x3.2记录Whiley记录类型的实现必须支持结构子类型。一个简单的方法（在许多动态语言中使用）是将它们转换为HashMap，将字段名映射到值。这确保了记录对象可以自由地传递，只要它们具有所需的字段。这种方法的一个问题是，每个字段访问都需要一个HashMap查找，虽然相对较快，但与Java（字段访问是恒定时间）相比并不好Whiley的语义支持更高效的实现。特别地，类型{intx}是一个只包含一个字段x的记录。因此，记录可以有一个静态的布局，以提供恒定的时间访问[40]。例如，可以使用引用数组而不是HashMap在JVM上实现记录。在这种方法中，每个字段对应于数组中的一个槽，其索引由字段的字典顺序使用静态布局实现记录需要编译器插入强制以支持子类型。考虑以下情况：将R1定义为{int x，inty}将R2定义为{int y}R1r1 ={x：10，y：20}R2r2 =r1让我们假设我们的记录是使用静态布局实现的，其中字段按顺序排列。因此，在R1中，场x占据第一个槽，场y占据第二个槽。类似地，场y对应于R2的第一个槽，因此R1与R2不兼容。相反，我们必须通过构造一个由单个字段组成的新数组，并使用第二个slot（即字段y）填充该数组，将R1的实例转换为R2的实例。这种转换是安全的，因为Whiley54D.J. Pearce，J.Noble/Electronic Notes in Theoretical Computer Science 279（1）（2011）3.3收藏Whiley 提 供 了 第 一 类 列 表 、 集 合 和 映 射 ， 它 们 在 JVM 上 分 别 被 转 换 为ArrayList、HashSet和HashMap当然，所有这些集合类型在Whiley中都必须具有值语义回想一下，在下文中，更新ys不会更新xs：int f（[int]xs）：ys =xsys[0]= 1...将这段代码简单地转换到JVM中，将克隆（）xs引用的ArrayList，并将其分配给ys。这可能会导致大量不必要的数据复制，有几种简单的策略可以降低此成本：(i) 使用CopyOnWriteArrayList确保仅在实际需要时才进行数据的完整副本。(ii) 使用术中数据流分析确定何时不再使用变量。例如，在上面的例子中，如果xs在赋值给ys之后不是活的，那么克隆它是不必要的。(iii) 利用编译器推断的函数参数的只读修改器。这样的修改器可以嵌入到JVM字节码中，并用于在调用的参数不需要克隆时识别位置。目前，我们只使用CopyOnWriteArrayList来提高性能，尽管我们想进一步研究这些其他方法的好处3.4产品型号测试在JVM上实现运行时类型测试是一个挑战。虽然许多运行时类型测试使用适当的instanceof测试直接转换，但情况并非总是如此：int f（realx）：ifx =int：return xreturn 0虽 然 Whiley ints 被 实 现 为 Java BigDatas ， 但 是 这 个 测 试 不 能 被 转 换 为 “einstanceof BigData“ 。 这 是 因 为 Whiley 因 此 ， 测 试 被 转 换 为 检 查 给 定 的BigRational实例是否对应于整数。联合类型也带来了挑战，因为区分不同的情况并不总是简单的。举例来说D.J. Pearce，J.Noble/Electronic Notes in Theoretical Computer Science 279（1）（2011）55将数据定义为[实数]|[[int]]int f（datad）：if [[int]]：return |0[0]|返回|D|由于变量d被保证是一个被查找的列表，它在条目上的类型被转换为JVM上的List。因此，Whiley不能在d直接区分这两种情况。相反，我们必须检查列表的第一个元素并测试它。因此，如果列表的第一个元素本身就是一个列表，那么真正的分支是3。下面的例子提出了另一个有趣的挑战：int f（[real]d）：ifd =[int]：return d[0]return 0要转换这个测试，我们必须遍历列表中的每个元素，并检查它是否是整数。此外，如果是这种情况，我们必须将列表转换为BigRational 列表，而不是BigRational列表。最后，记录提出了一个有趣的问题。请考虑以下示例：定义Rt为{int x，int y}|{int x，int z}intfindDuplicate（r）：如果r={int x，inty}：返回r.y返回R.Z由于变量r被保证是某种类型的记录，它在条目上的类型被翻译为Object[]。因此，使用instanceof实现类型测试是没有意义的，因为这不会区分两种不同类型的记录。相反，我们必须检查r是否有场x和y。为了支持这一点，记录的表示还必须将相应的字段名称与Object[]数组中的这是通过保留数组的第一个插槽作为对字段名称数组的引用来实现的，每个字段名称都从外部数组中标识剩余插槽的名称可以通过减少现场存在检查的数量来优化不同记录类型之间的区分。例如，在上面的例子中，检查场x的存在没有什么意义，因为它在两种情况下都是有保证的。Whiley编译器生成最小数量的字段检查，以确定存在哪些可能的情况。3注意，在空列表的情况下，类型测试始终成立。56D.J. Pearce，J.Noble/Electronic Notes in Theoretical Computer Science 279（1）（2011）4相关工作在这一节中，我们主要集中在与Whiley的流水敏感类型系统相关的工作上4.1数据流分析流敏感数据流分析已被用于推断各种信息，包括：流敏感类型限定符[21，22，12，17，27，13，1，41，4，35]，信息流[30，44，36]，类型状态[49，19，8]，字节码验证[33，32]等。类型限定符约束变量可能包含的值。 CQual是一个对时间敏感的限定符推理，支持许多类型限定符，包括同步和文件I/O [21，22]。CQual不考虑条件句的效果，因此重新输入是不可能的。Chin等人的工作是类似的，但对下行不敏感[12，13]JQual将这些系统扩展到Java，并考虑了整个程序（对下行不敏感）推理[27]。AliasJava引入了几个限定符来推理对象所有权[1]。unique限定符表示变量拥有对对象的唯一引用;类似地，owned用于将对象限定到其封闭的“所有者”对象的范围Füahndrich和Leino在C#的上下文中讨论了一个用于非空限定符的系统[18]。在这里，变量被注释为Nonvalues，以表明它们不能为null。非空限定符很有趣，因为它们要求在 条 件 句 之 后 重 新 输 入 变 量 （ 即 ， 在 v ！ = 之 后 将 v 从 Nullable 重 新 输 入 为Nonvalid）。null）。Füahndrich和Leino关注的不是类型的使用，而是主要关注与对象构造函数相关的问题。Ekman等人在JustAdd编译器中实现了这个系统，尽管关于变量重新类型化的细节很少[17]。Pominville等人还简要地讨论了使用SOOT构建的一个对数据流敏感的非空分析，它确实在！空检查[41]。JACK工具类似，但侧重于字节码验证[35]。这扩展了字节码验证器，增加了一个称为类型别名的间接层。 这使系统能够在主体a中将变量x重新键入为@ Nonvalues if（x！=空）条件。该算法是正式使用的Java字节码上操作的一个线程敏感的类型系统。JavaCOP提供了一种用于编写类型系统扩展的表达性语言，包括非空类型[4]。 该系统对空值不敏感，并且无法解释条件的影响;作为一种变通方法，该工具允许将可空变量x赋值给非空变量，前提是这是x！=之后的第一个语句。空条件信息流分析的问题是跟踪信息的流向，通常是基于安全原因限制某些流向。Hunt和Sands的工作在这里是相关的，因为他们采用了一种对湍流敏感的方法[30]。他们的系统是在一个简单的While语言的背景下提出的，与我们的语言没有什么不同，尽管他们没有考虑条件句的效果。Russo等人使用该系统的扩展版本来比较动态和静态方法[44]。他们证明，一个纯粹的动态系统将拒绝被认为是类型安全的亨特和金沙系统下的程序。JFlow扩展了Java，D.J. Pearce，J.Noble/Electronic Notes in Theoretical Computer Science 279（1）（2011）57静态检查对下行不敏感的下行注释[36]。最后，Chugh等人开发了一种基于约束（对JavaScript不敏感）的JavaScript信息流分析[15]。类型状态分析侧重于对对象状态的时间敏感的推理，通常是为了加强时间安全属性。类型状态是有限状态自动机，可以为常见的API编码使用规则（例如，文件在打开之前从未被读取），并由Strom和Yellin开创[48，49]。Fink等人提出了一个跨过程的、对流敏感的类型状态验证系统，该系统被分段以减少开销[19]。Bodden等人开发了一种程序间类型状态分析，该分析在程序内水平上是低敏感的[9]。这是一个混合系统，它试图静态地消除所有故障点，但在必要时使用动态检查。这后来被扩展到包括一个后向传播步骤，以提高精度[8]。Java Bytecode Verification需要一个对数据流敏感的类型化算法[33]。由于局部变量和堆栈位置在Java字节码中是无类型的，因此它必须推断它们的类型以确保类型安全。像Whiley一样，验证器在赋值后更新变量的类型，并使用最小上限运算符在控制流连接点组合类型。但是，它不会在instanceof测试之后更新变量的类型。此外，Java类层次结构不形成连接半，晶格为了解决这个问题，字节码验证器使用一个简化的最小上界完全忽略接口的操作符，而是依赖于运行时检查来捕获类型错误（参见例如[32]）。然而，一些关于形式化字节码验证器的工作选择用交集类型来解决这个问题（参见例如，[25，42]）。Gagnon等人提出了一种将Java字节码转换为中间表示的技术，每个变量都有一个静态类型[24]。关键是能够推断字节码中使用的局部变量和堆栈位置的静态类型。由于局部变量在Java字节码中是无类型的，这并不总是可能的，因为它们可以-而且经常-在不同的点有不同的类型;在这种情况下，一个变量根据需要被分成多个变量，每个变量都有不同的类型。Dubochet和Odersky [16]详细描述了结构类型如何在Scala中实现，并比较了在结构类型上实现方法调用的响应和生成方法。他们认识到，结构类型总是对当前的JVM施加惩罚，但描述了这两种技术在实践中通常如何提供足够的性能-在最坏的情况下，大约比Java接口调用5结论Whiley语言在JVM上实现了一个对线程敏感的结构化类型系统这允许隐式声明变量，允许在函数中具有多个类型，并允许在运行时类型测试之后重新类型化变量。其结果是一种静态类型的语言，在大多数情况下，具有动态语言的外观和感觉。在58D.J. Pearce，J.Noble/Electronic Notes in Theoretical Computer Science 279（1）（2011）在本文中，我们讨论了与Whiley在JVM上的实现有关的各种细节最后，可以从www.example.com免费获得Whiley语言的开放源码实现http://whiley.org。引用[1] J. Aldrich、V. Kostadinov和C.钱伯斯程序理解的注释。在Proc. OOPSLA，第311-330页[2] D. 安科纳湾Ancona，A.Cuni，和N.D. Matsakis RPython：协调动态和静态类型OO语言的一步 在proc DLS，第53-64页。ACM Press，2007.[3] C. Anderson，P. Giannini，and S. Drossopoulou面向JavaScript的类型推断。 在Proc. ECOOP，LNCS第3586卷，第428Springer-Verlag，2005.[4] C. André，J. Noble，S. Markstrum和T.米尔斯坦实现可插入类型系统的框架。 在proc OOPSLA，第57-74页。ACM Press，2006.[5] F. Barbanera和M.德扎尼-钱·卡格里尼交集和并集类型。在Proc. of TACS，Volume 526 ofLNCS，pages 651[6] G. Bierman，E. Meijer和M.托格森 迷失在翻译中：正式化对C#的拟议扩展。在proc OOPSLA，第479-498页，2007 年。[7] B. 天哪，J。Field，N. Nystrom，J. Oüstlund，G. Ri chards、细叶拟谷盗R. Strnisa，J. Vitek和T. 里格斯塔德。Thorn：JVM上健壮、并发、可扩展的 脚本。 在proc OOPSLA，第117-136页， 20 0 9 年 。[8] E.博登通过确定连续等效状态的高效混合型状态分析。在Proc. ICSE，第5-14页[9] E. Bodden，P. Lam，and L. J. Henrik。通过提前评估运行时监视器来更早地发现编程错误。 在procESEC/FSE，第36-47页。ACM Press，2008.[10] L.卡德利结构子类型和幂类型的概念。在Proc. POPL，第70-79页中。ACM Press，1988.[11] R. Cartwright和M.费根 软打字。 在Proc. PLDI，第278-292页中。ACM Press，1991.[12] B.钦，S。Markstrum和T.米尔斯坦语义类型限定符。在Proc. PLDI，第85-95页中。ACM Press，2005.[13] B.钦，S。Markstrum，T. Millstein，and J. Palsberg.用户定义的类型限定符和限定符规则的推断。《职工持股计划程序》，2006年。[14] J. - D.崔，M。Burke，and P. Carini.高效的对指针引起的别名和副作用敏感的过程间计算。 在procPOPL，第232-245页。ACM Press，1993.[15] R. Chugh，J. A.梅斯特河Jhala和S.勒纳阶段性的信息流为JavaScript。在Proc. PLDI，第50-62页，2009中。[16] G. Dubochet和M.奥德斯基 在JVM上编译结构类型。 在ECOOP 2009年面向对象语言，程序和系统（ICLOOPS）的实现，编译，优化研讨会，2009年。[17] T. Ekman和G.赫丁Java的非空类型的可插入检查和推理。JOT，6（9）：455[18] M. Füahndrich和K. R. M. 莱诺在非面向对象的语言中声明和编译非空类型。在proc OOPSLA，第302-312页。ACM Press，2003.[19] S. Fink，E. Yahav，N.多尔湾Ramalingam和E.天啊 有效的类型状态验证别名。ACM TOSEM，17（2）：1[20] C.弗拉纳根混合类型检查。在Proc. POPL，第245-256页中。ACM Press，2006.[21] J. S. Foster，M. F？hndri ch和A. 好吧 一个关于三个均衡器的理论。 在Proc. PLDI，第192-203页。ACM Press，1999.[22] J. S.福斯特，T。Terauchi和A.艾肯流量敏感型限定器。在Proc. PLDI，第1-12页中。ACM Press，2002.D.J. Pearce，J.Noble/Electronic Notes in Theoretical Computer Science 279（1）（2011）59[23] M. Furr，J.- H. An，J. Foster，and M.希克斯Ruby的静态类型推断。在Proc. SAC，第1859-1866页中。ACM Press，2009.[24] E.加尼翁湖Henan，和G.玛索java字节码静态类型的高效推理。Proc. SAS，第199-219页，2000年[25] A.金伯格Java加载和字节码验证的规范。 见Proc. CCS，第49-58页，1998年。[26] J. Gosling，G. S. B. Joy和G.布拉查Java语言规范，第三版。Prentice Hall，2005年。[27] D. Green fieldboyce和J.S.福斯特Java的类型限定符推理。 在Proc. OOPSLA中，第321-336页。ACMPress，2007.[28] S.好吧 Clojure编程 Pragmatic Programmers，2009年。[29] T. 霍尔参考资料：十亿美元的错误，在QCON，2009年的演讲[30] S. Hunt和D.桑兹对带宽敏感的安全类型。 在Proc. POPL，第79-90页中。 ACM Press，2006.[31] A. Igarashi和H.纳吉拉面向对象编程的联合类型JOT，6（2），2007.[32] X.勒罗伊Java字节码验证：算法和形式化。Journal of Automated Reasoning，30（3/4）：235[33] T. Lindholm和F.耶琳Java虚拟机规范Addison Wesley，第二版，1999年。[34] R. P. 路易In praise of scripting：Real Programming Pragmatism.IEEE计算机，41（7）：22[35] C.雄性，D. J. Pearce，A. Potanin和C.迪姆尼科夫 Java字节码验证@ Nonvalid类型。在proc CC，第229-244页， 2008年 。[36] A. C.迈尔斯JFlow：实用的大部分静态信息流控制。在Proc. POPL，第228-241页[37] J. K.奥斯特豪特脚本：21世纪的高级编程。IEEE Computer，31（3）：23[38] L. D.保尔森开发人员转向动态编程语言。 IEEE Computer，40（2）：12[39] D.皮尔斯和诺布尔。流量敏感型。技术报告ECSTR 10 -23，惠灵顿维多利亚大学，2010年。[40] B. C.皮尔斯类型和编程语言。麻省理工学院出版社，2002年。[41] P. Pominville，F. 钱河，巴西-地 瓦莱莱湖 H england和C. 维尔布鲁日。 一种使用属性优化Java的框架工作。在Proc. CC，第334-554页[42] C. Pusch.在isabelle/hol中证明java字节码验证器规范的可靠性。 在Proc. TACAS，第89-103页[43] D. Remy和J. J. Objective ML：一种有效的面向对象的ML扩展。对象系统的理论与实践，4（1）：27[44] A. Russo和A.萨伯菲尔德动态与静态对带宽敏感的安全分析。在Proc. CSF，第186[45] Scala编程语言http：//lamp.ep.ch/scala/。[46] J. Siek和W.塔哈逐步键入对象。在Proc. ECOOP，LNCS第4609卷，第151-175页。Springer-Verlag，2007.[47] D.斯皮内利斯 Java让脚本语言变得无关紧要？ IEEE Software，22（3）：70[48] R. Strom和S.耶米尼类型状态：一种用于增强软件可靠性的编程语言概念IEEE TSE，12（1）：157[49] R. E. Strom和D.M. 耶琳 使用条件活性分析扩展类型状态检查IEEE TSE，19（5）：478[50] T. Wrigstad，F. Z. Nardelli，S. Lebresne，J. Oüstlund和J. 维泰克 在脚本语言中集成了文本和非文本代码。在proc POPL，第377-388页。ACM Press，2010.