URL：http://www.elsevier.nl/locate/entcs/volume 19. html20页s互模拟与隐代数奥维迪乌·格奥尔基和阿德里亚娜·阿佩特里都是我的朋友a大学“A. I. Cuza”FacultyofComputerScienceB erth e lot 16，660 0 - I a Bagrisi，Romania电子邮件：{dlucanu，ogh，adrianaa}@ infoiasi.ro摘要隐代数是余代数的一个特例。一个隐代数上的隐同余对应于对应的余代数上的互模拟等价。本文将隐同余的概念推广到两个不同的隐代数之间的隐双模拟。我们首先定义了两个具有相同签名的隐藏代数之间的隐藏互模拟。隐互模拟实际上是对应的余代数之间的互模拟。然后，我们定义了两个隐藏代数之间的隐藏模拟，这两个隐藏代数具有由垂直签名态射相关的不同签名。我们更喜欢称之为关系模拟，因为它是单向的，由于签名态射。对于最后一种情况，讨论了模拟和细化之间的关系。1介绍通用代数在抽象数据类型建模中的使用具有可重复性，在某种意义上，数据类型的元素是通过构造器操作生成的。这里的重点是初始代数和自由代数，它们为数据类型提供了合适的表示。它对多序代数[14]和序序代数的优美而自然的推广[8]加上它易于处理的等式逻辑，使得泛代数适合于基于等式逻辑的规范语言的语义。余代数，作为代数的对偶概念，被证明适合于处理有限数据类型和一般的动态系统[19，18]，特别是对象[11，16]。这里的重点是通过析构函数操作来观察系统状态。final和cofree余代数分别与初始和自由代数对偶，并提供适当的行为表示因为它们包含了可能的行为。隐代数[5，6]结合了代数和余代数的概念，从某种意义上说，它的语法是许多排序代数语法的限制版本，它的语义是余代数。 隐代数是非常恰当的1999年由ElsevierScienceB. V. 操作访问和C CB Y-NC-ND许可证。2一个C→一个C要对对象建模，请执行以下操作：共代数语义提供对象的观察方面，而代数语法提供对对象的状态的（有限的）访问。隐代数的余代数性质在[12]中已经观察到，在[2]中得到了进一步的研究。然而，据我们所知，这种关系的全面阐述并不存在。例如，互模拟关系的唯一对应者是行为等价。但双模拟可以定义在两个不同的余代数之间，而行为等价则定义在单个隐代数上。在本文中，我们定义了隐藏-将两个不同的隐代数之间的互模拟作为余代数之间互模拟的对应.此外，如果φ：A → C是一个抽象隐规范的精化，具体的隐藏规格，Aan-模型和AJa-模型之间存在互模拟和J。这一点可以用隐藏互模拟来清楚地说明。从形式上讲，任何隐签名A对应于函子GA，使得任何隐A-代数A都可以看作GA-余代数Ac。A上的隐藏（行为）同余现在是Ac上的互模拟等价。两个隐代数A和AJ之间的隐互模拟实际上是对应的余代数Ac和Ajc之间的互模拟.我们还指出如何可以使用共归纳来证明两个状态是双相似的。隐藏互模拟的概念可以被定义，即使A和AJ有不同的签名，比如说A和AJ，但是它们通过垂直签名态射φ：A jJ相关。 这种关系称为φ-模拟，它也是余代数Ac和（AJφ）c之间的互模拟。我们给出了一个充分的条件，在此条件下，φ-模拟隐含了一个限制于可达模型的类钢筋性质。 问题找到一个充分必要的条件，在此条件下，φ-模拟等价于一个细化仍然是开放的。本文件的结构如下。第二节在简要介绍了隐代数和余代数的基础上，详细讨论了隐代数的余代数性质。由于本文中的所有示例都是用CafeOBJ编写的，因此本节还简要介绍了这种语言。第三节是本文的主要结果，它使隐代数的余代数性质得到更好的利用。定义了隐互模拟、φ-模拟，讨论了它们之间φ-模拟和细化。 一系列的例子表明，所有这些关系-在CafeOBJ等特定语言中处理。最后，第4节总结了结果，并概述了未来的工作。2预赛2.1隐藏代数一个可见的数据论域（V，n，D）由一个可见的分类集合V、一个签名（V，n）和一个n-代数D组成，使得对于每个d∈Dv，v∈V，3→{}∈隐藏签名（在（V，N，D）上）是一对（H，N），使得（V，N，N）是一个多排序签名，满足：(S1)若w∈V，v∈V，则有n_w，v= n_w，v;(S2)对每个σ∈εw，s中至多有一个w的元素在H中。H中的元素称为隐藏排序。我们通常只写（H，）和S为HV。一个隐藏的签名态射φ：f→ fJ是一个签名态射φ=（f，g）：f → fJ使得：(M1)f（v）=v，对所有v∈V;（M2）f（H）<$HJ;(M3)g（n）=n，对于所有n∈n;（M4）若σJ∈ΣJwJ，SJ且some_ort_inwJ位于sinf（H），则对于some_e，nσJ=g（σ）σ∈Σ。只满足条件M1-3的签名态射称为垂直签名态射我们经常把f（s）写成φ（s），把g（σ）写成φ（σ）。一个隐藏的（H，H）-代数是一个A-代数A，使得AH= D，其中AH是一个A-代数，忽略了在H中的排序和运算，而不是在H中。更一般地，给定一个签名态射φ：Aj φ J和一个Aj-代数AJ，我们可以定义AJφ，称为AJ到Aj的约化，通过设置（AJφ）s= AJφ（s）对于s∈S和（AJφ）σ= AJφ（σ）对于σ∈ Aj。 一个隐藏的n-同态h：A→AJ是一个n-同态使得hn= 1D. 一个隐藏的（行为）同余在隐藏的λ-代数A是λ-同余，这是平等的可见类。我们用HAlg表示所有隐代数的范畴。给定一个隐藏签名（H，H）和一个隐藏排序h，h是一个可见的排序的n-项c，它有一个排序为h的新变量符号z;我们经常写c[z：h]，或者如果h被理解了，就写c[z]。如果t的排序与z的排序匹配，则上下文c[z]适合于项t。C[z]表示使用变量z的上下文的V索引集合。一个隐代数A在行为上满足一个代数方程（X）t = tJ，记为A|对于所有适当的上下文c∈C<$[z]，我们有A|=（X）c [t] = c [tJ]。A在行为上满足条件方程e，形式（X）t=tJift1=tJ1， . . ，tm=tJm，writtenA|对不起，我为每一个人道歉赋值：X → A，对于所有适当的上下文c，我们有（c [t]）=（c [tJ]），其中ver（cj[tj]）=（cj[tJj ]），j=1， . . ，n，并且对于所有适当的上下文c，j，nd。如果从上下文中理解，我们经常省略下标“”。一个n（X）-项是局部的，它在D或X中。如果所有可见的有序真子项要么在D中，要么在X中，则一个X（X）-项是局部的。一个上下文是局部的，它是一个局部的n（z）-项。我们用L[z]表示使用变量z的局部上下文的V-索引集。隐藏满意度的定义上面的可以重新表述，以便它使用更小的上下文类别，即局部上下文（[7]中的命题19如果c[z：h]是4L∈[z]且da∈Ah，则nAc（a）=nAc（c），其中ea定义为dya（z）=a。如果a，aJ∈Ah，h∈H，那么我们说a和aJ在行为上等价i <$Ac（a）= Ac（aJ），对于所有局部上下文c。我们用A表示A上的行为等价关系（A是可见排序上的相等）。以下结果这是众所周知的（参见[6]）。命题2.1 A是A上的最大隐同余。一个隐藏的（或行为的）规范是一个三元组（H，E，E），其中（H，E）是一个隐藏的签名，E是一组E-方程。一个隐规范SP=（H，H，E）的模型是一个隐代数，它在行为上满足E中的所有方程。这样的模型被称为隐（E，E）-代数。我们记为HAlg，E是HAlg的满子范畴，其对象是隐（，E）-代数。如果SP =（H，N，E）是一个隐藏的规范，那么SP上的行为等价关系是：如果t和tJ是（相同的）可见类，那么t <$SPtJi <$E|如果t和tJ属于（相同的）隐藏排序h，则t <$SPtJi <$E|c [t] = c [tJ]对于所有的c∈L<$[z：h].很容易看出，如果A是一个SP-模型，并且t∈SPtJ，然后AtAtJ。设SP=（H，H，E）是一个隐藏的规范。对于每个上下文c（适当的排序），定义一个背景项i，存在某个d∈D，使得E|c = d;否则，我们说t是unfined。SP是词汇的，但所有的基础术语都有定义。如果至少有一个模型，则SP是一致的。下面的结果是[7]中的定理37。定理2.2SP有一个初始模型，它是相容的和词法的。隐排序代数在以下意义上被用作对象范例的基础：• 对象的状态通过隐藏排序来建模• 数据通过可见的分类建模;• 属性（对对象的观察）通过状态为一元的可见分类的操作来建模;• 方法（改变对象的状态）通过状态为一元的隐藏排序的操作来因此，一个运算σ∈n_w，s，其中w包含一个隐排序，如果s∈H，则称为方法，如果s∈V，则称为属性。 若w∈V∈H，s∈H，则σ∈V ∈w， s称为广义隐常数.2.2余代数给定一个范畴C和一个闭函子G：C→C，一个G-余代数由一个对象A和一个态射α：A→GA组成.余代数的一个同态5→⊆×∈→∈从（A，α）到（B，β）是C中的态射h：AB，它保持了余代数结构，即，h;β=α;Gh.这个方程对应于下图的交换性：AhBα β❄ ❄Gh余代数（A，α）和（B，β）之间的互模拟是一个关系R A B，它保持了余代数结构，即，存在一个余代数（R，ρ）使得下图可交换：Aπ0Rπ1Bα ρ β❄ ❄ ❄GAGπ0Gπ1其中π0和π1是投影。通过同态图给出互模拟的一个例子互模拟等价是一种互模拟，它也是一种等价关系。（A，α）和（B，β）之间的互模拟族的联合因此，（A，α）和（B，β）之间的最大互模拟，记为A，B，存在，它是所有（A，α）和（B，β）之间的互模拟。 我们只把A写为A，A。2.3隐排序代数与余代数本小节主要讨论隐代数的余代数性质。本文以[12，2]为基础。主要目的是提供适当的工具，使我们能够在这两种方法之间导航设（H，H）是（V，H，D）上的一个隐排序签名 设HSetS表示其对象是S-排序集A的范畴，使得Av=Dv，v∈ V，其箭头是S-排序函数f =（fs：As→ Bs|s ∈ S），使得对于所有v V，fv=1 Dv，并且令G：HSetSHSetS表示由下式定义的对象上的函子：（G<$A）v=Av=Dv对于每个v V，（GA）h=σ∈hw，sw∈V，s∈S[Dw→As]对于每个h∈H，假设每个操作的唯一隐藏排序参数σ是它的第一个参数。（G<$A）h中的元素γ记为（γ.σ：Dw→As|σ ∈6σ→Cs，w∈V，s∈S）。 我们经常使用较短的符号（γ.σ |σ ∈ Σ）。如果f=（fs：As→ Bs|s ∈ S）是HSet S中的箭头，则Gf定义为：• （Gf）v= idDv，其中v在V中，并且• （Gf）h（（γ.σ|σ∈ f））=（γ.σ; f |σ∈ φ），对h在H中.我们用CoAlg表示G-余代数的范畴引理2.3如果A是一个隐代数，则存在一个G的余代数Ac=（A，α），使得α（a）.σ（d）=Aσ（a，d）对任意的a∈Ah，d∈Dw，σ ∈ Hw，s，h∈H，s∈ S.注2.4如果Go是通过去掉一般化的隐藏常数从G得到的签名，则函子Go和Go是相同的。因此，一个隐代数A和一个约简A的余代数是相同推论2.5假设n不包含广义隐常数。若（A，α）是G的一个余代数，则存在一个隐余代数Aa，使得Aa（a，d）=α（a）.σ（d）对任意的a∈Ah，d∈Dw，σ ∈ Hw，s，h∈H，s∈ S.注2.6设G是一个任意签名，（A，α）是G的一个余代数.由于每个局部上下文c[z：h]不包含隐藏常数，所以定义Ac使得对于任何隐藏的代数AJ使得AJc=A，我们有AJc（a）=Ac（a），对于所有在Ah中的a。Ac（a）也可以通过对c的结构归纳来定义。引理2.7设A和AJ是两个隐代数. H集S中的态射h：A → AJ是隐G-余代数i的同态，它是G-余代数i的同态.证据 设Ac=（A，α）且AJc=（AJ，αJ）。设h：AIJ是隐代数的同态.然后（a，σ，d）h（Aσ（a，d））=AJσ（h（a），d）（αa，σ，d）h（α（a）.σ（d））= αJ（h（a））.σ（d）<$$>（αa）G<$h（ α （ a ） ） = αJ （ h （ a ） ）<$$>α; G<$h = h; αJ.最后一个方程说h是余代数的同态。✷推论2.8如果HAlg和CoAlg不包含广义隐常数，则HAlg和CoAlg同构。上述结果与[2]中的命题2完全相同。引理2.9设A是一个隐代数。如果R<$A×A是一个隐同余，则它是A上的互模拟等价。7证据设Ac=（A，α），定义函数ρ：R→G<$R为（a0，a1）<$→（（α（a0），α（a1））.σ |σ ∈ R），其中（α（a0），α（a1））.σ：Dw→ RsAs×Bs由（α（a0），α（a1））.σ（d）=（α（a0）.σ（d），α（a1）.σ（d））给出.然后G<$πi（ρ（a0，a1））={ρ的定义}G<$πi（（α（a0），α（a1））.σ|σ∈ π）={G的定义}（（α（a0），α（a1））.σ; πi|σ∈ Σ）= {ρ的定义}（α（ai）.σ|σ∈ Σ）=（πi;α）（a0，a1）对于i= 0， 1，这说明R是G互模拟。✷利用这些载体可以构造一个最终的G-余代数Zh=v∈V[L[z：h]v→Dv]若p∈Zh则p =（pv：L<$[z：h] v→Dv|v∈V）。 最终余代数Z→G<$Z定义如下：如果σ∈Hw，s，s∈S，则• 如果s=v∈V，则σ（d）=pv（σ（z：h，d））对于所有d∈Dw，且•如果s=hJ∈H，则σ（d）=（pJv：L<$[z：hJ] →Dv|pJv（c [z]）= pv（c [σ（z，d）]），v∈V）对所有d∈ Dw.对任意G的余代数α：A→G<$A，唯一同态A→Z将a ∈ Ah映射到（av：L<$[z：h] v→ Dv|av（c）= Ac（a），c ∈ L<$[z：h]，v∈ V）.引理2.10设Z是最终G余代数。 则Zc（p）= pv（c），p∈Zh，c∈L<$[z：h] v，v∈V.证据我们通过深度（c）的归纳进行。若c = σ（z：h，d），则Zc（p）=∑p（c）=∑p（σ（z，d））=Zσ（z，d）=pv（σ（z，d）），对所有p∈Zh.证明了c = CJ [σ（z：h，d）]，CJ∈L<$[zJ：HJ].如果p在Zh中，则Zc（p）=p（cJ[σ（z，d）]）=p（cJ）[p（σ（z，d））]=ZcJ（Zσ（p，d））=ZcJ（pJ）=pJv（cJ）=Zσ（p，d）v（cJ）=pv（CJ [σ（z，d）]）= pv（c）.8其中pJ是Zσ（p，d）的临时符号，ZcJ（pJ）=pJv（cJ）通过应用归纳假设得出。✷我们经常写Z为对应于隐藏签名的最终余代数。9∼→∼∼a ca一一一一ΣΣΣ命题2.11设A是一个隐代数。 然后A是最大的G相互模拟等价证据引理2.9证明了BRA是一个互模拟。 所以我们只需要证明A是最大的互模拟。设fA是唯一同态AcZ.很容易检验A是f A的核。这个定理的结论现在由定理9.3 [19]得出。✷注2.12这里给出的最终余代数的构造等价于最终隐代数Fo的 构 造（例如，见[7，6]）。更准确地说，我们有Z = Fo和Z= F o（Z看作一个代数）。如果A是一个隐代数，则用ZA表示ZA的最小子余代数，它（1）（<$c∈L<$[z：h]， d∈Dw）Ac（Aσ（d））=ACJ（AσJ（d））对每个隐常数σ：w→h，余代数FAJ：Ajc→Z的唯一同态对Ajc的象位于ZA中.引理2.13非线性代数Za是一个代数。证据Za通过（Za）σ（d）=fA（Aσ（d））解释隐藏常数σ：w→h对所有d∈Dw，其中fA是余代数fA的唯一同态：Ac→Zc。 注意，（Za）σ（d）由等式（1）很好地定义。✷2.4CafeOBJCafeOBJ[1，15，4]是一种多范式代数规范语言，目前正在日本开发。CafeOBJ 的 指 称 语 义 基 于 几 种 逻 辑 的 组 合 ， 包 括 MSA 、 顺 序 代 数（OSA）、HSA和重写逻辑（RWL）。CafeOBJ是OBJ的继承者，所以它的语法类似于OBJ[9]。这里有一些细节。有两种类型的模块，分别对应于初始和松散的语义。定义初始语义的关键字是mod！而定义松散语义的则是mod*。可见排序用[ ]声明，隐藏排序用 *[ ]* 声明。属性和方法的声明使用关键字bop（来自行为操作）。CafeOBJ是可执行的。它的操作语义是基于重写的，可以用来证明系统的性质。在演算证明中使用的主要策略是归纳法和余归纳法[6]。我们考虑一个不可靠的缓冲器的CafeOBJ规范作为例子：1mod* DATA{[Data]OP nothing：->数据}[1]在[10]中可以找到不可靠布尔代数余代数化的一个版本10mod*UB{protecting（DATA）*[Ub]*bop write： Ub Data -> Ubbop read： Ub -> Databop空的？：Ub -> Bool varB： Ubvar D：数据ceq read（write（B，D））= Dif not empty？（写（B，D））。ceq read（B）=如果为空，则无内容？(B) .}模块DATA由一个可见排序的声明组成它的语义由所有集合组成。为了我们的目的，DATA提供了数据宇宙。模块UB以面向对象的方式指定不可靠的缓冲器。它导入数据域DATA，并由一个隐藏排序Ub、一个方法write唯一的等式，和一个空的确认属性？2缓冲器是不可靠的，也就是说，它具有可能丢失数据的“属性”。属性为空？ 返回truei表示缓冲器丢失了存储在其中的最后数据。我们没有关于缓冲器如何丢失数据的信息。这样的缓冲器是公平的，如果不存在缓冲器丢失所有写入数据的连续写入的无限序列，按顺序排列一个非常特殊的公平不可靠的缓冲器的例子如下：mod*UB1{protecting（DATA）*[Ub1]*操作初始化1：->Ub 1op write：Ub1 Data -> Ub1 {coherent}bop read：Ub1-> Databop空的？：Ub1 -> Boolvar B： Ub1var D：数据ceq read（write（B，D））= Dif not empty？（写（B，D））。ceq read（B）=如果为空，则无内容？(B) .eq为空？（init1）= true。eq为空？（write（B，D））=不为空？(B).}模块UB1指定了一个不可靠的缓冲器，其中“丢失的写入”和“安全写入”交替。定义了UB12布尔值自动导入到任何模块中。11∼∼由BUB1BJi空？（B）=空？（BJ）和read（B）=read（BJ）。write操作的coherent属性声明此操作满足BUB1BJ意味着write（B，D）UB1write（BJ，D）。通过应用句法一致性标准[17]，可以得出write的连贯性。 关于CafeOBJ中的相干操作的更多信息可以在[3]中找到。3隐代数在这一节中，我们首先定义两个隐代数之间的隐互模拟，并解释如何使用余归纳来证明两个状态是双相似的。一个例子展示了如何在CafeOBJ这样的特定语言中处理隐藏的互模拟。然后我们将隐互模拟推广到一个隐代数A和一个隐代数AJ之间的φ-模拟，假设存在垂直签名态射φ：φ→ φJ。 再举一个例子显示了CafeOBJ中如何处理φ模拟。本节最后讨论了φ-模拟和细化之间的关系。我们给出了一个充分的条件，在此条件下，φ-模拟证明了φ是一个加细。找到一个必要和充分条件的问题仍然是开放的。所有在数据全域（V，N，D）上考虑隐藏签名。定义3.1设A和AJ是两个隐代数。关系RA×AJ是A和AJi之间的隐藏互模拟(i) R是可见排序上的相等，(ii) aRhaj蕴涵Aσ（a，d）RAJσ（AJ，d），对所有σ∈Hw，s，d∈ Dw.注3.2很容易看出，如果A=Aj，则R是一个隐互模拟i，它是一个隐同余。引理3.3若R是隐代数A之间的隐互模拟和Aj，则R是余代数Ac和AJc之间的互模拟。证据 类似于引理2.9。✷定义3.4设A和AJ是两个隐代数。则A，AJ由下式给出：A，AJ在可见排序上是相等的，如果a和aJ是隐藏排序h，则A AA，AJaJi <$Ac（a）= AJc（aJ）对于排序h的所有局部上下文c。定理3.5A，AJ是隐藏的n-代数A和AJ.证据我们将首先证明，A，AJ是一个隐藏的互模拟。A，AJ是定义上可见排序的相等。设a，aJ是h类，使得a∈A，AJaJ.对于所有的σ∈hw，s，我们有以下情况：1. s=v，其中v是可见排序。 则σ（z：h，d）是a的局部上下文，12∼ ∼∼∼∼aJ所以aA，AJajAσ（z：h，d）（a）=AJσ（z：h，d）（aJ）Aσ（a，d）=AσJ（aJ，d）Aσ（a，d）<$A，AJAσJ（aJ，d）.2. s=hJ，其中hJ是隐藏排序。然后aA，AJaj（<$c∈L<$[z：h]）Ac（a）=AJc（aJ）<$（（Aσ（a，d）<$A，AJAJσ（aJ，d）.所以，我不知道你在说什么A ，AJaJ表示Aσ（a，d）A ，AJAσJ（aJ，d）anddhence A ，AJ是一种隐藏的互模拟我们现在证明A，AJ是最大的隐互模拟。设R是A与C之间的隐互模拟，C是隐排序H.我们通过对深度c的归纳证明了：如果a RhaJ，则Ac（a）=AJc（aJ）.若c=σ（z：h，d），则Aσ（a，d）RAσ（AJ，d）蕴涵Aσ（a，d）=Aσ（AJ，d）.现在我们假设c=CJ[σ（z，d）]，其中σ∈hw，HJ.则Aσ（a，d）RAσ（ AJ，d）和归纳假设意味着 ACJ（Aσ（a，d））=AJCJ（AJσ（ AJ，d）），因此Acj（a）=Ajc（AJ）。 因此，aR aJ意味着aA，AJaJ，即，A，A.✷推论3.6若A和AJ是两个隐代数，则A，AJ= A，AJc。引理3.7设FJ：A → AJ和FJJ：A → AJJ是两个隐同态.如果aJ<$AaJJ，则fJ（aJ）<$AJ，AJJfJJ（aJJ），对所有aJ，aJJ∈A。证据如果aJ和aJJ是可见类的，则fJ（aJ）=aJ=aJJ=fJJ（aJJ）通过隐同态和A的定义。如果一个J和一个JJ是隐藏排序h，那么：aJAajj（<$c∈L<$[z：h]）Ac（aJ）=Ac（aJJ）<$（fc∈L（<$c∈L<$[z：h]）AJc（fJ（aJ））=AJJ（fJJ（aJJ））<$fJ（aJ）AJ，AJJfJJ（aJJ）✷推论3.8如果R <$A × A是一个隐同余，则{（f J（aJ），f JJ（aJJ））|aJR aJJ}是AJ和AJJ之间的隐藏互模拟。13通过共归纳证明双相似性。设A和AJ是两个隐代数. 设a∈Ah，aJ∈AJh对于某个h∈H.为了证明A，AJaJ，(i) 定义一个关系RA×AJ，(ii) 证明R是一个隐互模拟，(iii) 显示aR aJ。如果A和AJ是两个SP-模型，则R的候选是由AtR AJtJitSPtJ给出的关系。例3.9我们可以使用具有初始语义的模块来定义隐藏规范的模型下面是两个这样定义的UB1mod！M1{保护（数据）*[单元格1]*op [_，_]：Bool Data -> Cell1bop empty？：单元格1->布尔值op write：Cell1 Data -> Cell1bop read：Cell1-> Datavar B： Bool varD D操作为空：->单元格1eq empty = [true，nothing]。eq为空？([B，D]）= B。ceq read（[B，D]）= D if not B.ceq read（[B，D]）= nothing ifB.eq write（[B，D]，}mod！M2{保护（数据）*[细胞2历史]*op [_，_]：Bool Data ->Cell2 op _ _：Hist Cell2 ->Hist op nil：-> Histbop空的？：历史->布尔操作写入：历史数据->历史bop读取：历史->数据varB ： 布 尔值var D：数14据var H：历史eq为空？(nil)真的。eqread（nil）=无。eq为空？（H [B，D]）= B.15如果不是B，则ceq读取（H [B，D]）=D。ceqread（H [B，D]）= nothing ifB.eq write（H，D）= H [不为空？(H)，D]。}初始M1-模型M1和初始M2-模型M2都可以被看作是UB 1-模型。例如，如果我们考虑由下式给出的签名态射：查看从UB 1到M1的PHI {hsort Ub 1-> Cell 1，op init1 -> empty，op write -> write，bop read -> read，bop空的？ -> empty？}则M1PHI是UB 1-模型。我们把M1写成M1PHI.M1是单元模型，因为它通过表示最后应用的写入方法的结果的对[B，D]来对缓冲器的状态进行建模。M2是一个历史模型，因为它保留了存储在缓冲器中的所有数据的历史。M1和M2之间的互模拟定义如下：mod PROOF{保护（M1 +M2）op _R_：Cell 1历史->布尔变量B：布尔varD：数据varH：历史ceq [B，D] R H = true如果（B ==空？(H)而read（[B，D]）== read（H））。}R确实是互模拟的事实的证明遵循与行为等价性的证明相同的步骤，但是其中写入的一致性被以下属性取代：如果[B，D 1] RH，则写（[B，D 1]，D）R写（H，D）。以下是最后一个属性的证明分数开放证明ops d d1：->数据。op h：-> Hist .eq为空？(h)真的。-->案例1red write（[true，d1]，d）R write（h，d）. --应该是真正的接近开放证明ops d d1：->数据。16op h：-> Hist .eq为空？(h)= false。-->案例二red write（[false，d1]，d）R write（h，d）.应该是真的17→JA，AJA，AJA，AJA，AJA，A→JSP，SPJSP，SPJSP，SPJSP，SP不不SP、SPJ密切3.1垂直签名态射我们将具有相同签名的隐藏代数之间的隐藏互模拟的定义扩展到具有不同签名但通过垂直态射相关的隐藏代数。 考虑（H，）和（HJ，J）两个隐藏的在（V，V，D）上排序的签名，并且φ：（H，V）（HJ，VJ）是垂直签名态射定义3.10从一个隐代数A到一个隐代数AJ的φ-模拟是A和AJφ之间的一个隐互模拟。定义3.11考虑A是一个隐代数，Aj是一个隐代数。关系式φ定义如下：φ是可见排序上的相等，如果a是hidden sorth且aJ是hidden sortφ（h），则aφ（h阿吉Ac（a）=AJφ（c）（AJ）对于所有局部上下文c∈L<$[z]。3.12号提案是最大的φ模拟。证据 只要看到对于所有局部的双上下文，AJφ（c）（AJ）=（AJφ）c（AJ）就足够了。c [z]和aJ∈ AJ。✷用余归纳法证明φ设A是一个隐代数，AJ是一个隐代数.假设φJa∈Ah和AJ∈AJφ（h）。为了证明一只蜘蛛，(i) 定义一个关系RA×AJ，(ii) 证明R是φ-模拟，并且(iii) 显示aR aJ。R的候选者定义如下。考虑SP=（H，Ej，E）和SPJ=（HJ，Ej，EJ）两个隐藏规范，φ：Ej是一个垂直符号态射。定义3.13设t在T中，tJ在TJ中。如果t和tJ是（相同的）可见排序则t <$φtJi <$i有d∈D使得E|t = d，且EJ|tJ= d。 如果t是隐类h，且tJ是隐类φ（h），则t<$φtJi ∈L∈ [z：h]中的所有c，存在D中的d，使得E|c [t]= d，且EJ|φ（c）[tJ]= d从SP到SPJ的φ-模拟是一个关系R <$<$φ。命题3.14如果A是SP-模型，AJ是SPJ-模型，则关系{（A，A，j，J）|t<$φtJ}是φ-模拟。证据 用R表 示引 理结 论 的关系，并考虑t和tJ，使得t ∈φtJ。 如果c是L∈[z]中的局部上下文，则18Ac（At）=Ac[t]=d=dJ=AJφ（c）[tJ]=AJφ（c）（AJtJ）19JA，A→其中E |c [t]= d和EJ|φ（c）[tJ]= dJ。因为上下文c是任意的，因此，R ≠ φ。✷例3.15我们定义了一个模块UB2，它的行为与模块UB1的行为相似，但另外还有一个方法delete，它清空缓冲器：mod* UB2{extending（UB * {hsort Ub ->Ub2}）var B：Ub2var D：数据操作初始化2：->Ub 2bop delete：Ub2 -> Ub2bop no-del：Ub2 -> Ub2eq empty？（init2）=true。eq为空？（write（B，D））=不为空？（无del（B））。eq为空？（delete（B））= true。beq no-del（init2）= init2.beq no-del（write（B，D））= write（no-del（B），D）。beq no-del（delete（B））= no-del（B）。}派生的操作符nodel，它删除删除操作符的出现，是用来保持“精神”的UB1：值的属性为空？对应于交替的连续写入。 态射φ：<$（UB 1）<$（UB 2）的定义和预期的一样。关系式R定义如下：mod PROOF{保护（UB 1 +UB 2）op _R_：Ub1 Ub2 -> Boolvar B1： Ub1var B2： Ub2R的定义等式init1 R init2 =真。等式B1 R B2 =（空？(B1)空？（no-del（B2）或（notempty？(B1)而不是空？(B2)读（B1）=读（B2））。}下面的证明分数表明R是φ-模拟：开放证明--假设op b1：-> Ub1。20op b2：-> Ub2 .op d：-> Data.
我的内容管理
展开
