基于合作的不变量验证方法及其在面向对象编程中的应用

理论计算机科学电子笔记160（2006）225-237www.elsevier.com/locate/entcs面向对象语言中基于合作的不变量Ronald Middelkoop，CornelisHuizing，Ruurd Kuiper和Erik Luit埃因霍温理工大学数学与计算机科学系P.O. Box 513，5600 MB埃因霍温，荷兰摘要一般来说，不变量可以取决于其他对象的状态。本文中介绍的方法允许对相互可见的类的对象进行此操作，以支持模块化验证的方式。 为此，通过合作使依赖性变得明确。特别是，不变量表示非层次对象关系的支持。此外，内集允许方法显式地指定它不依赖于某个不变量的有效性。这样，即使不变量被违反，它也可以被调用。关键词：程序验证，不变量，模块化开发，面向对象编程。1介绍我们提出了一种方法，允许指定和验证强大的不变量，并支持面向对象（OO）开发的模块化风格。这样的模块化开发对于基于组件的范例是必不可少的。类不变式描述了从该类实例化的对象的一致状态。一般来说，这样的不变量可以将几个对象的状态联系起来。例如，在著名的观察者模式[4]中，当观察者的状态与其主体的状态相匹配时，观察者是一致的。传统上，人们期望不变量在方法执行的前状态和后状态中保持不变。我们的方法处理两个问题，这样的不变量第一个问题是，与任意对象相关的不变量不能被模块化地验证。这意味着我们必须限制这些关系。 我们引入1{r.middelkoop，c.huizing，r.kuiper，e.j.luit} @ tue.nl1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.05.025226R. Middelkoop等人/理论计算机科学电子笔记160（2006）225合作的概念，以最大限度地减少核查误差的方式明确表达关系。第二个问题是，来自不一致状态的方法调用有时是在观察者模式中，当主体的状态被更新时在我们的方法中，除非另有明确说明，否则为此，我们的方法引入了新的规范结构inc（不一致）。此构造允许方法显式指定它不依赖于某个不变式的有效性我们在1.1节中更详细地讨论了上面介绍的概念，并在1.2节中概述了本文的其余部分。1.1概念在本文中，我们考虑类Java的OO语言。OO程序的规范通常基于两个基本的规范构造，即方法的前置条件和后置条件以及类不变量。类不变量可以简化证明和规范，因为可以假设不变谓词在特定的程序状态中保持不变。此外，通过捕获所需的状态关系，不变量可以指导可以访问该状态的方法的设计不变量的能力是由它们的表达能力决定的，即。通过它们可以在程序状态中描述的关系以及通过它们的语义强度，语义强度确定了这种关系在哪些程序状态中成立。然而，为了使不变量成为规范的有用成分，它们的力量必须与它们的力量相平衡。 管理层由所需的规格分类决定(the所需关系的具体化）和验证分类（数量和与不变量相关的证明义务的复杂性最后，验证应该支持OO开发的模块化风格[13]。OO程序有一个显式的结构，其中类被分组到模块中（想想组件或Java包）。 模块化验证意味着类C是仅使用对C可见的类的指定进行验证，其中类D对当C和D在同一个模块中或者当C的模块导入D的模块时，类C此外，这种验证需要证明C是行为良好的。也就是说，存在着并非由C本身的具体化所引发的证明义务。这是为了保证一个类在任何行为良好的上下文中满足它的规范，因为类的行为可以被它不可见的类所忽略。例如，考虑重写方法，这需要一种行为子类型的形式[11，5]。1.2概述下一节将介绍本文中使用的一些基本术语。我们的方法在第3、4和5节中介绍。第3节讨论了合作，第4节处理来自不一致状态的方法调用，第5节提出了不变量的模块化验证的证明我们在第6节讨论现有的方法，在第7节讨论未来的工作。最后一节给出了我们的结论。R. Middelkoop等人/理论计算机科学电子笔记160（2006）2252272术语本节介绍与不变量相关的术语C和D标识类（也就是说，C和D是类名集合的典型元素）。f标识字段（也称为实例变量）。 为了简化表示，子类不允许定义已经在超类中定义的字段名（称为字段阴影）。扩展我们的方法以允许场阴影是简单的。α标识一个对象，即类的实例化（把α看作一个地址）。位置α.fC存储在类C中定义的对象α的 C类通常被省略，因为它可以从α的类型推断出来。 g表示形式为f的场访问。 对于i≥ 1，定义α1g1. gi以如下方式归纳：α1g1... gi= α2gi当α1g1. gi−1 = α2。 例如，当α1.f1=α2，α2.f2=α3，α1.f1.f2=α3.在类Java语言中，对象和它们的内容通过引用扩展访问。为了简单起见，我们只考虑由范围变量和零个或多个字段访问组成的引用。作用域变量s可以是关键字变量this、方法参数p、局部变量v或逻辑变量X。 参考 r是sg1.的表达式 gi，i ≥ 0.一个this-referencet是scope变量是什么作用域变量这在类Java中经常被省略。程序. 当r = s g1. gi和1 ≤ j ≤ i，参考s g1. gj被称为R的子引用（注意，R是R的子引用，但是由于技术原因，s不是）。在类Java语言中，方法选择是动态的，而字段选择是静态的。statType（r）生成引用r的静态类型。本文中的所有引用都假定是类型正确的（因此具有静态类型）。r #t，由r#（thisg1. . . gi ） d=efrg1. . . 吉岛例如，this.f1.f2 #this.f3.f4 = this.f1.f2.f3.f4。当α1g1... gi= α2，我们称之为-参考这个g1. gi表示从α1到α2。我们将允许的谓词子集称为不变谓词。我们使用R作为这种谓词的典型元素。在本文中，我们不考虑量化对象的不变量（见第7节）。实际上，这意味着不变量中的每个引用都是this引用。当此引用t出现在不变谓词R中时，我们称t的每个子引用为R的供应者引用。sup（R）产生不变谓词R的供应者引用的集合。当t.f∈sup（R）并且statType（t）=C，我们说R依赖于类C的场f。如果程序状态是方法执行的前状态或后状态，则它被称为可见状态[14]。传统的不变量语义，即所有不变量在所有可见状态下都成立，被称为可见状态语义。假设示例中的OO语法是自解释的。在示例中，我们忽略了如何指定方法保持不变的正交问题[9，18]。这个问题被缓解了，但不变量没有解决。此外，所有领域均被视为在规范层面公开可用。在这个层次上的隐藏场[16，13]是一个单独的问题。例如，参见[8，9，13]以获得对信息隐藏的特定语言支持。228R. Middelkoop等人/理论计算机科学电子笔记160（2006）225类节点{Node nextcoop I（this），J（next）; Node prevcoop J（this），I（prev）;invIdefthis.next =nullthis=this.next.prev;invJdefthis.prev =nullthis=this.prev.next;Node（）{this.prev：= null; this.next：= null;}public void run（Node n）{上一页：this.next=null下一页：此页上一页=null下一页/=null下一页：n.next=X发布：n.next=此站点this.next=X此.prev：= n; this.next：= n.next; n.next：=this; if（this.next/=null）{this.next.prev：=this;}}}例1. 双重链接节点3合作本节介绍合作的概念。合作意味着一个域通过规范化构造coop明确地规范化，当域被分配时，哪些不变量合作将依赖关系限制为相互可见的依赖关系（也就是说，当类C中的不变量依赖于类D的域时，D对C可见，反之亦然）。这个限制允许模块化验证给定可见状态语义的不变量。此外，这种明确的规定大大减少了所需的总验证时间。当然，最有表现力的不变量是那些可以依赖于任意场的然而，在这种情况下，任何分配都可能使这样的invari- ant无效。这意味着，给定可见状态语义，任何一对不变式和方法都必须被验证。在[7]中，使用全程序分析来验证这些对。不幸的是，这种方法不支持模块化验证（1.1节）。当模块化验证一个定义了一个不变量的类时，不能证明其他类的方法保留了不变量，因为它们的实现不可用。此外，当模块化地验证一个方法是否行为良好时，不能证明它保留了所有类的所有不变量，因为并非所有类都是可见的。因此，依赖性的限制是不可避免的。在我们的方法中，一个类可以定义多个命名的不变量。一个不变量在类中的定义如下invI defR也就是说，一个不变量有一个名字I和一个定义R（这是一个不变谓词）。IC标识在类C中定义的名为I的不变量。def（IC）产生不变谓词R，它是不变IC的定义。为了简化表示，我们不允许子类定义一个不变名称，在一个超类（我们称之为不变阴影）中已经定义了扩展我们的方法，使不变的阴影是简单的。在类中定义的不变式必须对该类的每个实例化都保持为了区分这些实例化，我们引入实例化的不变量。Instantiated InvariantIC（α）标识对象α上的不变量IC的实例化。要在规范语言中标识实例化的不变量R. Middelkoop等人/理论计算机科学电子笔记160（2006）225229被使用。当引用r引用对象α时，引用不变量IC（r）标识实例化不变量IC（α）。我们称r为IC（r）的相关引用。类名C在实例化或引用不变量中经常被省略，因为它可以从α当在给定状态下，位置α.f的值的变化可以使实例化的不变量I（α）无效时，我们称I（α）在该状态下易受α.f的攻击。例如，在示例1中，当α是Node对象时，J（α）在α.prev存储null而α. pre.next不存储α的状态下容易受到α.prev的攻击对于每个位置，我们的方法关联一组实例化的不变量，这些不变量可能容易受到该位置的影响。虽然这需要一些额外的规范分类，但它大大减少了总体验证分类。在一个行为良好的方法中，与该方法分配的位置相关的实例化不变量被重新证明，但是对于不在这个集合中的不变量，没有什么需要证明的（参见第5节）。注意，这得益于有多个命名的不变量。此外，这意味着集合越准确，所需的验证分类就越少。位置的属性由场的属性指定在我们的方法中，一个字段以以下方式指定修改T fcoop-集字段的访问修改器修改器、类型T和名称f都是标准的。coop-set是一组引用不变量。我们说场与这些引用不变量合作例如，在示例1中，类Node的fieldnext与I（this）和J（next）协作。当类D定义一个场f，且C是D的一个子类时，coop（f，C）产生类D的场f的coop-集。现在考虑一个位置α1.fC。 当这个参考t从α1指向α2时， 对于给定的一个状态，且I（t）∈coop（f，C），我们称α1，在该状态下fC与I（α2下面的合作义务确保了实例化的不变量仅易受与其合作的位置的攻击。只有满足此义务的不变量才是可接受的。当一个不变量可以写成不变量谓词R 1的析取时，它就满足了这个义务。. 其中dco（Rj，IC）对于每个间断Rj. dco（Rj，IC）成立，当对于R j的每个供应商参考t1.f，一个此参照t2，使得不变量所依赖的场f与I（t2）合作，并且使得Rj∈this=t1#t2。当不变谓词Rj成立时，这个蕴涵保证了与适当的实例化不变式的合作。合作：存在一组不变谓词R1到R1，使得：（def（IC）惠R1）。 . i）and（ij：1≤j≤i：dco（Rj，IC））dco（R，IC）d=ef∈t1， f：t1. f∈sup（R）：（t2：：I（t2）∈coop（f，statType（t1））anddRthis=t1#t2）例如，节点当R1为this.prev=null且R2为this=this.prev.next时，def（JNode）惠R1惠R2。R1有一个单一的供应商引用this.prev，它与字段prev有J（this）一样协作2 、230R. Middelkoop等人/理论计算机科学电子笔记160（2006）225在 它 的 coop-set中 ， 因 为 this=this# ， 这 是 平 凡 的 真 。 R2 有 供 应 商 参 考 资 料this.prev 和 this.prev.next 。 这 个 .prev 的 合 作 论 点 与 上 面 的 相 同 考 虑this.prev.next 。 这 个 .prev 的 静 态 类 型 是 Node 。 Node 类 的 字 段 next 与 J（this.next）合作，因为J（this.next）∈coop（next，Node）。以来this=this.prev.next此=this.prev#this.next，合作义务是met.在合作义务中处理单个析取项使得合作集比一次处理整个不变量时更准确。此外，它允许较弱的义务，这意味着更多的不变量是可接受的。一个不变式的静态供应商引用集合定义了一个实例化不变式的动态供应商集合：位置α1.f是一个给定状态下实例化不变式IC（α2）的供应商，当IC有一个供应商引用t.f并且t在该状态下从α1指向α2在任何状态下，IC（α）易受攻击的位置集合是其供应商集合的子集。该义务确保供应商对有效的不变量的分离进行合作。不变量不容易受到供应商，只发生在无效的析取，作为转让给这样的供应商可能会重新生效的析取，但不能使其无效。为什么义务确保与权利对象的合作是由下面的图片和文字说明通过定义，当t1.f∈sup（def（IC））且t1指α1到α2时，α2.f是IC（α1）的供给者。α2.f与IC（α1）合作，当存在this-引用t2使得IC（t2）∈coop（f，statType（ t1 ） ） 并 且 使 得 t2 从 α2 指 向 α1 。 第 一 种 是 由 义 务 明 确 保 证 的 第 二 个 由Rthis=t1#t2保证。由于这是从α1到α1的定义，这=t1#t2保证了t1#t2也是从α1到α1的。当t1表示从α1到α2，t1#t2表示从α1到α1，t2必须表示从α2到α1。（本）t1 ）（除了相互可见性之外，合作还需要依赖性引用的存在（上述示例中的t2也就是说，不变量然而，由于附加的要求，作为辅助状态（即，仅用于规范和验证目的确保不变量在应该保持的时候保持不变所需的义务的正式化被推迟到第5节。4来自不一致状态的通过本节中介绍的新的specification constructinc，方法可以明确表示它们不会依赖于某些对象的某些不变量。允许从这些不变量不一定保持的不一致状态调用这些方法。也就是说，inc允许指定器精确定位可见状态语义太强的可见状态，并仅针对这些特定状态削弱它。有时，如果没有α1与ICα2包含fcoopI（t2）t2R. Middelkoop等人/理论计算机科学电子笔记160（2006）225231classLeft{protected Right rcoop I（this），J（r）; protected int valcoop J（r）; protected int rValcoop I（this）;invIdefthis.rV al=this.r.val=this.r.l=this;public void run（）{Right ri：= new Right（this）;}void setRight（Right）{inc：I（this），J（ri）pre：this=ri.lthis.r=nullthis.val=Xthis.rV al=ri.valpost：I（this）this.r=rithis.val=Xthis.r：= ri;}public void run（）{inc：I（this）上一篇：this.r.l=thispost：我（）int i：= this.r.getVal（）; this.rVal：=i;}public classRight{protected int valcoop I（I）;protected int lvalcoop J（this）;invJdefthis.lV al=this.l.val=this.l.r=this;Right（Left le）{inc：I（le）前：le.r=null，值= 0，值 = 0post：I（le）this.l：= le; this.l.setRight（this）;}public int findDuplicate（int findDuplicate）{post：this.val=newV althis.val：= newVal; this.l.sync（）;}public void run（）{inc：I（this.l）post：return=this.valreturn：= this.val;}}}实施例2. 左/右（整型字段初始化为0，引用字段为null）方法调用，因为它需要访问一组字段，任何单一的方法。考虑示例2。类左的不变量I将左的Right正如val的指定所示，这可能会使右场l所引用的左对象的不变量I无效但是，setVal不能赋值给Left相反，它必须从不一致的状态调用Left挑战是允许这样的程序，而不必削弱不变量。作为一种解决方案，我们提出了一个削弱的基础上的想法，最直观的不变量几乎总是持有的可见状态语义。因此，我们将它们不存在的情况视为需要额外授权的例外情况，并再次依赖于某种形式的合作。为此，方法规范可以通过规范结构进行扩展，包括：inc：inc-set入集是一组引用不变量，该方法将不依赖于在其前提条件中保持。例如，Left一个方法继承了它覆盖的方法的in-set，如果需要的话，可以扩展它。我们的不变量的语义由以下定义捕获。定义4.1：一个程序有不变的性质i，对于程序的每个执行序列，以下成立：• 在方法执行的prestate中，无效实例化不变量的集合是由该方法的inc集合中的引用不变量标识的实例化不变量的集合的子集• 在方法执行的后状态中，无效实例化不变量的集合是该方法执行的前状态中的无效实例化不变量的集合的子集。232R. Middelkoop等人/理论计算机科学电子笔记160（2006）225请注意，此语义接近可见状态语义。所有的不变量在一个方法的前状态和后状态下都保持为空。只有涉及到初始化或更新某些不变量的方法可能需要一个非空的inc集。对于这些方法，保持了一个重要的单调性属性：在方法执行的前状态中保持的每个不变量，在该方法执行的后状态中保持（即使它在方法的入集中inc可以在不变量的类对要调用其方法的类可见时使用。当情况不是这样时，我们不得不依赖于更传统的技术，即使用一个标记来削弱不变量。一个布尔标记是一个布尔条件b（例如类的一个辅助布尔字段），它表示对象是否是一致的。当所需的不变谓词是R时，将不变谓词定义为bR。然后，当b为false时，不变量可能易受标记的攻击，但不受任何其他位置的攻击然而，这种技术是不变量和对象一致性之间的关系，是相反的。当对象是一致的时不变式才成立，而不是当对象是一致的时不变式才成立。虽然非常灵活，但使用标记意味着每当依赖不变量时都需要验证或指定标记。特别是，当指定方法时，必须决定它是否需要不变量。 与此相反， INC要求决定哪些方法涉及某些不变量的初始化或更新这就有了更多的实施自由。也就是说，inc-set通常是空的，这意味着每个不变量都可以被依赖。inc也可以更自然地使用子类化。子类中的重写方法可以依赖于超类方法不依赖的不变量，例如子类添加的不变量。这样的覆盖方法也可以用于更新或初始化额外的不变量，因为在子类方法中扩展inc集不会影响超类方法或其任何用户。5证明义务本节介绍适用于不变式模块化验证的证明义务。这些证明义务利用了前面几节介绍的coop和inc在证明义务的表述中，假设每个方法都被充分注释，即每个陈述x都有一个由Px标识的前提条件和一个由Qx标识的后置条件。建立了以下定理定理5.1当一个程序被正确地注释并且满足本节中提出的证明义务时，该程序具有不变性质。这个定理已经在一个类似Java的顺序语言中得到了证明。[12]这是一个证明在第3节中，我们定义了场何时与参考不变量合作引用不变量被添加到命题语言中，以描述场如何合作。引用不变量在没有被引用对象或R. Middelkoop等人/理论计算机科学电子笔记160（2006）225233被引用对象IC（r）d=efnoObj（r）def（IC）[r/this]P[r/this]是谓词P，其中this的所有出现都被r替换。noObj（r）定义为：noObj（sg1. . . gi）d=efj：0≤j≤i：sg1. . . gj=null不允许返回值被分配给具有非空coop集的字段的方法调用（即，应分为两个部分）。这避免了因方法返回上下文切换而失效的不变量的复杂性。扩展是简单的。简单地说，依赖义务确保了当一个赋值使一个不变量无效时：1。它在以后的状态中被重新证明，以及2.在重新证明之前，不调用依赖于不变量的方法。这个简单的概念被两个问题复杂化：1。需要跟踪可能无效的实例化不变式;以及2.状态（ment）排序由于分支和循环而变得复杂。为了简化表示，通过禁止在分支和循环中调用方法来避免后一种复杂性允许这样的调用是一个相当简单的扩展。然后，方法M的主体是方法调用的序列主体（M），并且局部不是方法调用的语句的代码块（LCB）我们写x y，当在物体（M）中x出现在y之前。calls（M）和lcbs（M）分别在body（M）中产生方法调用和lcbs的序列。LCB的前置条件和后置条件分别是LCB的第一个语句的前置条件和最后一个语句的后置条件。抚养义务如下。它使用一个逻辑变量X来不变量必须在赋值后的后置条件Qz中重新证明。在赋值和后置条件Qz之间调用的任何方法都不能依赖于不变量，这由下面定义的inInc保证为了提高本节中义务的可读性，隐含约束最弱，并且隐含左侧的所有自由变量都被认为是对隐含的普遍量化依赖性：x∈lcbs（M）包含s到r的赋值，f和I（t）∈coop（f，statType（r））意味着<$X：：Ps<$X=r#t，z：z∈body（M）且x≤z：（Qz<$I（X）and ny：y∈calls（M）andx y≤z：inInc（y，I，X））inInc需要几个其他的定义。inc（M）产生方法M的inc-set。e标识了一个旁射自由表达式。当语句y是对r.m（e1，.，ei），callee（y）产生由m和statType（r）确定的完全限定的方法名M。当被调用者（y）具有形式参数p1到pi时，act（rJ，y）等于rJ [r，e1，.，ei/this，p1，.，pi]，即act（rJ，y）在方法调用y的前状态中引用的值与rJ在被调用方法M的前状态中引用的值相同。inInc（y，I，r1）在callee（y）的inc集合中存在引用不变量时成立在调用的前状态中标识I（r1）所标识的相同实例化不变量234R. Middelkoop等人/理论计算机科学电子笔记160（2006）225inInc（y，I，r1）d=ef<$r2：r2∈{r|I（r）∈inc（callee（y））}：Py<$r1=act（r2，y）我们举例说明依赖义务的使用。考虑示例2中的方法setVal。 它由一个lcb和一个方法调用组成。LCB包含（con-sists of）对this.val的赋值。当I（this.l）∈coop（val，Right）时，满足依赖义务的左侧。 这意味着需要以下内容 方法的注释。 必须有一个逻辑变量X， X=this#this.l在赋值的前提条件中成立。此外，I（X）必须在赋值或方法调用的后置条件中成立。看看这个例子，第一个不会是这样，但第二个会。在这种情况下，inInc（this.l.sync（），I，X）也必须保持。由于Left方法M不变量义务确保M调用的任何方法都不依赖于这样的不变量，除非它在调用之前被重新证明。PM确定了主体（M）中第一个陈述的前提条件。不一致：I（r）∈inc（M）蕴含<$X：：PM<$X=r，x：x∈calls（M）：（inInc（x，I，X）或y∈body（M）且y≤x：Py<$I（X））这只剩下初始化的问题。一般来说，由类C定义的不变量I不会在该类的构造函数的前置状态中保持。 在类Java语言中，构造函数中的第一个（可能是隐式的）语句是对超类构造函数的调用.在Java语义中，这个调用的前状态中的this-object的动态类型是C或C的子类。由于动态方法绑定，超类构造函数中的方法调用可能会执行C的方法。由于不变量的语义，该方法假设所有对象都是一致的，但事实并非如此。在不限制不变量（默认情况下保持不变）或编程语言的情况下，没有模块化的方法来防止这种情况通过假设构造函数的行为更类似于C++的行为，可以避免这种限制我们假设在类C的构造函数的前置状态中，this-object的动态类型是Object。在（可能是隐式的）超类构造函数调用之后，有一个隐式语句将this对象的动态类型更改为C类型。 注意，当D是C的超类时，在超类构造函数调用的后状态中，this-object的类型是D第一个M标识方法M的第一个语句。构造义务确保不变量由构造函数初始化，并且在初始化之前不依赖于：构造：方法M是类C的构造器，C定义了一个不变量I蕴涵了：y∈body（M）和第一个M

下载后可阅读完整内容，剩余1页未读，立即下载