基于命令类的OO语言的余代数语义和观测等价性的研究

理论计算机科学电子笔记104（2004）163-180www.elsevier.com/locate/entcs基于命令类的OO语言的余代数语义和观测等价性Furio Honsell1 Marina Lenisa2，3DipartimentodiMatematiceInformatica，Universit`adiUdine， Viadelle Scienze 206，33100 Udine，ITALY.RekhaRedamallaDipartimentodiMatematiceInformatica，Universit`adiUdine， Viadelle Scienze 206，33100 Udine，ITALY，和B.M. Birla科学中心，Adarsh Nagar，Hyderabad，500 063 A.P.，印度摘要Fickle是一种基于类的面向对象的命令式语言，它通过对象重新分类来扩展Java。在本文中，我们介绍了一个自然的观察等价的Fickle程序。这是关于给定的类定义序列的主方法的上下文等价，即程序。为了研究它，我们使用的正式计算模型OO-编程的基础上，最近出现的余代数，即对象被认为是平等的方法时，他们的行动产生相同的意见和等价的下一个状态。然而，为了处理命令式特征，我们需要以各种方式扩展H.Reichel和B.Jacobs的原始方法。 特别是，我们引入了一个coalgebrical描述的对象（状态的一个类），这会导致一个coinductive的行为等价的程序。为了简单起见，我们关注Fickle对象，其方法不接受多个对象参数作为参数。完整性的结果，以及二元方法所产生的问题进行了讨论。关键词：基于命令类的面向对象编程，观测等价，共代数语义，共归纳行为等价。1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.08.024164F. Honsell et al. / Electronic Notes in Theoretical Computer Science 104（2004）163-介绍在全球计算界，基于类的面向对象语言受到越来越多的关注尽管如此，然而，相对较少的工作已经做了程序等效的语言。这可能也是由于没有OO编程的正式模型被普遍接受的事实。近年来，Reichel和Jacobs [13，9]引入了基于余代数的模型。支撑这种方法的思想是，余代数，代数的子代数，允许关注对象的行为，同时从自我的具体表示中抽象出来。这种方法主要用于将逻辑规范、程序和数据精化技术扩展到OO语言（见[10，5]）。本文旨在开展一项研究计划，探讨利用共代数计算模型进行程序等价性和程序转换的可能性。这是一个有点双重的目标w.r.t. Reichel和Jacobs的程序改进。为此，我们需要直接解决与命令式特性有关的关键问题，以及二进制方法，即采用多个对象参数作为参数的方法。我们关注的是基于类的命令型语言Fickle的一个片段，[4]，它通过重新分类扩展了Java。重新分类允许对象动态地改变类成员，同时保持它们的身份。我们认为Fickle作为这类类型的命令式基于类的面向对象语言的代表，本文的结果也适用于Java和类似的语言。我们研究（家庭）的上下文等价物CUP-P（由程序P索引）的Fickle表达式（即主体方法）。为了这个目的，我们利用一个coalgebrical行为等价的善变对象。我们的主要结果是一个足够的共代数语义的Fickle表达式w.r.t.等价物共代数语义起源于Aczel-Mendler，Rutten-Turi，用于CCS类语言，[1，2，15]，并进一步推广到λ-演算，[6]，高阶命令式语言，[12]，函数设置中的面向对象语言，[13，9]，π-演算，[7]。共代数语义学范式（final semantics）的要点是将从语法到语义的解释函数视为适当范畴中的final映射为此，语义必须被解释为最终的*研究得到了UE项目IST-2001-33477DART和MIUR项目COFIN 2001013518COMETA的支持。1电子邮件：honsell@dimi. 联合国。I T。2电子邮件：lenisa@dimi. uni ud. IT。3通讯作者。4电子邮件：rrekhareddy@yahoo.com。F. Honsell et al. / Electronic Notes in Theoretical Computer Science 104（2004）163-165≈一个合适的函子F的余代数和语法必须转换为F-余代数的形式。这种方法是由语言的操作语义驱动的，因为正是语义决定了函子F的结构。这与代数语义（初始、指称语义）的语法驱动方法是对偶的，其中语法被解释为初始F-代数，语义被定义为F-代数。 共代数语义的主要优点是，它诱导程序上的行为等价性，其特征可以被描述为共代数双相似性，即最大的共代数互模拟。关于余代数语义的代数，我们参考[11]。然而，在原来的共代数方法中，只有一个孤立的类被认为是和设置是纯粹的功能。在处理Fickle时，[13，9]的方法需要改进以适应命令式特征以及一般程序，即可能通过继承、相互定义等相关的类序列。需要特别注意表示存储，并且在定义对象的演化时，我们必须考虑所有可能涉及它们的指针为了简单起见，我们首先只处理非二进制方法，即只接受一个类参数的二进制方法不能被简单地处理，因为它们在相应的函子中产生变量的逆变在[14]中已经考虑了将余代数范式扩展到混合函子，但是这样的扩展相当复杂，并且只覆盖了有限的情况。我们简要地勾勒了一种处理二进制方法的替代方法，基于将函数表示为图。这种方法在纯功能设置中是完全令人满意的。然而，在命令式设置中，二进制方法带来了我们简要触及的进一步问题。有趣的是，Fickle对象上的共代数等价导出了Fickle表达式上的拟代数等价，从而可以用来研究观测等价的概念。本文利用余代数等价研究了我们引入的上下文等价P这是关于给定程序P的Fickle表达式的等价，Fickle表达式被视为主方法的主体，即类定义的集合。两个主要的方法被等同当且仅当它们在任何上下文中具有相同的行为，w.r.t.给定程序P。概要。在第一节中，我们回顾了Fickle的语法和操作语义，并介绍了表达式（程序）上的观察等价性在第二节中，我们给出了Fickle规划的余代数描述，166F. Honsell et al. / Electronic Notes in Theoretical Computer Science 104（2004）163-⇓与诱导的行为等价。在2.1小节中，我们讨论二元方法。在第三节中，我们比较了前面介绍的表达式上的余代数等价和观测等价最后评论和未来工作的方向见第4节。致谢。作者感谢M。Dezani进行有益的讨论。1语言的变化无常在本节中，我们首先回顾语言Fickle的语法和操作语义（更多细节请参见[4]然后，我们将介绍我们将要研究的程序的观测等价性。1.1语法Fickle语法总结在表1中。Fickle程序是一个类定义（可能是抽象的）的集合。一个类定义可以在关键字state或root之前。状态类描述对象满足某些条件时的属性;当它不再满足这些条件时，它可以显式地重新分类到另一个状态类。根类抽象于状态类。虽然（状态）类由一系列字段和方法组成，但在抽象（根）类中，一些方法只能被声明。状态或根类的任何子类都必须是状态类。国家的对象类c可以重新分类为类cJ，其中cJ必须是C的唯一定义的根超类。 非状态、非根类的对象c的行为类似于Java对象，也就是说，它们永远不会被重新分类。字段的类型可以是布尔型或整数型，也可以是非状态类。因此，场不能被重新分类。相反，this和parameters的类型可以是状态或根类，即这些变量可以重新分类。然而，尽管这些限制对于定义一个健全的类型系统是重要的（见[4]），但它们对我们的目的来说并不是严格必要的。对象是用表达式newc创建的，其中c是任何类。重分类表达式id c将id的类设置为c，其中c必须是状态类。方法声明具有以下形状：t m（t1x1，.，t q x q）{c1，.，c n}{e}其中t是结果类型，t1，. ，t q是形 式 参 数 的类型x1，. ，x，q，e是身体。 根类c1，... ，c，n是效应，F. Honsell et al. / Electronic Notes in Theoretical Computer Science 104（2004）163-167------||||||||--−→r：= classclass：= [state]classcextendscfieldmeth类：=[root]classcextendsc场方法矩阵场：=类型fmeth：= type m（park）eemdecl：= type m（parl）e类型：= boolintcpar：= type xe：= cexpr（）e：=if ethen eelse evar：=ee;esVal这个变量新的c |e.m（e）|iddecF|fi|......你好。.X|y |z|......这是什么？表1善变的也就是说，可以通过调用该方法重新分类的所有对象的根类。为了简单起见，我们假设类中的所有字段都是私有的，即只能通过类方法从类外部访问。相反，我们将类中的所有方法都视为public。此外，我们假设在方法体中没有局部变量。在表1中，总结了Fickle语法，我们省略了布尔和整数表达式的语法，这涉及到标准运算符。最后，我们假设继承层次结构是一棵树，根类只扩展非根和非状态类，状态类扩展根类或状态类。对于Fickle程序的示例，我们参考[3，4]。1.2操作语义的操作语义给出的SOS“大步”的关系，重写对表达式和存储w.r.t.将程序P分成成对的值、异常或错误，并存储。被求值的表达式表示程序开始执行的特殊方法main（在P的外部）重写关系的类型为：−→：r→expr×store→（valdev）×store其中：varsValID：=：=：=X |e.F真正|虚假|null|0 |1.一、. .这|X使用以下约定CF：：=：：=C |C '|Ci|D|......这是什么？对于类名对于字段名MX：：=：：=M|M i|米伊杰|......这是什么？方法名称对于参数名称168F. Honsell et al. / Electronic Notes in Theoretical Computer Science 104（2004）163-.addrNatValsVal地址dev{nullPntrExc，stuckErr}对象c{[f1：v1，.，f r：v r] c| f1，.，f r∈fidc是c，v1，..，v r∈val}objectc objectcstore（{this}→addr）×（varid→p finnval）×（addr→pfinnobject），其中sVal在表1中定义，varid是变量标识符的集合，fidc是c的场标识符的集合，而→p finn表示具有有限域的部分函数的空间。注意，对象c的元素实际上是（fidc→pfinval）中的部分函数。特别地，存储是具有有限域的部分函数，将其映射到地址，将基类型的变量映射到值，将类类型的变量映射到地址，并将地址映射到对象。特别注意，在存储中，地址指向对象，但不指向其他地址。因此，在Fickle中，就像在Java中一样，指针是隐式的，没有指向指针的指针。我们用i表示地址，用σ表示存储，用v表示值，用o表示对象，用dv表示异常和错误。在介绍重写规则之前，我们需要定义一些对对象和存储的操作。对于对象o[f1：v1，...，f l：v l，. f r：v r] c，存储σ，值v，地址i，标识符或地址z，字段标识符f，我们定义：•场访问：o（f）v l如果f= f l对于某个l∈ 1，...，r，Udf否则•对象更新：o [v/f][f1：v1，.，f l：v，. fr：v r] c，其中f l= f，对于某个l∈1，.，r，•存储更新：σ[v/z]（z）=v，σ[v/z]（zJ）=σ（zJ），如果zJz。我们使用σ（i）（f）=Udf的约定，每当σ（i）=Udf时，即I/∈dom（σ）。表2和表3列出了操作语义的重写规则。由于空间不足，在表3中，一些规则被压缩在单个规则中（例如，参见第一条规则）。注意，表3中的规则是不确定的，但是常识告诉我们如何解决歧义。表达式newc在存储σ中的求值用一个新的规范地址扩展了σ。此外，新对象的所有字段都是用规范值初始化的，按照惯例，我们假设这些值为false和0，F. Honsell et al. / Electronic Notes in Theoretical Computer Science 104（2004）163-169CFF⇓∆≈如果t是状态类s，c是root，布尔型和整数型字段，类类型的字段为null。在new（和重新分类）规则中使用的函数FS是这样的，S（P，c）返回类c中定义的场的集合，而S（P，c，f），使用在重新分类的规则中，给出了类C中的场f的类型。在方法调用的规则中，e0.m（e1，.在表2中，我们使用函数M：M（P，c，m）返回通过类层次结构的类c中方法m的定义（更多细节请参见[4]）。此外，前提σ n（i）= […]意味着，在本发明中，ddressi指的是clas sc的对象。对于重分类表达式id d，我们找到id的地址，它指向类c的对象。我们用一个新的d类对象替换原来的对象。我们保留属于c的根超类的字段，并根据它们的类型初始化d的其他字段（如新表达式的情况）。R（P，t），定义为R（P，t）测试超类尽管如此，表示t的最小超类，如果t是一个类，它不是一个状态类，如果t不是一个类，它表示t本身1.3观察等效性Fickle程序上的各种观测等价性的概念是由操作语义学自然产生的。首先，我们可以在主方法上定义一个上下文等价一个给定的程序P，通过评估与任何表达式上下文C[ ]中的主方法体相对应上下文只是一个有无限多漏洞的表达式。作为可观察值，我们采用基本类型和错误/异常的值，即obsvalsValdev.其中（e，σ）Pu证明了存在σJ使得（e，σ）→P（u，σJ），其中u∈sValdev.定义1.1（上下文等效）：设Pexpr×expr定义为：ePeJ<$C[ ]<$σ <$u∈obsval. （C [e]，σ）Pu惠 （C [eJ]，σ）<$Pu.表达式e，eJ上的上下文等价P导出程序P与主体为表达式的主方法之间的一个主方法，它的主体是一个170F. Honsell et al. / Electronic Notes in Theoretical Computer Science 104（2004）163-F {}F∈{}−→∈{}c（e，σ）JJ−→P（true，σJJ）（e，σ）−→P（false，σJJ）（e1，σ）−→P（v，σJ）J（e2，σJJ）−→P（v，σJ）J（ifethene1elsee2，σ）−→P （v，σ）（ifethene1elsee2，σ）−→P（v，σ）（e，σ）−→P（i，σJJ）（eJ，σJJ）−→P（v，σJJJ）σ（x）/=UdfσJJJ（i）（f）Udf（e，σ）−→P（v，σJ）JσJσJJJ[σJJJ（i）[v/f]/i]（x：= e，σ）−→P （v，σ [v/x]）（e.f：= eJ，σ） −→P（v，σJ）（e1，σ）−→P（vJ，σJJ）（e，σ）−→P（i，σJ）（e2，σJJ）−→P（v，σJ）JσJ（i）（f）UDFJ J（e1; e2，σ）−→P（v，σ）（e.f，σ） −→P（σ（i）（f），σ）σ（id）=/Udf（id，σ）−→P（σ（id），σ）（v，σ）−→P（v，σ）S（P，c）=f1，...，frvl首字母（P，c，fl）（l1，.（r）i是σ（new c，σ）−→P（i，σ [[f1：v1，. ......、fr：vr] c/i]）（e0，σ）−→P （i，σ0）（ei，σi−1） P （vi，σi）（i 1，.，n）的σn（i）= [... . ]MJ（P，c，m）=tm（t1x1， . . ，tnxn）φ{e}σ = σn [1/this，v1/x1，...，vn/xn]（e，σJ）−→P（v，σJJ）JJ（e0.m（e1，.，en），σ） −→P（v，σ[this <$→σn（this），x1<$→σn（x1），.，xn<$→ σn（xn）]）σ（id）= 1σ（i）=[... . ]cFS（P，R（P，c））={f1，. 、.中，fr}vl = σ（i）（fl）（fl∈ {1，. r}）FS（P，d）\{f1，.， fr}={fr+1，. 、.中， fr+q}Jvl初始的FS（P，d，fl）（fl ∈ {r +1，. ......你好。r + q}）（id，σ）−→P（null，σ）（idd，σ）−→P （i，σ [[f1：v1，. .，fr+q：vr+q] d/i]） （idd，σ）−→P（null，σJ）表2操作语义学：无异常和错误是表达式EJ。注意，假设类中的所有字段都是私有的（参见1.1节），main方法只能通过类方法。特别地，在上面的定义1.1中，字段访问表达式既没有出现在表达式e，eJ中，也没有出现在上下文C[ ]中。在上述观测等价性的定义中，程序P是固定的。然而，在许多情况下，例如，在程序精化中，我们感兴趣的是在不同的程序P1，P2之间建立等价关系，它们实现了相同的程序规范。程序规范的一个简单概念可以被看作是一个没有字段的抽象类列表，只有一个方法声明序列。然后，程序P1实现了一个特定的程序，F. Honsell et al. / Electronic Notes in Theoretical Computer Science 104（2004）163-171J−→∈{}c（e，σ）−→P（null，σJ）（e.f：= eJ，σ）−→P （nullPntrExc，σJ）（e.f，σ）−→P（nullPntrExc，σJ）J（e，σ）−→P（v，σJ）（e.m（e1，.，en），σ） −→P（nullPntrExc，σ）v= true，v/= falseσ（x）= true或σ（x）= falseJ（ifethen e1elsee2，σ） −→P（stuckErr，σ）（x<$c，σ）−→P（stuckErr，σ）（e，σ）−→P（v，σJ）σ（x）=Udfv/=零v/∈addrJ（x，σ）−→P（stu ckErr，σ）（e. f，σ）−J→P （stu ckErr， σ）J（x：= e，σ） −→P（stuckErr，σ） （e.f：= e，σ）−→P（stuckErr，σ）（x<$c，σ）−→P（stuckErr，σ）（e0，σ）−→P （i，σ0）J（ei，σi−1）−→cP （vi，σi）（σi∈{1，. ，n}）（e，σ）−→P（i，σ）σn（i）= [. . ]σJ（i）（f）=UdfJM（P，c，m）=Udf（e.f，σ）−→P（stuckErr，σ）（e0.m（e1，.. .，en），σ）−→P（stuckErr，σn）（e0，σ）−→P（v，σ0）（e，σ）−→P （i，σJJ）v/= null（eJ，σJJ）−→P（v，σJ）v/∈addr或σ0（v）=UdfσJ（i）（f）=Udf（e0.m（e1，.，en），σ）−→P（stuckErr，σ0）（e.f：= eJ，σ）−→P（stuckErr，σJ）（e，σ） −→P（dv，σJ）或（（e，σ）−→P（true，σJJ）and（e1，σJJ）−→P（dv，σJ））or（（e，σ）−→P（false，σJJ）and（e2，σJJ）−→P（dv，σJ））（ifethene1elsee2，σ）−→P（dv，σ）（e1，σ）−→P（dv，σJ）或（（e1，σ）−→P（v，σJJ）and（e2，σJJ）−→P（dv，σJ））（e1;e2，σ）−→P（dv，σJ）J（e，σ）−→P（i，σJJ）（e，σ）−→P（dv，σ）J（eJ，σJJ）−J→P（dv，σJ）J（x：=e，σ）−→P（dv，σ）（e.f：=e，σ）−→P（dv，σ）（e.f，σ） −→P（dv，σJ）J（e.m（e1，.，e n），σ）−→P（dv，σ）（e.f：= eJ，σ）−→P（dv，σJ）（e0，σ）−→P（i，σ0）（e i，σ i−1）−→P（v i，σ i）（i∈ {1，.，q}，q< n）（e q+1，σ q） −→P（dv，σ q+1）（e0.m（e1，.，e n），σ）−→P（dv，σ q+1）（e0，σ）−→P（i，σ0）（e i，σ i−1）P（v i，σ i）（i1，.得双曲正切值.σ n（i）= [... . ]MJ（P，c，m）=tm（t1x1， . . ，tn：xn）φ{e}σ = σ n [i/this，v1/x1，...，v n/x n]（e，σJ） −→P（dv，σJJ）JJ（e0.m（e1，.，e n），σ）−→P（dv，σ [σ n（this）/this，σ n（x1）/x1，.，σ n（x n）/x n]）表3操作语义：异常和错误的生成和传播172F. Honsell et al. / Electronic Notes in Theoretical Computer Science 104（2004）163-∆≈当P1的每个类中的方法声明与P中的方法声明完全对应时，人们可以考虑一个更复杂的程序规范概念，涉及一阶逻辑来表达字段上的条件。这对于研究程序的优化是很有用的。通过示例，我们引入以下简单等价。两个程序P1，P2，实现了相同的程序规范P，可以被认为是等价的，当对于任何可能的主方法，它们的值相同时：定义1.2设P1，P2实现相同的程序规范P.我们通过以下方式定义等价性：P1P2双金属 e（e，）P1u惠 （e，n）nP2u.由于篇幅有限，本文将只关注上下文等价P，而不研究定义1.2的程序等价。我们只是指出，我们在下一节中给出的Fickle对象的共代数描述也引出了共代数程序等价的概念，这与程序等价进行比较会很有趣。2易变对象和程序的余代数描述在本节中，我们给出了一个共代数帐户的Fickle对象（和程序）的片段Fickle组成的一元方法，即方法，不采取一个以上的对象参数。在[13，9]之后，我们将类建模为余代数，其中载体表示类的对象，余代数结构由方法的操作语义确定。余代数结构捕捉对象在方法作用下的演化。为了在命令式设置中对对象的演化进行建模，我们还需要考虑存储中地址的共享和变量的别名。我们的共代数模型自然地导出了程序P的对象上的共归纳等价，我们将在第3节中使用它来研究上下文在定义1.1中引入了等价性。最后，我们简要地讨论了二元方法的一般情况。这些都是有问题的处理，因为他们产生逆变出现的参数在函子建模的程序。我们提出了两种可能的方法，为了把逆变发生的协变的。第一种是“冻结”X对载体的F. Honsell et al. / Electronic Notes in Theoretical Computer Science 104（2004）163-173{}∈余代数第二个是将二进制方法表示为图而不是函数。在适当的条件下，这两种方法是一致的。此外，为了说明对象在二进制方法下的行为，我们需要扩展原来的方法，不仅描述对象在应用其类的方法下的行为，而且还描述在应用程序中使用此类对象作为参数的任何其他二进制方法下最后，在处理命令式设置中的二进制方法时，我们需要注意对象参数引用值的可能不一致性我们首先定义类c的命令对象的表示。定 义 2.1 设 refobjectc 是 对 （ i ， O ） 的 集 合 ， 其 中 i∈addr ， O∈（addr→pfinobject）是最小闭函数，即，n∈ range（O）。i∈ range（o）。i∈ dom（O）-，使得i∈ dom（O）且O（i）∈对象c。本质上，当我们不考虑环境部分时，refobject可以被视为由地址诱导的最小在下文中，我们简单地用O表示c refobject c的元素（i，O）。在介绍我们的共代数语义之前，我们需要定义refobject和store之间的一致性概念，用refobject更新store的概念，以及由store中的地址诱导的refobject的概念定义2.2令σ∈store，O∈refobjectc，i∈addr。i) O和σ是一致的，记为con（O，σ），如果对于所有地址，i∈dom（O），如果i∈dom（σ），则O（i）=σ（i）。ii) 对于O和σconsistent，并且x∈id，我们定义σ[O/x]存储σ，其中对应于refobject O的对象已经与x相关联，并且存储的其余部分，如果必要的话，已经根据O更新。iii) 设I dom（σ）。 我们用σ（i）表示包含在σ中的唯一refobject（i，O）。设xvarid这个 我们用σ（x）表示σ（x）本身，如果x有基类型， 包含在σ中的唯一refobject（σ（x），O），否则。现在我们介绍由一元方法组成的Fickle片段的余代数描述为此目的，我们赋予一个给定的程序P的refobjects的集合与一个余代数结构的函子诱导的方法在P。一种方法t0m（t1x1，.，t q x q）在P中，当对一个对象和一个实际参数列表一起调用时，可以终止（成功或异常/错误），产生一个可能修改的对象，或者不终止。方法在对象上的行为决定了共代数结构：定义2.3设Pc1，.，c n，其中c i{f i1;. fhi; m i1;. ;miki}.174F. Honsell et al. / Electronic Notes in Theoretical Computer Science 104（2004）163-⎧⎪⎨⎪∗∅P如果e是mij的body，且我 Ji) 设F：Set→Set定义为：F菲，其中Fij：Set→Set由方法声明确定t0m ij（t1x1， . . ，tqxq）{cJ1， . . ，cJp}ci类如下：F ij X[[t1]] ×. ×[[tq]]→（（[[t0]]+dev）×X+1），其中，对于所有i = 0，.，q，[[ti]]=boolifti =boolintifti =int请将其他地址发送给我们。F ij在箭头上的定义是规范的。ii) 让我们用refobjectP简单地表示cirefobjectci。设αP：refobjectP→F（refobjectP）定义为：αP[j]i，当reαij：refobject ci→Fij（ckJ∈Cijrefobject cJk）时，对于方法mij可以重新分类对象的类别的Cij个集合αij（O）a›→（e，<$[O/this，a/x]）−→P（u，σ1）不过，哪里 表示1的唯一元素。 请注意，商店 [O/this，a/x]总是有定义的（即没有一致性问题），因为所有的实际参数都是基类型。iii) 设[ ]F：（refobject，αP）→（refF，αP）为余代数语义，即PF唯一的F-余代数态射到最终的F-余代数。应用余代数语义学的一般理论，我们得到了[]F诱导的等价的如下余归纳刻画：PF. Honsell et al. / Electronic Notes in Theoretical Computer Science 104（2004）163-175PPPP∼PPPProposition 2.4coalgebraic semantic[[]]F诱导以下内容-P的对象上的等价：对所有O，OJ∈refobjectc，其中c是P的一个类OFO将方法m（x）在c中与主体e结合，将参数a的列表与x结合，（e，<$[O/this，a/x]）−→P（u，σ1）<$（e，<$[OJ/this，a/x]）−→P（u，σ1J） ∧σ1（this）<$Fσ1J（this），andc.推论2.5F是下列单调函数的最大不动点（w.r.t. 子集包含）操作符：Φ（R）{（O，OJ）|m（x）：c中的e，x的参数列表a，（e，<$[O/this，a/x]）−→P（u，σ1） <$（e，<$[OJ/this，a/x]）−→P（u，σ1J） ∧σ1（this）Rσ1J（this），和c_（？）换句话说，下面的共归纳原理是合理的并完成：OROj R是Φ-互模拟，OFOJ其中Φ-互模拟R是关系s.t. R Φ（R）.例2.6i）设Register是一个类，只有一个字段包含寄存器的整数值，以及两个方法，getval和setval。第一个方法返回寄存器的内容，第二个方法将内容设置为作为参数传递的新值，并返回新值。可以很容易地检查对象类Register上的共代数等价当且仅当它们具有相同的内容时才等于两个寄存器。ii) 设IntList是一个表示可能是整数循环列表的类。IntList类有两个字段，分别表示列表的头和尾，即分别包含一个整数值和一个列表，还有两个方法，分别返回列表的头和尾。然后IntList上的共代数等价等价等价当且仅当两个列表在头部具有相同的值并且在尾部具有相同的地址。iii) 为了恢复列表上的扩展等价，可以定义IntList类，只考虑一个方法，取整数n作为参数，返回列表中第n个元素的值。余代数等价于在最小存储中，对于所有参数列表，在方法应用下以相同方式行为的对象。实际上，商店最小化是不相关的。也就是说，如果我们假设表达式newc不出现在类方法的主体中，我们可以很容易地证明对象的行为只取决于方法参数，而不取决于存储的其余部分。然而，我们推测，176F. Honsell et al. / Electronic Notes in Theoretical Computer Science 104（2004）163-PPPPPPPPPPPP× → ××上述假设可以排除。无论如何，我们觉得这不是一个强有力的假设，因为通常类方法用于访问或修改对象，而新对象的创建是在main方法中执行的此外，在下文中，我们还默认，如果两个对象如果一个根类d的正则扩展（通过重新分类）是等价的，那么它们对一个状态子类c的对象的正则扩展仍然是等价的。这意味着在子类c中，没有额外的方法仅根据超类d中的场进行区分。这是一个相当自然的假设，对于处理重新分类是必要的因此，我们有：引理2.7OFO在c中的带体e的迭代方法m（x），con（O，σ）con（OJ，σ），（e，σ[O/this]）−→P（u，σ1）<$（e，σ[OJ/this]）−→P（u，σ1J）<$σ1（this）<$Fσ1J（this），反之亦然。等价性 on refobjects自然会导出一个等价的onstores，如果我们把所有变量的stores都取为等价：定义2.8我们定义∆σFσJ⇐⇒ <$x∈id. σ（x）<$FσJ（x）.对象行为只依赖于方法参数这一事实的另一个直接后果是，如果两个对象是等价的，那么它们在应用等价的方法时的行为是相同的。产品参数：引理2.9OFOm（x）：e in c， σJ<$con（O，σ）<$con（OJ，σJ），（e，σ[O/this]）−→P（u，σ1）<$（e，σJ[OJ/this]）−→P（u，σ1J）<$σ1（this）<$Fσ1J（this），andc.2.1二元方法如果定义2.3中的方法mij是二元的，那么很明显函子Fij（因此F）不是协变的。二元方法的一个例子是equal：c×c→bool方法，它将类的另一个实例作为参数。c的第二次出现产生X在FX...（X）（（bool + dev）X）+1）因此，并不直接适用于这种情况。F. Honsell et al. / Electronic Notes in Theoretical Computer Science 104（2004）163-177将函子F中的逆变出现转化为协变出现的第一个解决方案是将X的逆变出现“冻结”到余代数的载体refobject P上例如，在方法equal的情况下，我们可以取GX... ×（refobject P→（（bool + dev）×X）+ 1）×. .另一种方法是将二进制方法建模为图而不是函数，方法是用幂集函子代替函数空间。在方法相等的情况下，这将对应于取HX. ×P（X×（（bool +dev）×X）+ 1）×... .此外，在这两种情况下，为了正确地描述对象在二元方法应用下的行为，我们需要扩展原来的共代数方法，并在函子的定义中考虑可能不同类的（二元）方法，对象作为参数提供给它们。否则我们就失去了引理2.9的类似物。也就是说，让我们考虑下面的平凡反例。设A是一个只有一个bool类型字段的类，并且只有一个（二进制）方法m将类A的另一个对象作为参数，并返回该参数的字段的值。那么A的所有对象都是余代数等价的，如果我们不考虑对象的行为作为m的（普通）参数。然而，方法m应用于同一个对象，加上域中具有不同值的参数，会给出不等价的结果。一般来说，G诱导的等价包含在H诱导的等价中，但反之则不然。为了使这两种方法与“预期逆变”等价一致，必须补偿一元方法的“可粗略地说，必须在类中添加足够数量的一元方法，以允许观察二元方法使用的所有字段。因此，共代数等价仅由一元方法确定。该程序在功能设置中运行顺利[8]。然而，在我们的命令式设置中，二进制方法引起了对象O和其他对象参数之间可能不一致的额外问题特别地，如果我们考虑一元方法的共代数语义到二元方法的自然扩展，我们得到一个对象等价，它在地址的基础上进行区分，无论是在冻结函子G的情况下还是在图函子H的情况下。也就是说，让我们专注于冻结，让我们考虑例2.6中的类Register，它扩展了二进制方法add，该方法将两个寄存器的内容相加。然后，当我们将方法add应用于与以下参数一致的寄存器参数时，方法add区分具有不同地址但内容相同的例如，第一个寄存器，而不是第二个寄存器。为了克服这个问题，可以通过测试行为来178F. Honsell et al. / Electronic Notes in Theoretical Computer Science 104（2004）163-CUPPPCUPCUPCUP）：CUP≈方法应用下的对象的参数与两个对象一致。然而，有点令人惊讶的是，这通常不是一个传递关系。上述传递性问题的一个可能的解决方案再次在于补偿一元方法的可观测性缺陷。然而，这值得进一步研究，我们离开它作为一个开放的问题，如何在一般情况下给一个共代数描述的变化无常的对象。3程序图上的余代数等价和观测等价在本节中，我们引入表达式w.r.t.的等价性概念一程序P，.这是由对象上的余代数等价导出的.第二节的第二节，我们简要讨论了CNOP和第1.3节的上下文对等性从现在起，我们将等价性<$F简单地表示为<$P。前一节中介绍的对象上的余代数等价自然地引出了表示主要方法主体的表达式上的等价概念w.r.t.给定程序P.两种主要的方法是等效的w.r.t. P，当对任何一种存储，它们产生相等的值和相等的存储时：定义3.1Let. Eexpr×expr定义为：e.J≈Pe ⇐⇒好吧（（e，σ）→P（u，σ1）=<$（eJ，σ）→P（uJ，σ1J）<$u<$PuJ<$σ1<$Pσ1J），反之亦然，其中u是u，如果u∈sValdev，它是σ1（u），如果u∈addr。即：我们推测。足够的w.r.t.语境等价物CUP，猜想3.2（的不确定性）.好吧普雷普山口的完整性。因为在上下文对等中，无法观察到由新表达式生成的不同地址例如，如果程序P中的类c是s. t。 只有具有相同地址的对象是等价的，那么表达式ex：= newc和eJx：=newc;x：=newc不相等。P-E Qui vale nt. 但是，没有什么分离它们的上下文，因为在观测等价P中，我们只观察基本类型的值。尽管如此，我们仍然可以得到不包含新表达式的受限表达式集F. Honsell et al. /