jContractor：Java中的契约式设计工具

55理论计算机科学电子笔记70第4期（2002）URL：http://www.elsevier.nl/locate/entcs/volume 70. html25页sjContractor：用于在Java帕克·阿伯克龙比a，1穆拉特·卡鲁曼b，2加州大学圣塔芭芭拉分校，加州93106b德州仪器公司315 Bollay Drive，Santa Barbara，CA93117摘要契约式设计是一种软件工程实践，它允许将语义信息添加到类或接口中，以精确指定其正确操作所需的条件。契约式设计的基本构造是方法的前置条件和后置条件，以及类不变量。本文介绍了jContractor的详细设计和实现概述，jContractor是一个免费的工具，允许程序员按照直观的命名约定将“合同”编写为标准的Java方法。前置条件、后置条件和不变量可以与任何类或接口相关联，也可以被任何类或接口继承。jContractor执行On-the-Challenge字节码检测，以检测程序执行期间违反合同规范的情况。jContractor的字节码工程技术允许它指定和检查合同，即使源代码不可用。jContractor是一个纯Java库，提供了一组丰富的语法结构，用于表达契约，而无需扩展Java语言或运行时环境。这些构造包括对谓词逻辑表达式的支持，以及对属性的入口值和方法的返回值的引用。细粒度控制，控制水平的监测是可能的，在运行时。由于合约方法被允许使用无约束的Java表达式，除了运行时验证之外，它们还可以执行额外的运行时监视，日志记录和测试。1电邮地址： parkera@cs.ucsb.edu2电子邮件：muratk@ti.com2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。一个伯克龙比和卡宾枪手561介绍契约式设计（DBC）是一种软件工程实践，通过指定有关程序运行时状态的断言来向应用程序接口添加语义信息。这些断言，统称为契约，必须在程序执行期间的特定检查点保持正确。方法前提条件是合约中指定方法调用者必须满足的状态的部分。不变量和方法后置条件提供了契约的另一半，指定了在方法执行完成时保持为真的相关状态信息。合约指定了控制模块接口的正确使用和实现的条件。将合约表示为与实际实现代码一起编译的指定代码是很自然的。可以评估合约代码以确保模块根据规范运行，但程序的正确执行不应依赖于合约代码的存在或检查。仍然期望在程序执行期间自动执行合约检查将布尔表达式（断言）与代码相关联作为论证代码正确性的一种手段的想法可以追溯到Hoare [4]和其他在程序正确性领域工作的人。Meyer引入契约式设计作为Ei语言的内置功能[9]，允许指定代码与可以编译为运行时检查的类相关联。在本文中，我们提出了一个详细的设计和实施概述jContractor，免费分发作为一个纯Java库，允许程序员添加合同的Java程序作为方法，遵循一个直观的命名约定。一个协定由与任何类或接口相关联的前置条件、后置条件和不变方法组成。合约方法可以直接包含在Java类中，也可以作为单独的合约类编写。契约也可以很好地与Java继承一起工作。在加载每个类之前，jContractor会检测Java类字节码中是否存在合约代码模式，并执行On-the-They字节码插装，以在程序执行期间启用合约在程序执行时评估合约会带来一些性能损失。然而，运行时契约检查在测试和调试期间是最有用的，当运行时速度通常不是关键的时候。合约代码可以保留在已部署的字节码中，但只有在调用jContractor时才会对合约进行评估。将合约保留在部署的代码中有助于故障排除，但在不检查合约时不会降低性能本文的其余部分组织如下。在第2节中，我们介绍从一个在Java中使用DBC的程序员的角度简要概述了jContractor。在第3节中，我们将详细介绍jContractor的设计和字节码插装技术，以支持运行时契约检查。最后，我们简要介绍了相关的工作，并讨论了替代用途一个伯克龙比和卡宾枪手57表1基本jContractor构造构建体jContractor模式和描述前提protected boolean methodname> Precondition（arguments>）在执行方法之前进行求值。先决条件失败表明调用者中存在错误。后置条件protectedbooleanmethodname>Postcondition（arguments>，return type> RESULT）在从方法返回之前计算。后置条件失败表示被调用方中存在错误。结果参数保存方法不变protected boolean Invariant（）在每个公共方法的开始和结束时进行评估。固定失败表示被调用方中存在错误。老classname> OLD; return count== OLD.count +1;允许后置条件在方法入口处引用对象的状态。jContractor执行其他运行时监控。2jContractor概述jContractor可以在www.example.com上以开源形式http://jcontractor.sourceforge.net。它是一个纯Java应用程序，可以在所有支持Java的平台上运行。在本节中，我们将概述jContractor如何促进编写合约并在运行时启用合约检查。2.1使用jContractorjContractor中的契约被编写为遵循命名约定的方法。支持的构造及其模式在表1.所有合约方法都返回一个布尔值，这是合约评估的结果。如果合约方法返回false，则会抛出异常。先决条件前置条件方法采用与它关联的方法相同的参数，并在方法执行前立即进行检查一个伯克龙比和卡宾枪手58调用者有责任确保先决条件检查成功。后置条件后置条件方法接受与它所关联的方法相同的参数，后跟一个与该方法的返回类型相同类型的额外的RESULT参数对于void方法，将RESULT声明为类型java.lang.Void。与检测方法关联的后置条件将在方法返回前立即检查，该方法带有保存方法返回值的RESULT参数。这允许后置条件对方法的结果进行断言。实现方法的类有责任确保后置条件成立。不变量不变方法类似于后置条件，但不接受任何参数，并隐式地与所有公共方法相关联。它在每个公共方法的开始和结束时进行评估。实现类负责保证不变式检查的成功。我们的方法与Ei Eisel的不变量检查略有不同，foo.bar当bar（）方法被同一个类中的另一个方法调用时，不检查它的不变量。这种区别使Ei类不必在其内部操作期间维护不变量旧参考文献jContractor允许后置条件在方法入口引用对象的状态。要启用此功能，类必须声明一个与该类类型相同的名为OLD的实例变量。后置条件可以通过引用OLD访问属性或执行方法。字节码插装将所有对OLD的引用路由到在方法入口处创建的对象的克隆。克隆是使用clone（）方法创建的，因此类必须实现java.lang.Cloneable接口并定义此方法。谓词逻辑量化器jContractor还提供了一个支持库，用于使用谓词逻辑量化器和运算符（如Forall、Quests、suchThat和implies）编写表达式。支持的量化器在java.util.Collection实例上运行，如表2所示。这些量化器提供了高层次的抽象，并大大提高了编写合同规范时的可读性。一个伯克龙比和卡宾枪手59表2 jContractor构建体jContractor模式和描述ForAllForAll.in（集合）.确保（断言）确保集合的所有元素都满足断言。存在Exists.in（collection）.suchThat（assertion）确保集合中至少有一个元素满足假设.元件Elements.in（collection）.suchThat（assertion）返回一个java.util.Vector，其中包含集合中满足断言的所有元素。意味逻辑.暗示（A，B）如果A和B都为真，或者A为假，则计算为真。 的逻辑等价物A和B。2.2使用jContractor运行一个启用了合约检查的程序就像将类名和命令行参数传递给jContractor程序一样简单例如，包含jContractor合约的程序可以在不进行运行时合约检查的情况下运行，%java Foo arg1 arg2 arg3.要运行具有完整合同检查的同一应用程序，可以输入% java jContractor Foo arg1 arg2 arg3.jContractor将用一个专门的类加载器替换系统类加载器，它将在加载类字节码时对其进行检测，并执行Foo程序。jContractor允许用户为系统中的每个类指定插装级别（仅前置条件、前置条件和后置条件，或所有契约）。要执行Foo程序，只检查先决条件，但检查bar包中的先决条件和后置条件，以及FooBar类中的所有契约，可以输入% java jContractor -pre * -post bar.* - 所有酒吧。FooBar Fooarg 1 arg 2 arg 3.jContractor支持类似于Java导入状态中使用的通配符，允许用户简洁地指定插装级别。的一个伯克龙比和卡宾枪手60也可以从文件中读取仪表水平。仪器水平（前、后和所有）是Meyer在[10，p.393]和[9，p.133]中建议的水平。其基本原理是，要满足方法的后置条件，前提条件必须已经满足。不变量只有在前提条件和后置条件都满足的情况下才能满足。不检查前置条件而检查后置条件，或者不检查前置条件和后置条件而检查不变量，都是毫无意义的。在某些情况下，不可能替换系统类装入器。例如，Web浏览器用来加载Java小程序的类加载器是由程序员控制的在这种情况下，jContractor可以将插装的字节码写入磁盘，创建一组插装的类，这些类 与 原 始 的 未 插 装 的 类 并 行 。 这 些 插 装 类 可 以 在 没 有 完 整 的jContractor发行版的情况下执行。要检测文件Foo.class，可以执行jContractor% JavajInstrument Foo.class这个命令将用插装的字节码覆盖Foo.class。3设计与实现jContractorjContractor在字节码级别对类进行了插装，但是在3.1节到3.7节中的讨论使用Java源代码模型来说明代码转换。字节码实现细节在3.8节中讨论。在第3.1节中，我们将讨论简单的仪器技术。在下面的章节中，我们将在基本的基础上开发一个健壮的契约式设计实现。3.1实施简单的合同检查jContractor使用的基本插装技术是在加载每个类之前对其执行以下步骤对于类C中每个签名为s的非契约方法m，• 在C中搜索一个名为m的方法，该方法的签名为s，或者搜索一个单独的合约类C CONTRACT，并将对m的调用前置到m。• 在C或C CONTRACT中搜索一个名为m、签名为s、带有附加参数RESULT的Postcondition的方法，并附加一个对m的后置条件。• 如果m是public的，则在C和C CONTRACT中搜索名为Invariant的方法。一个伯克龙比和卡宾枪手61公共虚空推（对象（二）如果（！ I n v a r i an n t（））扔新invariantVIOLATIONError（）;如果（！（a）在（a）段中，扔新Prec nditio nVio latio nErro r（）的情况;I m plementatitonn.return（i）;如果（！ 普乌舍Postco nditio n（o，null））扔新public void run（）;如果（！ I n v a r i an n t（））扔新invariantVIOLATIONError（）;}是的。乌特湖矢量的多方向性;...公共虚空推I m plementatitonn.return（i）;（对象（二）}Fig. 1. Stack.push（Object）的列表图二. Stack.push（Object）的简单插装在m的开头和结尾插入对invariant方法的调用。在运行时检查合约包括调用合约方法，如果结果为false则抛出异常。 乍一看，检查合同非常简单。 只需要在方法的开始或结束处添加对合约方法的调用，并在接触评估为false时抛出异常。jContractor抛出以下异常：PreconditionVi-olationError、PostconditionViolationError和InvariantViolationError。这三个都扩展了java.lang.AssertionError。为了演示插装过程，我们使用Stack类的push（Object）方法简单的代码转换可能会导致图2所示的插装推送（Object）方法。这几乎是正确的，但忽略了一个重要的问题，这将在下一节中讨论。3.2断言评估规则在运行时检查合约通常有助于发现错误并验证正确性。但是，必须注意防止合同检查本身引入错误。考虑一下在这个简单的例子一个伯克龙比和卡宾枪手62SS级堆栈{...公共in tsize （）{... 个文件夹保护booleanInv a r iant（）个{返回size（）=0;}}当检查不变量时，将执行size（）方法以确保大小是非负的。size（）是一个公共方法，因此应该在其入口点检查样本不变式。但是检查不变量需要调用size（），这会导致合约检查的无限递归。为了避免这种情况，契约式设计包括断言评估规则[10，p.402]，它规定一次只能检查一个契约。 在Stack示例中，不变量将调用size（）。由于已经有一个契约检查正在进行中，所以不变量将不会在size（）上进行检查。实现断言评估规则要求jContractor跟踪合同检查的进行情况。此信息与每个活动线程相关联。jContractor通过维护主动检查合约的线程的共享哈希表来实现断言评估规则。在线程检查合约之前，它会查询表以查看它是否已经在检查合约。如果没有，线程将自己插入到表中，并继续进行契约检查。检查完成后，线程将自己从表中删除。jContractorList类提供了静态方法来确定线程是否正在检查协定，并管理每个线程上的断言检查锁。图3显示了插装的push（Object）有必要将每个合约检查包装在一个try-finally块中，以便即使在检查合约时抛出异常，也可以释放锁通常，违反约定会终止程序，在这种情况下，锁是否被释放并不重要。但是错误是可以被发现和处理的。如果是这样的话，如果锁没有被释放，合约检查将在运行的剩余时间内停止。3.3谓词逻辑支持契约通常涉及约束，这些约束最好使用谓词逻辑量化器来表达。例如，在图结构中，可能有一个节点数组，每个节点都可以连接到其他节点。使用此结构的在数学符号中，这样的约束可以写为n ∈ nodes |n.连接>= 1一个伯克龙比和卡宾枪手63公共虚空推（对象（二）如果（j）在本报告中， public void run（）{j.重新运行时间。public void run（）;如果（！ I n v a r i an n t（））扔新不变的暴力（）的情况;如果（！ 推先决条件（o））扔新预编码错误（）的情况;尝试{}最后，你可以进入无线电。reeleaseseA sert i onCheck（）;}}I m plementatitonn.return（i）;如果（j）在本报告中， public void run（）{j.重新运行时间。public void run（）;如果（！ I n v a r i an n t（））扔新不变的暴力（）的情况;如果（！ 推POSTCONDITION N（O，null））扔新 Pos t condi t onV i ol a t o n（）;尝试{}最后，你可以进入无线电。reeleaseseA sert i onCheck（）;}}}图3.第三章。Stack.push（Object）的最终检测版本jContractor允许合约是任何计算结果为布尔值的函数，因此可以使用循环编写图约束，如下所是的。乌特湖收集节点;...是的。乌蒂湖它是一个i =节点。i t r a to r（）;而（一）public void run（）{如果 （（Node）i. next（））。C o n n e c t i o n s 1）<返回f a l s e;}返回真的;使 用 循 环 是 可 行 的 ， 但 它 需 要 程 序 员 为 每 次 使 用 重 写 量 化 器jContractor o使用一个简单的Java库为常见的谓词逻辑表达式提供高级编程jContractor这一个伯克龙比和卡宾枪手64表3jContractor提供的断言断言描述InstanceOf断言对象属于特定的运行时类型。平等断言对象是相等的。程序员指定比较应该是通过引用还是通过值。InRange断言一个数字落在最小和最大边界之间。不使用 到 否定另一个断言，如new Not（new Equal（Foo））。库与主jContractor代码完全隔离，可以独立使用。图不变量可以使用jContractor的语法表示是的。乌特湖收集节点;...A s e r t i o n连接=新 public void run（）{公共布尔e v a l（对象（二）返回（（节点）o）。1= 1;}}的情况;返回对于All。i n（节点）。e n s u r e（connected）;这个版本与使用循环的版本长度相同，但它使合约更显式。包中提供了一些常用的断言，并在表3中进行了总结。例如，确保集合的每个元素都符合特定的运行时类型非常简单，如下面对于All。in（元素）。 确保（新Insta nceOf（I n t e g e r. cla ss））;这种类型的断言对于控制可以存储在数据结构中的对象的类型很有用。在Java中实现quantifier的逻辑非常容易，因为所有常见的数据结构都实现了java.util.Collection接口，并提供了迭代器。最大的障碍是找到一种 干 净 的 方 式 将 代 码 传 递 到 迭 代 器 对 象 中 。 jContractor 通 过 引 入Assertion 接 口 解 决 了 这 个 问 题 ， 该 接 口 声 明 了 标 准 接 口 方 法 eval（Object）来测试断言。ForAll量化器的实现如图4. 以类似的方式实现元素量化器和元素量化器。最后，Logical类的静态implies方法允许程序员编写A implies B形式的表达式，其中A和B是布尔类型。一个伯克龙比和卡宾枪手65∼∨公共I n t e r f a ce联系我们公共布尔e v a l（对象o）;}公共 c l as sFo rAll {保护是的。乌特湖收集收集;公共对于A l l（C collect ion）（c）收集=c、}公共A llin（j a v a. 乌特湖C）{return newForr A l l（c）;}公共布尔e n s u r e（A sse rtio n（a）是的。乌特湖I t e r a t i = the Collec tion .i t e r a t or r（）;而（一）public void run（）{如果（！a.e v a l（i.publicvoid run（）{返回f a l s e;}}返回真的;}}见图4。 j承包商这样的表达式是A B的逻辑等价物。 使用jContractor语法，表达式将被写为Logical.implies（A，B）。3.4实现结果后置条件经常对函数的结果进行断言，这意味着后置条件方法必须有一种引用函数返回值的方法。在jContractor中实现此功能需要捕获结果并将其作为额外的参数传递给后置条件方法。如果方法无效结果的运行时值将始终为空。支持结果的机制很简单。jContractor为每个方法添加一个新的局部变量，并使用后置条件存储结果。字节码插装将返回指令替换为将返回值保存到结果变量的指令。最后，插装确保在契约检查期间将计算结果传递给后置条件。对于void方法，没有要保存的结果，因此将空值传递给后置条件。图5中显示了一个插装size（）方法的Java模型，以说明这种转换。一个伯克龙比和卡宾枪手66公共in t尺寸（）个{int$r e s u l t = i m plementa t i o n.sort（）;如果（j）在本报告中， public void run（）{j.重新运行时间。public void run（）;如果（！sizeP ostcondition（$result））扔新 Pos t condi t onV i ol a t o n（）;尝试{}最后，releaseA ssertionChec k（）的情况;}}返回$re sul t;}图五. 支持结果3.5实施OLD后置条件通常表示方法的执行如何改变对象因此，后置条件必须能够在执 行 方 法 之 前 引 用 对 象 的 状 态 。 Ei Ezel 为 此 提 供 了 old 关 键 字 。jContractor通过引入OLD实例变量来模仿Ei Jumel两种实现的语法如图6所示。为了访问jContractor中的旧值，类必须显式声明一个名为OLD的私有实例变量，与类的类型相同。变量是私有的，因为它只在声明它的类中有意义。子类将声明自己的OLD变量。有两种方法可以支持旧引用。第一个技巧是简单地将代码从旧引用移到方法的顶部并保存结果。 这种方法的一个例子如图7所示。这种技术在其他一些依赖源代码的Java DBC工具中得到了成功的应用[2，6，8，11]。但是，当检测字节码时，这是不可行的。jContractor可以处理任何有效的Java字节码，即使是那些已经运行了混淆器和优化器的字节码。严重混淆或优化代码的可能性使得提取构成OLD引用的代码变得极其困难（如果不是不可能的话）jContractor使用的第二种方法是在执行方法体之前创建对象的克隆。当jContractor检测一个后置条件方法时，它将对OLD的引用重定向到在方法入口处保存对象状态的克隆副本。jContractor使用clone（）方法来创建副本，因此所有包含OLD引用的类都必须实现可克隆接口。图8说明了这种方法。不幸的是，简单地将克隆状态存储在OLD实例变量中是不够的，因为需要在每个一个伯克龙比和卡宾枪手67公共虚空推（对象（二）int$old大小=return（）;//////////检查前提和输入n v a r i a n t方法体检查在检查使用大小为$ o l d的位置pl a c e of OLD.s i z e（）退出不变}艾勒切尔类STACK [ G ]特征push（n w object：G）is deferred确保西泽增加：大小= o l d size + 1 endend−−cla ss STACKjContractor公共摘要c l a s s堆栈{私人堆栈旧;公共摘要虚空推（对象o）;保护布尔推POSTC ENDITION N（）个{返回size（）== OLD. int n = 1;}}图六、旧版本的Ei Contractor和jContractor语法比较见图7。通过选择性地保存数据在后置条件中使用OLD的方法。在最坏的情况下，需要为每个方法调用保存OLD。这导致jContractor采用基于堆栈的解决方案变体。当执行进入一个需要保存OLD的方法时，jContractor创建一个对象的克隆，并将其推送到堆栈上。当方法退出时，对象从堆栈中弹出，并用于检查后置条件。jContractor一个伯克龙比和卡宾枪手68公共虚空推（对象（二）你可以进入无线电。push State（c l o n e（））;//P r e c o n d it i t i o n和entry i v a r i a nt检查//方法体//Post c o n d it i n和e Xiti n v a r i nt检查}保护布尔推邮政编码（对象不，Stack $ol d =（Stack）j contra ct or R un t i m e.return（）;返回count（）== $ o l d . int n = 1;Void RESULT）{}公共虚空推（对象（二）String s =（String s）;//检查前提条件和入口变量//方法体//检查位置，位置;老持有s t a t e在入境//检查退出不变量}见图8。 使用克隆见图9。 使用堆栈3.6单独的合同类别jContractor允许在单独的合约类中编写合约。合同类遵循命名约定类名合同。当in-strumenting一个类时，jContractor将找到它的合约类，并将所有合约代码复制到非合约类中。如果在两个类中定义了相同的契约（例如，两个类都定义了一个方法的先决条件），则两者在逻辑上是与的。在单独的类中定义合约允许jContractor将合约添加到源代码不可用的类中。3.7继承和合同jContractor的契约式设计实现在类和接口继承方面都很好。类从它的超类和实现的接口继承合约。方法图10显示了如何将所有部分组合起来形成完整的契约。任何插装方法都必须• 接受对超类方法有效的所有输入和前提条件状态• 满足超类方法一个伯克龙比和卡宾枪手69classFoo_CONTRACT {booleanm_Precondition（）{ }boolean m_transform（）{.publicvoid run（）{ 个文件夹}classSuperFoo {public voidrun（）{ 个文件夹booleanm_Precondition（）{ }boolean m_transform（）{.public voidrun（）{ 个文件夹}publicclassFooInterface_CONTRACT{booleanm_Precondition（）{. }boolean m_transform（）{.publicvoid run（）{ 个文件夹}//工具化版本类Foo扩展了 SuperFoo实现FooInterface {public voidrun（）{检查不变量检查前提条件原始方法主体检查后置条件检查不变量}}public voidrun（）{return接口前置条件|| super.m_Precondition（）（外部先决条件）&&原先决条件）;}public booleanunique（String s）{return外部后置条件接口后置条件&&super.m_后置条件（结果）&&原始后置条件;}public voidrun（）{return外部不变量接口不变量&&super. Invariant（）&&原不变量;}}类Foo扩展了 SuperFoo实现FooInterface {public voidrun（）{ 个文件夹booleanm_Precondition（）{ }boolean m_transform（）{.public voidrun（）{ 个文件夹}见图10。合同是如何组合的。实线显示字节码被复制的位置，虚线显示方法调用被插入的位置换句话说，子类方法只能这意味着，表4方法契约的四个部分内部合同在与方法相同的类中定义。外部合同在单独的合同类别中定义。超类契约从超类继承的。接口合同从接口继承。一个伯克龙比和卡宾枪手70SS级A{公共I n tFoo（）下一页保护布尔}{.. . 个 文件夹福澳POSTC ENDITION N（int）结果）{... 个文件夹SS级B延伸A{公共I n tFoo（）下一页保护布尔{...}//Ove rride sA. foo（）的缩写返回super. f o o P o s t c o n d i t i n（RESULT）（RESULT> 0）;FOO PO STC ENDITION N（int）结果）{}}见图11。 后置条件继承子类方法与超类的前置条件是逻辑或，后置条件是逻辑与。这要求子类接受所有对超类方法有效的输入，并且可以接受更多对超类无效的输入。然而，它必须遵守其母公司所作的保证，尽管它可能会加强这些保证。和后置条件一样，类不变量也是逻辑与。jContractor通过检测每个合约方法来调用超类合约方法来实现合约继承图11显示了这种检测的一个示例。实现合约继承的另一种方法是将合约方法从超类复制到子类中。但是，我们觉得这种方法不如调用超类方法那么干净。更重要的是，当契约引用超类中的私有成员时会出现问题。将合约代码复制到子类中会导致非法访问错误。调用超类合约在超类的上下文中计算合约，并正确处理私有成员。然而，上面描述的技术不适用于接口，因为接口不能包含合约代码。接口合约必须在单独的合约类中编写，jContractor将找到并合并到实现类中。继承的契约保证当在对象上调用方法时，无论对象的运行时类型如何，都将满足契约。然而，这种保证只对行为多态的方法有意义。私有方法、构造函数和静态方法不以这种方式工作，因此合约继承对这些方法没有意义。jCon-tractor认识到这一点，并且只对非私有、非静态、非构造函数的方法强制执行继承的契约。3.8字节码插装的实现到目前为止，我们对契约检查的讨论已经说明了使用Java源代码模型的代码转换。然而，实际的插装是使用Java类字节码完成的，并与源代码的逻辑相匹配。一个伯克龙比和卡宾枪手71阵jContractor使用字节码工程库（BCEL）[1]在字节码级别上检测类，而不需要源代码或额外的编译。图12显示了pop（）及其后置条件的源代码图14和图15给出了这些方法为了简洁起见，这个方法没有检测到一个不变量，也没有先决条件。检查前置条件和不变量的模式非常相似。由于Java方法可以包含任意数量的return语句，jCon- tractor将所有return指令替换为跳转到方法末尾，在此插入代码以检查后置条件和退出不变量。jContractor使用clone（）方法允许后置条件引用成员的入口值。但是，这会在后置条件和clone（）之间创建依赖项。在计算从clone（）或从clone（）调用的方法调用的后置条件时，试图保存对象由于clone（）方法需要检查合约，因此在执行clone（）本身时无法检查合约。图14中的语句13请注意，返回指令已被替换为跳转到方法末尾。(This可以消除跳转，但jContractor不执行此类优化。）语句29将结果保存到局部变量$result中，jContractor将其添加到方法中。语句30和33检查是否应该检查后置条件。如果是，则通过语句39-44检查后置条件。语句47至此，已经讨论了运行时契约检查中涉及的所有主要问题。最终目标（将契约检查代码添加到类中）是通过小而大部分独立的子目标（例如，添加代码以检查先决条件或处理旧引用）来实现的。jContractor采用装配线方法来实现字节码插装。每个独立的操作都被编码为一个单独的 类 ， 扩 展 了 一 个 抽 象 的 Transformation 类 。 然 后 ， 每 个Transformation对象处理要插装的类文件，在序列的最后，它完全插装。图16显示了jContractor应用的转换序列。这种架构简单，但有效。大多数转换是完全独立的。但是，有一些需要保存数据以供后续转换。创建了一个共享哈希表，一个转换可以将数据 放 入 其 中 ， 以 便 稍 后 由 另 一 个 转 换 读 取 。 这 个 解 决 方 案 对 于jContractor来说是令人满意的，但也有很多改进的机会。一个普遍有用的框架将提供一个更受控制的机制，以允许转换来交换数据。一个伯克龙比和卡宾枪手72公共对象流行（）个{返回I m plementa t i o n. remove（s i ze（）−1）;}保护布尔博普POSTC ENDITION N（对象结果）{返回（结果！=null）（size（）== OLD.尺寸−1）;}见图12。 Stack.pop（）和后置条件public Object pop（）0：aload 01：get fieldStack.implementation Ljava/util/Vector;（4）4：负载05：invokevirtual Stack.size（）I8：iconst 19：isub10：invoketvirtualjava.util.Vector.remove（I）Ljava/lang/Object;13：areturn局部变量：index = 0：Stack thisprotected boolean pop Postcondition（ObjectRESULT）0：aload 11：ifnull #244：负载05：invokevirtual Stack.size（）I8：aload 09：get fieldStack.OLD LStack; 12：invokevirtual Stack.size（）I15：iconst 116：isub17：如果icmpne #2420：iconst 121：goto #2524：图标0第25章：我的天局部变量：index = 0：Stack thisindex = 1：对象结果图13.未检测的Stack.pop（）和Stack.pop后置条件的字节码列表一个伯克龙比和卡宾枪手73public Object（）如果当前线程没有检查协定，则调用$saveState（）创建并保存对象的克隆。13：aload_014：getfield Stack.implementation Ljava/util/Vector; 17：aload_018：invokevirtual Stack.size（）I 21：iconst_122：isub23：invoketvirtual java.util.Vector.remove（I）Ljava/lang/Object; 26：goto #29原始方法体。局部变量：index = 0：Stack thisindex = 1：Object $result第29章：我的天将结果保存到$result。30：invokestatic jContractorList.canCheckAssertion（）Z33：ifeq #6336：invokestatic jContractorList.lockAssertionCheck（）V39：aload_040：aload_141：invokevirtual Stack.pop_Postcondition（Ljava/lang/Object;）Z 44：ifne #6047：new PostconditionViolationError>50：up51：ldc“jContractor Exception：Postcondition Violated”53：invokespecial PostconditionViolationError.& lt;init>（Ljava/lang/String;）V 56：invokestaticjContractorList.releaseAssertionCheck（）V第59章：一夜情60：invokestatic jContractorList.releaseAssertionCheck（）V如果线程还没有检查合约，则检查后置条件。第63章：不一样第64章：你是谁回想一下结果，并从该方法见图14。 已检测的Stack.pop（）的4今后的工作和相关工作4.1工厂样式实例化在本文中描述的实现允许用户来控制下到类级别的编译。但是，可以在逐个实例的基础上控制客户端可以调用jContractor.create（String，Class[]，Object[]）方法，而不是使用new关键字创建对象，该方法将实例化并返回类的插装实例。工厂风格的实例化可以通过对jContractor当前的字节码转换进行轻微修改来实现。首先，jContractor将创建一个新类，它是基类的子类然后，将为超类的每个非私有方法添加一个方法这