文件标题：控制流推断会话类型

理论计算机科学电子笔记238（2010）15-40www.elsevier.com/locate/entcs从控制流推断会话类型彼得科林伯恩1保罗H J凯利2伦敦帝国理工学院计算机系，邮编：SW72AZ联合王国摘要本文研究的是一种从静态类型命令语言的控制流中导出程序会话类型的技术。我们强加于我们的无标签的会话类型的语法规范化的基础上的格式良好的约束，并探讨其效果。我们提出了我们的推理算法声明，并在一个适合于实现的形式，并举例说明。 然后我们介绍使用程序分析和转换工具包的算法的实现关键词：会话类型，命令式编程，控制流，类型推断，程序分析1引言会话类型[10]是一种描述通信信道上进程之间的二元交互的方法。会话类型是会话的一个属性，会话是通过信道建立的通信链路。进程交互被表示为一系列通信操作，并且在与该类型相关联的会话上发生的任何通信都必须符合该操作序列。虽然会话类型的根源可以追溯到π演算[15]，但它也被应用于广泛的编程范式，包括面向对象的命令式编程[6]。会话类型可以采取多种形式，但是让我们现在考虑由图组成的会话类型，其中通信进程与图中的单个节点相关联。 通信操作必须与传出的弧，并根据通信操作的类型，使会话类型的适当弧被遵循。 图1示出了三个会话类型图（a）、（b）和（c），其中（a）和（b）以及（a）和（c）1电子邮件：pcc03@doc.ic.ac.uk2电子邮件：p. imperial.ac.uk1571-0661 © 2010由Elsevier B. V.出版在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.06.00316P. 科林伯恩，P.H.J.Kelly/Electronic Notes in Theoretical Computer Science 238（2010）15s1s1s1外α外α在α中在α中S2S4S2S4单位β在γ中输出β外γ第三季第五集第三季第五集(a)(b)（c）第（1）款Fig. 1. 三个示例性会话类型图。据称是相互兼容的（由于公共子图）。让我们考虑两个进程A和B，分别具有会话类型图（a）和（b）。两个进程都在状态s1中启动。首先，进程A发送一个类型为α的消息，并转换到状态s4。当进程B接收到这个消息时，它转换到状态s2.然后进程B发送一个类型为β的消息。然而，进程A不能处理这个消息，因为根据它的会话类型图，它只能接收类型为γ的消息。类似的情况出现在类型（a）和（c）的交互进程A和C中，其中进程A在接收到类型α的消息时首先转换到状态s2。因此，我们可以得出结论，不可能构造一个会话类型，使得具有该会话类型的进程可以安全地与会话类型（a）的进程通信请注意，进程A在内部选择它的两个分支中的哪一个在发送类型α的值之前获取。请进一步注意，没有从进程A向其对等进程传递关于其分支选择的信息。这是我们在具有隐式选择的会话类型系统中所期望的。在本文中，我们将探讨如何上述情况可能会出现在会话类型推理系统，产生会话类型与隐式选择，以及我们如何可以检测到它。我们要求作出以下贡献：• 第一个会话类型推断算法的作者已知的静态类型的命令式语言与会话类型语法的基础上隐式选择;• 一种基于规范化的会话类型格式良好性约束，P. 科林伯恩，P.H.J.Kelly/Electronic Notes in Theoretical Computer Science 238（2010）1517⊕⊕基于内隐选择;• 一个属性，确保会话类型的会话类型安全，该属性具有基于隐式选择的语法，同时允许输入和输出，称为安全方向性属性;• 基于C++的基于会话的通信进程库实现了会话类型推断。1.1背景：会话类型在大多数现有文献中，会话类型被表示为具有指定语法的表达式。会话类型语法通常是递归的。 这允许通信动作以任何适合程序结构的形式进行任意组合。一个会话类型可以采取多种形式，我们将简要描述其语义会话类型可以是动作。 动作指定通信方向（输入或输出）和类型（这可能是语言特定的原语类型，或者在委托[6]的情况下，另一个会话类型）。一个动作表示，根据通信方向，接收或发送指定类型的值（或会话）。 会话类型也可以是两个或更多个会话类型的顺序组合。会话类型，它是一个或多个会话s1，s2.sn表示s1中的操作，然后依次是s2中的操作，依此类推，直到sn。会话类型也可以是在多个会话s1、s2...sn. 在这些选择之间做出决定的过程在下面的段落中描述会话类型也可以是终止会话类型。具有终止会话类型的会话不能执行任何通信动作或改变其类型。它只能关闭通信信道。一个进程可以被动地或主动地、隐式地或显式地提交这些选择之一。如果一个进程主动地做出选择，那么这个选择是由进程根据它对通信步骤的选择做出的。如果进程被动地做出选择，那么这个选择是基于它的对等进程做出的主动选择。在隐式选择下，过程执行仅与其中一个选择一致的通信动作。 请注意，流程在提交 根据通信动作的方向，选择是主动的还是被动的。如果进程发送数据，它的角色是主动的;如果它接收数据，它的角色是被动的，它的选择取决于接收到的数据的类型。[5]是一个包含隐式选择形式的系统在显式选择下，该过程执行某些动作，而不是具有选择特定选择的效果的通信动作。文献中包括了许多表达明确选择的方法在[10]中，选择由和二元运算符表示。会话类型为s1s2形式的进程在s1和s2之间进行被动选择，而会话类型为s1s2形式的进程通过inl和inr操作符进行主动选择。在[8，9]中，每个选择都用标签注释。做出主动选择的过程18P. 科林伯恩，P.H.J.Kelly/Electronic Notes in Theoretical Computer Science 238（2010）15该标签对应于其期望的选择，并且进行被动选择的进程选择对应于其接收的标签的会话类型在执行通信动作之后，或者在明确选择其他相关动作的情况下，会话的当前类型发生变化，以便反映信道的当前状态。如果已做出选择，则会话类型将替换为与已做出的选择对应的类型。如果发生了通信操作，则从当前会话类型的开头删除表示该通信操作的类型。结果会话类型称为给定操作下该会话类型的延续类型兼容性[8]是会话类型之间的关系，表明两个具有指定会话类型的程序是否保证彼此安全通信;也就是说，在运行时没有任何可能的协议不兼容性。兼容性关系在指定和验证双方之间的合同方面特别有用：通过在可能的通信发生之前验证兼容性，可以检查在双方之间可能不会发生协议不兼容--只要双方遵守它们的会话类型合同。 显然，会话类型的必要条件是与另一个兼容的一个重要条件是它必须至少接受另一个可能发出的数据类型。稍后我们将看到这个概念的更正式的定义这项工作的目标是调查的手段推断会话类型使用程序分析技术给出了一个命令式的程序组成的一系列通信动作。在某些进程形式主义中，例如[10]中描述的π演算，通常不需要推理算法，因为进程的构造规则隐式地执行类型化。在这里，我们采用了一种语言中立的方法，更适合于命令式程序的结构，使用控制流和表达式类型的信息提供的主机语言，以获得一个适当的会话类型。与许多其他关于会话类型推理的研究[10，6]相反，我们的会话类型使用隐式选择。我们做出这个设计决策的理由是，隐式选择提供了行为之间更紧密的映射，程序及其会话类型。 此外，它使程序员不必为非类型化程序中的每个通信操作提供标记名。我们将探讨这一决定对我们的类型推理技术的影响。我们的类型推理工具允许我们决定程序之间的接口兼容性，而不需要超出程序类型和控制流程结构所暗示的正式协议规范。例如，程序员可以编写一个用于客户机/服务器体系结构的服务器通信程序 并期望与之通信的任何客户端都受到其原型的约束， 没有任何额外的工作。在这样一个过程中有两个关键步骤：首先，我们的推理算法被用来确定控制那些我们希望决定兼容性的程序的会话类型;其次，通过宿主语言的类型系统检查兼容性P. 科林伯恩，P.H.J.Kelly/Electronic Notes in Theoretical Computer Science 238（2010）1519而（一）int x;recv选择 （s）情况要求1：S . receive（Req1（x））; s . return（x）;情况要求2：S . receive（Req2（x））; s . return（x+2）;情况退出：S . receive（Quit（））; s . return（）;return;//出口子程序}}图二. 简单的伪代码服务器进程。int x;S . send（Req1（42））; s . return（x）;S . send（Quit（））; s . return（）;图三. 简单的伪代码客户端进程。1.2例如考虑图2中所示的服务器程序，我们希望它与图3中所示的客户机程序进行接口。我们通过检查来验证这两个程序可以正确地相互接口，并且通过会话类型推断和兼容性检查来验证我们的系统。我们的系统可以推断出这两个过程的类型会话的推断类型图2中的s是μt。（要求1）out int.t|在要求2中。out int.t|退出。end），图3中推断出的会话s的类型是{{20P. 科林伯恩，P.H.J.Kelly/Electronic Notes in Theoretical Computer Science 238（2010）15输出要求1。在整数中。退出。端使用这些类型，宿主语言的扩充类型系统将验证兼容性。P. 科林伯恩，P.H.J.Kelly/Electronic Notes in Theoretical Computer Science 238（2010）1521|≡D：：=ST：：=“在”|“出局”“μ“t“。“ST（穆）|“结束”（完）|不（电视）|“（“ST“|“ST“）”（选择）|“（“ST“。“ST“）”（Seq）|D V T（行动）见图4。 Ninja会话类型。1.3定义我们的推理系统有两种不同的方式。首先，我们将提供一组推理规则和应用它们的方法，以便导出会话类型。其次，我们将描述一个基于图形的算法实现技术。该技术使用的图基于有限自动机[18]，因此我们采用了该领域的许多技术，包括子集构造[18]。Ninja是基于组件的命令式语言扩展的规范。Ninja可以被认为是通用组件模型的实现，例如第2节中描述的架构描述语言。它可以扩展大多数命令式语言，但是我们的实现是针对C++语言的，被称为Ninja-C++。 我们描述了Ninja-C++的实现和一个类型推理工具.图4显示了Ninja语言中会话类型的语法。 请注意，在非正式讨论中，我们使用““和“”的结合性尽可能省略括号参考第1节，大部分语义都很清楚，但请注意语法元素（Mu）和（TV）。这些是用于递归类型定义的标准[17] syn- tax元素。(Mu)声明一个任意名称的类型变量t以供使用。对应的（TV）元素在（Mu）元素内找到，并且等价于对应的外部（Mu）的整体Ninja是一种基于组件的语言;组件是活动的，被称为参与者。参与者通过特定会话类型的通道相互通信，这意味着他们的会话类型必须兼容。我们继续介绍我们的相容性概念，最初由[8]定义，并由[20]等扩展。为了确定兼容性，我们必须首先为我们的会话类型语法定义等价性、连续性、子类型和对偶性。 等价 （）是满足图5中给出的规则的最小关系。 可以使用图6中给出的规则来导出给定通信动作下的会话类型的持续类型。然而，许多等价和连续规则是自解释的我们认为有必要给予规 则 的公正性（|Dist ←）. 这将在22P. 科林伯恩，P.H.J.Kelly/Electronic Notes in Theoretical Computer Science 238（2010）1512121212121intint2第3.1节在必要的背景介绍之后定义1.1会话类型上的自由名称。FN（μn.s）=FN（s）\nFN（end）=FNFN（n）={n}，n是类型变量FN（（t1|t2））= FN（t1）<$FN（t2）FN（（t1.t2））=FN（t1）<$FN（t2）FN（a）=定义1.2输入域和输出域。idom（μn.s）=idom（s）odom（μn.s）=odom（s）idom（end）=idom（end）=idom（n）=n， naty pevariableidom（n）=n， natypevariableidom（（t1|t2））= idom（t1）idom（t2）odom（（t1|t2））= odom（t1）odom（t2）idom（（t1.t2））= idom（t1）odom（（t1.t2））= odom（t1）idom（int）={t}odom（int）=Idom（outt）=Idom（outt）={t}定义1.3类型模拟[8]。类型模拟是满足以下性质的关系R（S1，S2）∈R_n（S1）_n（S2）第二章（S1）∧∀t∈idom(S1)∃SJ,SJ:(S1−→SJ∧S2−→SJ∧(SJ,SJ)∈R)<$<$t∈odom（S2）<$SJ，SJ：（S1o−u→ttSJ<$S2o−u→ttSJ<$（SJ，SJ）∈R）1.4分型定义3. S1≤S2i ≠存在型模拟R使得（S1，S2）∈R.P. 科林伯恩，P.H.J.Kelly/Electronic Notes in Theoretical Computer Science 238（2010）15233这是宿 主 语 言 的 子 类 型 关 系 的扩展， 以 在 会 话 类 型 上 提 供 子 类 型 。24P. 科林伯恩，P.H.J.Kelly/Electronic Notes in Theoretical Computer Science 238（2010）15112221212123123SS (Re）idom（S1）= idom（S2）（（S.S）|（S.S））（S|（S））（|Dist ←）S1和S2（Sym）1 2 12S公司简介（（S .S）|（S .S））（（S|（S）（|Dist→）S1-S2-S3S1和S3（翻译）S1S1J（S1）|S2）S（S1J|（S2）（|聪）w∈/FN（S）（μRen）μv.Sμ w. （S[w/v]）（μExp）μv.SS[μv.S/v]S1S1J（S1.S2）（S1J.S2）S2S2J（S .S）（S.SJ）（。Cong←）（。Cong→）（S|S）S（|同上）1 21SSJ2（μCong）（S|S）（S|（|通信）μv.Sμv.SJ1221v∈/FN（S1）（|天冬氨酸）μv。（S1.S2）μv.（S2[（S1.v）/v]））（。Rot→）（（S1|（S2）|（S3） 中文（简体）|（S2）|S3））v∈/FN（S2）（. Rot←）（（S .S）.S）（S .S）））。天冬氨酸）μv。（S1.S2）μv. （S1[（v.S2）/v]）.S2）图五. 等同规则S（a.SJ）S−a→S J（续）S1−a→S J（S1）|S2）−a→SJ（|以琳←）S2−a→S J（S1）|S2）−a→SJ（|Elim →）定义1.5二元性1P. 科林伯恩，P.H.J.Kelly/Electronic Notes in Theoretical Computer Science 238（2010）1525见图6。 延续规则输入t=输出t=输入tS1.S2= S1.S2S1|S2= S1|S2μv.S=μv.S v=v，v类型变量end=结束26P. 科林伯恩，P.H.J.Kelly/Electronic Notes in Theoretical Computer Science 238（2010）15定义1.6兼容性T daST≤S也就是说，T被定义为与S兼容，它的补体是S的一个亚型。为了保持两个对等体之间的兼容性，在允许输入和输出的状态下，我们对所有有效的会话施加安全的方向性属性。安全方向性属性在附录A中进行了说明。定义1.7安全方向性。 会话S是安全定向的，（idom（S）/=idom（S）/=）→<$to∈odom（S）<$SJ：So−ut→toSJ<$S≤SJ在测试中，i∈idom（S）<$SJ：S−→SJ<$S J≤S1.4类型突变和线性在本文中，我们假设一个静态类型的语言。然而，会话类型理论[10]指出，在会话执行通信操作后，其类型必须自动突变为相对于已发生的操作的会话的延续类型。大多数静态类型语言不允许 变量的类型在任何情况下都会发生变化，尽管有些情况下确实允许一个变量，可以被同名但作用域更严格的变量重写。这似乎是模拟类型“变异”的唯一可行方法，但在每次通信操作后创建新作用域的要求将严重限制程序的结构。因此，我们采取的策略，引入一个新的会话变量后，每一个通信行动。在我们使用了一个会话变量（即通过它发送或接收）之后，它就变得无效了。这意味着任何进一步使用该变量都是错误的，并且会违反我们的类型系统。 具有这种约束的变量被称为[22]线性变量，任何满足此属性的程序都被称为满足线性约束。我们已经开发了一个原型工具来检查会话值的线性使用[3]。1.5关闭会话为了确保程序的正确行为，我们对关闭会话的操作施加了以下约束。end类型的会话必须通过对会话执行close操作来关闭其会话。此外，任何其他类型的会话都不能关闭。第二个约束是微不足道的强制，但我们可以通过断言每个语句，a分配给类型为end会话s，必须存在s.close（）形式的语句c，cpdomaP. 科林伯恩，P.H.J.Kelly/Electronic Notes in Theoretical Computer Science 238（2010）1527{组件滤波器提供输出流char>;需要输入流char>;}见图7。 一个Darwin组件类型的例子（礼貌[14]）即cpostdomains [1]a.直观地说，这意味着所有计划关闭的会话（通过导致结束类型会话的通信操作）都被程序的控制流程保证关闭，只要程序不中断，例如。由操作系统。definite termination属性声明只有end类型的会话可以被关闭。此属性确保通信进程之间的同步2相关工作这项工作这项工作还介绍了会话类型的π演算推理。Dezani-Cianca- glini等人[6]将会话类型带到了命令式语言中莫斯他们[5]后来用兼容性的概念扩展了这项工作[8]。其他指定和验证协议兼容性的方法包括有限状态自动机（包括接口自动机[4]和编排[7]），通道契约[11]和组件接口[2]。Ninja提供了一个类似于统一建模语言[16]或架构描述语言（如Darwin [14]）的组件模型。虽然UML组件模型在很大程度上是抽象的，允许任何形式的通信，如流模型，共享内存模型或过程调用，但NinjaDarwin3衍生与规范性本节提供了我们的推理算法的推导步骤的高级描述。 由于我们的算法是语言独立的，控制结构被定义为被语言。特别是，宿主语言应定义以下内容：撑条对话程序语句►表达式的类型赋值EX表 达 式 语法会话变量的S然而，对会话进行操作的程序语句的语法是定义的28P. 科林伯恩，P.H.J.Kelly/Electronic Notes in Theoretical Computer Science 238（2010）15λ（S（，S））：=S.T={t}∅SS：：=|||S.send（EX）（发送）S.receive（EX）（Recv）S.close（）（关闭）（Lambda）图八、会议发言稿输入数据中不存在灰色语法图8中给出的语法。我们的算法支持无限数量的并发会话。定义3.1选择组合。 选择复合运算符的非确定性定义如下。. T=（t|. （T\{t}）），|不| ≥2<$t∈T定义3.2规范。在下文中，a是一个动作。(i) （S1）|如果会话S1和S2是规范的，则Idom（S1）是规范的Idom（S2）=odom（S1）=odom（S2）=n，S1/nend和S2/nend。(ii) （a.S）是正则的，如果S是正则的。(iii) （S1.S2）不是典范的，如果S1不是一个动作。(iv) μv.S是正则的，如果S是正则的且v∈FV（S）。(v) 结尾是canonical。(vi) V是典型的。(vii) A不是典型的。我们开始重写所有形式的状态[s.send（e）]]到[[s：=s.send（e）]];以及所有形式的状态[s.receive（e）]]到[[s：=s.receive（e）]]。 我们尝试将会话语句转换为单一静态使用形式。然后应用图9中给出的规则，通过求解Δ =为每个会话变量分配类型，其中Γ包含当前上下文的语言特定类型信息。每个良构类型必须有一个规范形式，如定义3.2所述，根据图5中给出的等价规则，它等价于原始派生类型。如果任何类型不是格式良好的，即它不具有等价的规范形式，则推理算法失败。在导出每个会话类型的规范形式之后，我们首先将出现在λ语句左侧的任何会话变量全局替换为右侧命名的会话变量，然后删除λ语句本身，从而消除λ语句。请注意，会话变量保留在λ语句被消除之前分配给它们的类型。S：=S：=P. 科林伯恩，P.H.J.Kelly/Electronic Notes in Theoretical Computer Science 238（2010）1529.|←[s. close（）]]∈StmtsΓ， ΔΔ εs：结束（关闭）[[s] J：= s. send（v）]]∈StmtsΓ <$v：tv<$freshΓ，Δ[s <$→<$]<$sJ：tsJs∈/domΔΓ，Δ εs：μ π ι。（outtv.tsJ）（发送）[[s] J：= s. receive（v）]]∈StmtsΓv：tvfreshΓ，Δ[s <$→]sJ：tsJs∈/domΔΓ，Δ ε s：μ π ι。（intv.tsJ）[[λ（s1，s2，.，sn）：= s]]∈Stmts新鲜的（接收）1≤i≤n：Γ， Δ[s<$→Γ，Δ ε s：μ π ι。（{ti：1≤i≤n}）Δ（s）=Δ（λ）（缩写）Γ， Δεs：π3.1司法化见图9。 类型推理规则本节给出了我们上面给出的推导过程的部分背后的推理规范性规则（i）确保在一个选择结构中没有两个选项可以呈现相同的选择。 这一规则确保将此类选择推迟到 最后一刻这反映了对通信进程的限制，即进程只能根据它发送或接收的变量的类型，而不是任何其他信息。 在将等价规则应用于会话类型以使其符合规范性规则（i）的过程中，等价规则（Dist）将被最频繁地使用。这条规则防止了第1节中所示的情况，即会话类型的两个不同分支最初通过其输入的类型来区分。没有必要对最初由其输出类型区分的分支强加这样的规则，因为通信过程可以在此时简单地接受两种值类型4算法本节提供了一个具体的描述，我们的类型推理算法适合实现。我们的算法分三个阶段实现。为了30P. 科林伯恩，P.H.J.Kelly/Electronic Notes in Theoretical Computer Science 238（2010）15}{}个字符。∗LLLLL如果（）下一页s1：= s1. send（int） ;s1：=s1.receive（int）elses1：=s1.send（long）;s1：=s1.接收（长）;s1：=s1.send（bool）见图10。 简单的LN程序。为了说明，我们将使用Ninja-C++的简化版本，称为N，其语法仅包含if，while和会话通信语句，其中符号取代了布尔表达式，表达式类型取代了所有其他表达式，并且其控制流程以明显的方式定义。将一个用 C++ 编 写的 Ninja-C ++程序翻译成N是可能的，方法是用通常的方式将for循环转换成while循环，删除所有变量声明，删除所有在N中没有对应项的语句，并将所有原始值替换为它们的类型。注意，N不包括调用，因为我们没有推断通道的类型;它可以有任何类型，比参与者的dual更不特定我们的语言支持无限数量的并发会话。4.1阶段1：静态一次性使用第一步是确保没有会话变量被超过必要的重用。这与第1.4节中提到的线性约束不同;我们在这里要做的是检测合法的线性程序，这些程序重用会话变量，而不是尽可能使用新变量，这意味着我们的推理算法将生成过于通用的会话类型。 在最极端的情况下，整个过程中只使用一个会话变量（注意，这是我们推导算法的起点）。因此，程序图10显示了N中的一个程序，它可以自由地重用会话类型，图11显示了应用SSU后的同一个程序。4.2第二阶段：图表构建在获得程序的SSU形式之后，我们然后使用其通信语句构建程序中包含的会话转换的图。图12所示为构建该图的函数g，图13所示为统一映射器fG的辅助。该功能的目标是双重的：• 提取所有通信动作并将其收集到带有弧的图中P. 科林伯恩，P.H.J.Kelly/Electronic Notes in Theoretical Computer Science 238（2010）1531}{}个字符。λ（s2，s3） ：=s1;如果（）下一页s4：= s2。send（int） ;s6：=s4.receive（int）elseS5 ：= s3。send（long）;s6：=s5.接收（长）;s7：=s6.send（bool）见图11。 简单的LN程序后，SSU应用。g（p）=fG（G，δ）其中（G，δ）=fP（p）fP（sJ：=s.send（t））=（（{{s}，{sJ}}，{（{s}，{sJ}，outt）}，），λx.x）fP（sJ：=s.receive（t））=（（{{s}，{sJ}}，{（{s}，{sJ}，int）}，），λx.x）fP（sJ：=s）=（（n，n，n），n（{s，sJ}））fP（s.close（））=（（，，{{s}}），λx.x}））fP（if（*）{p1}else{p2}）=fP（p1;p2）fP（while（*）{p}）=fP（p）fP（s.recv choice{c}）=fC（c）fP（λ（s1，... ，sn）：=s）=（（，，），（{s，s1，.，sn}））fP（p1;p2）=（（n1<$n2，e1<$e2，a1<$a2），δ1<$δ2<$δ1）其中（（n1，e1，a1），δ1）=fP（p1）（（n2，e2，a2），δ2）=fP（p2）fC（caset：p）=fP（p）fC（c1;c2） =32P. 科林伯恩，P.H.J.Kelly/Electronic Notes in Theoretical Computer Science 238（2010）15（（n1<$n2，e1<$e2，a1<$a2），δ1<$δ2<$δ1）其中（（n1，e1，a1），δ1）=fC（c1）（（n2，e2，a2），δ2）=fC（c2）见图12。 图形构建函数g。P. 科林伯恩，P.H.J.Kelly/Electronic Notes in Theoretical Computer Science 238（2010）1533⎧⎨⎩（{δ（n）|n∈N}，fG（（N，E，A），δ）={（δ（n），δ（nJ），e）|（n，nJ，e）∈ E}，{δ（a）|a∈A}）（S）（x）=xx，否则图13岁统一映射器和辅助函数。在源和目标会话变量之间;• 对于变量赋值，确保源会话和目标会话接收相同的类型（这是fG构建δ函数的目的）。helper函数footer（图13）通过为给定的变量集提供接收相同类型的方法来帮助实现这一点。在构建图形之后，检查definite termination属性。对于图G=（N，E，A），其有限终止性可以表示如下：a∈A：$n2∈N，e：（a，n2，e）∈E请注意，如果同时使用多个会话，则图将由不相交的子图组成这些图是独立的，除非在阶段3中的安全合并操作4.3阶段3：图形简化和翻译在这个阶段，我们必须首先处理图，以便识别和合并节点，从而保留语义此外，我们希望识别无效图。首先，让我们定义图中节点等价的概念定义4.1图中的节点等价eq（ns，c，（N，E，A））<$→ ns ∈ c <$|NS| ≤ 1 ∨（ {eq（{nJ|n∈ns<$（n，nJ，e）∈E}，c{ns}，（N，E，A））|n ∈ ns ∧ (n,,e) ∈ E}（nsn1<$Gn2参与式（{n1，n2}，n，G）定义4.2应用替代函数。为了应用替换函数δ，我们用统一映射器fG（G，δ）的结果替换当前图G，其中fG在图13中定义。34P. 科林伯恩，P.H.J.Kelly/Electronic Notes in Theoretical Computer Science 238（2010）15.S.∈{}≤⎧⎪δ(n),n∈ns∩domδτ（ns，（N，E，A），δ）=μ πι。⎪⎪τ（n，G）=τS（{n}，G，n）<$$>{（a.τS（{nJ：n∈ns<$（n，nJ，a）∈E}，（N，E，A），δ[n→n∈ns]））nsA=A新鲜：n∈ ns<$（n，，a）∈E}结束，否则见图14。 会话类型构建函数τ。根据定义4.1，只要节点等价，我们就可以统一节点。这允许我们简化具有多个收敛弧的图，这些弧具有通向单个节点的相同标签。 对于图中的每对节点n1和n2G使得n1<$Gn2，我们应用替换函数<$（n1<$n2）。我们必须处理的第二种情况是发散。如果一个图有许多有相同标签的发散弧指向节点n1，n2. nn，我们必须将这些节点和任何依赖子图替换为单个节点n和关联子图，使得i 1.. n，τ（n）τ（ni），其中τ是图14中定义的会话类型构建函数。初始处理可以通过将我们的会话图视为NFA，使用子集构造将其转换为DFA并拒绝任何不满足此属性的图来实现。这种转换是合理的，因为它已经被证明[18]，每个NFA都有一个等效的DFA（接受相同的语言，或者在我们的情况下，通信动作的序列），它直接转换为跟踪合理性。在我们检查这个属性之前，我们必须将DFA中的节点标签从集合的集合转换为集合，以使其与NFA一致。这是通过应用替换函数来δ（x）=X验证上述属性的一种简单方法是在DFA图中的每个节点和原始图中的每个对应的组件节点之间“表面地”这样做定义4.3表观亚型。一个类型图H=（NH，EH，AH）是一个类型图G=（NG，EG，AG）i的一个超特殊子类型：<$nh∈NH，ng∈NG：ng<$nh=n idom（sg）nidom（sh）odom（sg）其中sg=τ（ng，G）sh=τ（nh，H）请注意，在实践中，表面子类型属性意味着每个节点、