存在子类型化时进程的类型化行为等价

网址：http://www.elsevier.nl/locate/entcs/volume61.html18页存在子类型化时进程的类型化行为等价马修·亨尼西和朱利安·拉特克·科格斯，苏塞克斯大学，布莱顿BN 1 9QH英国电邮地址：matthewh,julianr@cogs.sussex.ac.uk摘要我们研究类型化的行为等价的演算，其中的类型系统允许一种形式的子类型。这使得进程能够有选择地在通信信道上分配不同的功能。所考虑的等效性包括测试等效性和倒钩互模拟等效性的类型化版本。我们表明，这些可以通过标准的技术应用到一个新的标记过渡系统的congurations的特点。这些由一个过程术语和两个相关的类型环境组成;一个约束过程，另一个约束过程的计算环境。1引言类型系统在分布系统理论中起着越来越重要的作用。它们本质上是静态分析的一种形式，有助于消除程序中的运行时错误。在分布式系统理论中，这种运行时错误的直观概念已经扩展到包括各种属性。例如，在[14，3]中，类型系统被设计为检测潜在的死锁，而[19]则引入了一个类型系统，- 微积分，用于控制对- 微积分 这个类型系统在[18]中得到了进一步的扩展，现在形成了在编程语言Pict中实现的强大类型系统的基础，[20];高阶并发语言的相关类型系统可以在[12，13]中找到。在[22，21]等论文中，类型已被用于管理对资源的访问控制，而在[23]中，信任的概念已被纳入，以保护好的主机站点免受坏的计算代理的影响。子类型是大多数这些系统的重要组成部分例如在c2002年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。2图1在一个程序的同一个“区域”中，通信通道同时用于输入和输出是相对罕见的。通常，服务器有一种访问形式，而客户端需要不同的形式。这些访问要求可以使用类型集上的子类型关系来实现和管理。例如，一个特定的通道可以声明为允许读和写访问的类型;该通道可以传递给一个进程，比如说一个服务器，在一个只允许读或输入访问的子类型，并传递给一个客户端，在一个不同的子类型，只允许写或输出访问。事实上，在[22，26]等论文中，类型被视为能力的集合，例如读访问和写访问，并且将名称发送到子类型的进程相当于将其与声明的能力的子集许多分布式系统共同的另一个重要特性是能够测试代理名、资源名、位置名等的身份。这种语言特征在-演算中通过匹配构造来建模如果a = b，则P，否则Q具有在名称a和b相同的情况下P将执行的语义，否则Q将执行。在子类型存在的情况下，这种语言特征可能会表现出微妙的属性。例如，坚持a和b具有相同的类型以使上面的表达式是良好类型的，这将是不必要的限制。特别地，可能的情况是a和b被绑定到相同的名称，尽管是在不同的超类型，具有受限的能力，具有某种共同类型。在这种情况下，我们注意到，不仅条件语句会采取包含P的执行分支，而且a和b相同的信息也可以用于整理类型信息。对于P来说，使用a和b以及a或b类型中允许的任何能力都是完全安全的。这种灵活性和观察能力在类型化的面向对象语言（如Java）中通过显式向下类型转换和运行时类型检查来提供。为了满足这种可能性，我们在这里为条件构造提供了一个静态类型规则，该规则隐式地将a和b的类型转换为两者中最常见的子类型。本文的主题是调查的行为等价的类型化过程语言，特别是在存在子类型和平等测试的名称。一个进程运行的类型环境显然会影响它的行为，因此也会影响行为标识。让我们非正式地写`P'Q（y）表示P和Q当在受某种类型环境约束的环境类型环境规定可以使用标识符的类型;如果标识符不在域中，1 根据[20]，第93那么直观上它不能被过程的环境使用。然后，使用-演算的语法，我们将期望恒等式啊！hviR '0如果标识符a不在约束环境It的域中，也应该为真，如果它在域中，但规定它只能用于输出值。在这种情况下，流程环境将永远无法执行组件a！hvi;这样做需要对a进行读访问，而这是被禁止的。在出现子类型时，情况变得更加复杂。例如，考虑这两个过程，再次用-演算语法表示，P（ 新 c ： rw 嗨 ） a ！ hcijc！hi S Q（ new c： rwhi）a！hcij0两者都以某种类型rwhi生成新的通道c，其允许读取和写入访问。现在假设有一个类型环境，其中与a相关联的类型是这样的，它只能用于读取和写入标识符，而这些标识符本身最多只能用于写入访问。这些类型是微积分的许多类型系统的标准部分[19]。在这种情况下，我们希望“P”Q因为没有观察过程可以锻炼c！HVI组件。这是因为观察过程只能通过在通道a上接收新通道c来获得它的知识;但是这种传输方法确保了它永远不能获得对c的读访问，因为a的类型是in，因此永远不能激活组件c！hvi.类型环境中的直觉约束被观察的进程和与它们交互的进程，即观察进程。然而，这个例子表明，一般来说，观察者的类型环境与被观察进程的类型环境不同，在这种情况下，P和Q. 在通道a上的通信之后，观察到的过程P和Q，现在相对于在类型rwhi上用新名称c扩充的环境工作，而观察过程相对于在不同类型上用c扩充的不同类型环境工作;实际上是rwhi的超类型。使用[16]中的思想，为类型化版本的微积分定义合理的行为等价性是相对简单的。近似地，我们可以说（y）为真，如果C[P]和C[Q]对于所有关于适当类型的上下文C[ ]表现出相同的（简单的）行为;这样的等价被称为上下文定义的。此外，对于这种等价性，已经建立了有趣的恒等式[25]。然而，这种等价性的证明通常涉及对可能的上下文的复杂推理，本质上是在每个特定的上下文中建立一种形式的上下文引理。4案子这与无类型的行为等价相反，[15，9]，有一系列基于标记转换系统的强大技术。这些描述的过程中，他们可以执行的行动和他们的后果，与形式的判断P ！Q在本文中，我们表明，通过建立在[2，18]中的思想，可以为我们版本的演算开发类似的技术，其中名称可以被测试为同一性，更重要的是名称的类型可以动态变化。其中心思想是将上面的非类型化操作替换为以下形式的新类型化操作I; `P ！I0;0`Q哪里表示被观察进程的类型环境P，而I表示周围上下文或观察上下文所知道的知识. 执行一个动作可能会导致这些环境中的一个或两个的修改。形式I的三元组; `P，具有较小的一致性要求，被称为congurations，我们的判断赋予congurations的集合Conf具有标签转换系统的结构。我们表明，类型化版本的倒钩同余和可能和必须测试等价可以通过调整标准方法来表征，[15，9]这个lts。我们现在概述这个扩展摘要的其余部分。在下一节中，我们将回顾-演算，它的操作语义和类型系统;这是完全标准的。其次是我们对我们所研究的类型化行为关系的定义;我们的结果的新颖性和兴趣将在很大程度上取决于这些定义的自然性。这是论文的核心，第4节。在这里，我们定义了我们的知识为基础的标记转移系统Conf和状态的特征定理。 最后是结论，其中包含了相关工作的讨论。所有的证据，和许多细节都省略了，因为缺乏空间。但它们可能会在论文的完整版本中找到，[10]。2语言该语言的语法如图1所示，它预先假定变量（范围为x; y）和名称（范围为n; m）都是可计数的。熟悉微积分的读者在这里不会感到惊讶，除了可能省略了非确定性选择运算符。这个操作符对类型化，特别是子类型化没有什么影响，所以我们在本文中忽略了它。我们假设这种语言的标准约定，例如变量的自由和绑定出现，alpha转换，以及定义良好的无捕获替换操作。5T; U：：=术语 u？（X：A）T Inputu！hvi T输出ifu = vthenT elseU匹配（newn：A）T名称创建T j T并发T重复0终止X; Y：：=模式x变量（X1;：; Xn）元组u; v; w：：=值BV基准值n名称x变量（u1;：; un）元组图1。语法没有变量自由共现的项，称为过程，用P; Q表示。语言的操作语义是完全标准的，一个还原关系！，虽然我们在图2中的正式定义，使用两个类型的操作，a！？v（input）和（c~：C~）a！！v（产出）。我们的类型和子类型关系是[22]中所用类型的温和变化，而[22]又是[19]中所用类型的温和变化。除了一些基本类型，如int; bool，我们还有形式为r hAi; w hBi和frhAi;whBi g的类型，其中A;B又是类型。所有这些类型的值分别被认为是具有读取类型A的值、写入类型B的值或两者的能力的通道名称。我们经常用简写r whAi来表示frhAi;whAig。类型的正式定义如图3所示。唯一需要注意的一点是最大类型的存在>，它支配子类型关系中的所有类型。 直觉一个名字a at这种类型不能用于读或写;但我们的版本6e（l-输出）（l-输入）一个！我的爸爸！！VP是吗？（X：A）Pa！？vPfjv=Xjg（l-开放）P（c~：C~）a！！v 均p0（b：B）（ce：C）a！vb6= a0b2fn（v）（新b：B）P！ P（l-com）P（c~：C~）a！！vP0;Qa！？vQ0ec~\fn（Q）=;Pj Q！（新的ec：C）（P0jQ0）（l-com）Pa！？vP0;Q（c~：C~）a！！v Q0eintn（P）=;Pj Q！（新的ec：C）（P0jQ0）（l-当量）如果u = w，则P，否则Q！Qu 6= wif u = u then P else Q！P（l-cntx）P！均p0P！均p0PjQ！Q jP！P0 jQQ j P0bn（）62fn（Q）P ！P j P 0P！均p00 a62n（）P！P0PQ0（new a：A）P！ （新的a：A）PQ！ P图二. 操作语义的-calculus具有名称匹配，因此类型>的名称可以与其他名字相比。正如在[22]中详细解释的那样，由子类型关系排序的类型集：有一个部分满足运算符，表示为u;直观地说，A1 u A2是A1和A2中的能力的并集。流程术语的类型推断规则如图4所示。判断的形式是`T，其中是类7型环境，即从标识符、变量和名称到类型的nite映射。对于标识符id，我们写;id：A，用于通过扩充获得的类型环境，以便将id映射到A;只有当id不在的域中时，才定义此标记。更一般地，我们使用uid： A来表示类型环境;id：A如果id不在的域中，否则为0，其中0等于除了可能在id处，其中0取值（id）u A（如果定义）。这个符号以明显的方式推广到值。我们也说2是1的扩张，如果它的形式为1; 0，对于某个0。一般来说，我们会写2：1如果2（id）：1（id）用于域中的所有id1 .一、 最后我们会经常写对于封闭型环境，8我（A1：An）：（A0：A0）类型：>; int; bool 2类型A2类型rhAi 2类型whAi 2类型A; B 2类型; B：AfrhAi;whBig2类型Ai 2类型（A1;：;An） 2种类型分型：答：A0rhAi：rhA0ifrhAi;whBig：rhA0i答：A0whA0i：w hAifrhBi;whA0ig：whAi甲：甲0;乙：乙0frhAi;whB0ig：frhA0i;whBigA：>Ai：A01N图三. 类型仅仅由名字组成。熟悉微积分的输入/输出能力类型的读者，[19]，应该对推理规则没有任何困难，除了来自[22]的条件句的类型规则。为了建立如果u= v则 T，否则 U相对于类型环境是良好类型的，我们被允许在环境中输入T，通过将与u相关联的能力与与v相关联的能力“联合”来增强，反之亦然。操作语义和类型系统是一致的。建立这一事实的定理使用r（n）#来表示n处的类型环境nt具有形式为rhAi或frhAi;whBig的类型，在这种情况下，我们将r（n）写为引用类型A，在该类型下n可以读取值。对于w（n）也是如此。定理2.1（主语归约）假设”他说。然后P！ Q意味着Q啪！？vQ蕴涵r（a）#，并且如果uv：r（a）是l l-ded d，则uv：r（a）`Q.9P（c~：C~）a！！vQ蕴涵w（a）#，且c~：C~`v：w（a）;Q.10（t-id）（t-碱基）（t-ε）（u）：Abv2基地vi：Ai（8i）u：A`bv：基础`（v1;：; vk）：（A1;：;Ak）（t-输出）（t-当量）（t-in）;X：A`T`u：rhAi你：怎么了？`v：A`Tu：A;v：B`Uuu：Buv：A`T你呢？（X：A）T你！hvi T`如果u = v则TelseU（t-新）（t-str）;a：A`TT; U`（新a：A）T`T j U; T;0见图4。 打字规则3类型化行为等价我们专注于两种主要方法，第一种基于观察者辨别进程运行时行为差异的能力[17，9]，而第二种通常与互模拟理论[15]相关，使用共归纳方法。3.1测试预订在这里，我们明确了一个进程运行的计算上下文。测试或观察者是出现新保留名称的NITE！，用于报告测试成功。对夜间测试的限制只是为了方便;众所周知，[9]，在夜间测试中不会产生任何额外的辨别能力。我们让T在测试范围内，使用类型规则I`！！我为所有的你，我为所有的你，当与过程P并行放置时，测试可以与P交互，产生输出！如果已经观察到P的某些期望行为。我们写如果Tj P！P可能TR对于某些R，则R可以重新输出，即， R！！！海岛的较强关系在每次计算P必须T11T j P！R1！“……”Rn！* *有一些Rk; k 0，可以报告成功。 行为等价现在可以通过要求过程以相同的方式反应来定义，12一个给定的测试类在这里，选择相对于给定环境I类型良好的测试类是合适的定义3.1 [测试前序]我们写Ij= P@may Q，如果P may T蕴涵Q may T，对于每个测试T，使得I`T。同样，Ij= PQ必须T。@mustQ意味着对于每个这样的T，P must T意味着我们用=may和=must表示相关的等价关系。请注意，在I `P =must Q（以及类似的判断）中，类型环境I是对观察者或计算上下文的约束，而不是进程P; Q本身。3.2共归纳法在本小节中，我们使用类型环境作为对进程本身的约束，而不是它们的计算上下文。定义3.2过程上的类型化关系由过程上的关系族R组成，由封闭类型环境参数化R =fRj闭型环境g满足PRQ蕴涵P; Q。我们通常写j= P R Q代替P R Q。过程上的类型化关系由de n推广到任意项，ing;X：A j= T RoU为真，如果对于每个值v，封闭类型环境0与A不相交，并且ty peA使得;0`v：A，weave;0`Tfjv=XjgRUfj v=Xjg。请注意，这使我们能够替换新值，这些值不一定为当前类型环境所知;X：A，尽管它不允许 我们可以扩展已经在域中的 值 的 类 型 。然而，即使在封闭项上，关系R和它的开放扩张R o之间也可能存在差异;一般来说，j= P R o Q为真，我们必须有0j= P R Q对于每个允许的扩展0。请注意，这是一种弱化定义3.3一个类型化关系R被称为弱闭或w-闭，如果限制于过程的Ro与R重合。我们将考虑的所有行为等价都是w-闭的。为了定义这些，我们需要考虑类型化关系的一些属性关闭还原：类型化关系R是归约闭的，只要j= P R Q，P！P0意味着存在某个Q 0使13得Q！Q0和j= P0R Q0。140O=上下文：上下文是通过扩展图1中的语法来定义的，允许在术语中键入holes[ 图4中的类型化系统被扩展到 最明显的方法是，（int n） ;0`[]我们用C[ ]表示最多有一个洞的上下文，C[T ]是将T项代入洞中得到的项。我们留给读者去建立命题 3.4T和`C[0]表示`C[T]。2然后我们说类型化关系R是上下文的，只要0j= T Ro U，C[0]表示j= C[T]RC[U ]。这一条件对过程施加了许多限制。例如，在输入上，它说a？（X：A）T和A？（X：A）U相关，如果Tfjv=Xjg和Ufjv=Xjg对于每个v和0相关，;0`v：A;这包括当前环境倒刺保存：对于给定的名称，`a：rwh>i. 我们写j= P +倒钩 a，如果存在某个P 0使得P！一个！！嗨均p0. 然后我们说类型化关系R是倒钩保持的，如果j= P R Q，j= P +倒钩 a意味着j= Q +倒钩 a。定义3.5 [倒钩同余]设=cxt是最大的类型关系在过程中，对称，即关系的每个分量都是对称的上下文归约闭合倒钩保存。我们通常把这个关系写成j= PCXTOBSQ，我们强调这是对过程本身的限制，即P; Q，而不是它的上下文。命题3.6r=cxt 是w-封闭的。当我们给出这个关系的共归纳特征时，这个结果将有一个重要的结果4类型化动作15在本节中，我们正式定义了在引言中讨论的类型化操作。这些将形成标记的转换系统Conf，其可以用于16以提供上一节中讨论的行为等效性的特征。4.1类型化操作类型环境I兼容，如果I：>dom（I）=dom（）定义4.1三重I; `T是一个构形，如果是封闭型环境，I兼容于`T环境I表示进程中分配给名称的类型的环境视图因此，这个视图必须与分配给这些名称的实际类型一致这通过要求I：>来保证，其中是正在调查的术语的实际类型上下文。基本这表明环境不能知道根本不存在的信道的能力。环境域相同的要求是确保新名称唯一性的技术手段。我们使用Conf ，用C; D 来表示所有Congurations的集合类型化动作的转换系统的生成规则在图5中定义，并且应该被理解为作用于配置。这些规则是通过考虑计算上下文的类型环境I从图2中获得的;本质上，只有在 I允许的情况下，操作才是可能的。这种对可能操作的控制在从输入和输出压力生成操作的规则中很明显。我们看到，通道a上的输出动作（相应地，通道a上的输入动作）仅在环境具有互补能力（即通道a的读能力（写能力））的情况下才是可观察的。这个需求是为了确保测试这个动作所需的上下文，它将使用通道a上的输入（输出），在类型上下文I中实际上是可类型化同样值得注意的是，这种知识环境在行动之后是如何变化知识的唯一更新发生在从过程观察到输出假设，给定初始知识状态I，过程在通道a上输出值v作为测试人员，我们可以构建一个上下文，它接收通道a上的值，这些值的类型最多为Ir（a）。因此，在输出转换之后我们对该值的所得知识是转换之前v和Ir（a）的知识的最大公共子类型u这反映在输出转换的lts规则（ty lts-out）中。 使用在新名称文本下使用的相同基本规则（ty lts-out）（rule（tylts-open））来获得观察特定名称的输出的转换。可以观察到新名称b的输出，17（tylts-红色）P！I;P！均p0I;`P0（tylts-out）Ir（a）#我; 啊！我的爸爸！！vIu v：Ir（a）; `P（tylts-in）Iw（a）# I `v：Iw（a）I;`a？（X：A）Pa！？vI;`Pfjv=Xjg（tylts-打开）I; b：>;; b：B`P（c~）a！！vI 0;0`P0ba（b、c、e）a！v000b2fn（v）I; `（新b：B）P！I; `P（tylts-ctxt）I;P！I;P！I 0;0`P0I 0;0`PjP0（ty lts-equiv）I;`P！I;Q！I 0;0`P0I0;0`P0P QI;P！I 0;0`P0I;`Pj Q！I0;0`P0jQI;`Qj P！I 0;0`QjP0bn（）62fn（Q）I; a：A;; a：A`P！I0; a：A;0; a：A`P00 0 0a62n（）I; `（new a：A）P ！I; `（new a：A）P图五. 类型化操作并且获得与b已经存在但环境没有关于它的类型信息的情况相同的知识，即， b：>。还要注意，输出操作的绑定名称上的类型注释被删除了;它们在图2中只需要用于定义非类型化的还原关系！.命题4.2如果I; `P，那么I0;0`P0也是如此。！18I0;0`P0和I;`P是一个函数因此，（Conf;Act）确实是一个标记的转换系统，（lts）。5首先，我们回顾一下[15]中弱互模拟的定义。定义5.1给定一个标号转移系统T，我们说一个二进制T上的关系R是互模拟，如果每当n R m，则19如果p！如果q！p0thenthereexistsaq=）^q0thenthereexistsap=）^使得p使得其中=）^是注定的！，如果是，还有！！！否则，请执行以下操作。然而，我们知道，倒刺同余，=cxt，是w-封闭的，因此，当应用这个定义，以Conf，我们必须确保我们获得的关系，也有一个适当的推广这一性质。因此，对于我们使用表示Conf上的最大关系，弱互模拟w-闭的;满足I; `P我的;0`Q意味着I;00;;00`P I; 00; 0; 00` Q用于所有适当的00。定理5.2j=P=cxtQ当且仅当;`P;`Q。众所周知，[6]大多数测试通常是由过程可以执行的动作序列决定的。因此，让我们将这个想法应用于Conf，通过定义配置可以执行的类型化操作的序列：I;`P=）“I;P！I00;00`P00I;P！I00;00`P00I; `PI0;0` P0andI 0;0` P0=）sI0;0` P0andI 0;0` P0=）sI 00;00` P00暗示I;` P=）sI00;00` P00暗示I;` P=）s写I; `P=）这意味着存在一些I 0和0，I;`P=）sI0;0.定理5.3（May刻画）设I `P; Q。那么我j=P@may Q当且仅当I 0;I 0`P扩张I0ofI.=）表示I0;I0`Q=），对于每个请注意，使用了由yI0 扩 展的 类型 配 置文 件。 通常这是必需的，因为= may是一个封闭的关系;直觉上，测试人员，在我的环境中工作，可以发明新的名称来测试P; Q，在当前环境I中不知道的名称。同样众所周知的是，[6]为了进行随机测试，我们必须额外考虑过程在执行一系列动作时发散的能力，P + s，以及在执行一系列动作后它们的接受集Acc（P; s）。由于空间有限，我们省略了可能在[9]中找到的正式定义，但我们将其应用于lts Conf：20定义5.4在Conf中我们写CmustC0if for every trace s C +simplies（a） C0 +s（b）8A2Acc（C 0;s）9A02Acc（C;s）表示A0A：