通信模式中的进程同步对应断言

理论计算机科学电子笔记97（2004）175-195www.elsevier.com/locate/entcs并发通信中进程同步的对应断言Eduardo Bonelli爱德华多·博内利1，3史蒂文斯理工学院和LIFIA6Adriana Compagnoni阿德里安娜·Compagnoni1，4史蒂文斯理工Elsa Gunter艾尔莎·冈特1，2，5新泽西理工摘要通信模式（如协议）的高级规范可以通过会话类型优雅地建模[14]。然而，一些例子表明，当需要更精确的协议规范时，会话类型就不够用了。 为了增加会话类型的表现力，我们求助于对应断言理论[5，10]。由此产生的类型规程用事件扩充长期通道的类型，从而产生可能依赖于在同一会话中较早读取或写入的消息的类型。我们证明了评估保留了可类型性，并且类型良好的过程是安全的。此外，我们说明了如何产生的理论使我们能够解决存在的缺点，在纯理论的会话类型。关键词：并发编程，π演算，类型系统，会话类型，对应断言。1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.04.036176E. Bonelli et al. / Electronic Notes in Theoretical Computer Science 97（2004）175-1介绍分布式和并发编程范式越来越受欢迎，特别是自从Internet进入公共领域以来。这带来了新的挑战，包括这些程序的规范和实现，以及对其属性进行正式验证的技术。其中一种指定方法是协议指定。这包括识别为了执行某些特定任务而在多方之间发生的消息交换的顺序。最近，使用类型系统来形式化协议引起了许多研究人员的兴趣，特别是会话类型[13，14]已经成为一种有前途的方法。通过指定通过专用信道的消息的相互交换的这样的序列被建模为类型，在信道的每一端的双方具有双重这样的类型。这对对偶类型构成会话类型。会话类型被分配给长期通道，并在进程之间共享。长期通道是通信协议预先指定的端口。会话类型的一个示例是：（↓Int;↓Int;↑Int，↑Int;↑Int;↓Int）第一个组件，即<$Int;<$Int;↑Int，表示在一个会话点上的期望值：进程必须从通道中读取一个整数，然后读取另一个整数，然后将一个整数写入通道（考虑一个“加法”服务器，读取两个数字并写出它们的和）。为了使另一方正确地交互，它被分配了一个双类型表达式（该对的第二个组件）。相当多的资源被投入到会话类型的研究中，其动机是这样一个系统为协议分析提供的好处。从Honda等人的工作开始[13]，[6]中探索了会话类型的子类型的合适概念，[21]中提出了基于组件的软件开发中会话类型的好处，[12]中研究了会话类型存在时的有界多态性，[7]中考虑了具有输入/输出操作的λ-演算中的会话类型本文通过引入对应断言理论来加强会话类型（参见第1.2节）。我们将讨论1这项工作部分得到了NSF资助号CCR-0220286 ITR：安全电子交易的支持。2它也得到了ARO的部分支持，DAAD-19-01-1-04733电子邮件：ebonelli@cs.stevens-tech.edu4电 子邮件地址：abc@cs.stevens-tech.edu5电 子邮件地址：elsa@cis.njit.edu6阿根廷拉普拉塔拉普拉塔大学信息学院E. Bonelli et al. / Electronic Notes in Theoretical Computer Science 97（2004）175-177Cl（id，amt，a）=请求k中的a（k）！[id]; k<$deposit; k！[amt]; k？（bal）in stopATM（a，b）=在k中接受a（k）？（idA）ink<${存款：请求b（h）在k中？（amtA）in存款; [idA];h！[amtA];h？[balA]在k！[balA];ATM[a，b]Q撤回：请求b（h）在k？（amtA）在h中撤回;h！[idA];h！[amtA];h？（OKedAmtA）ink！[OKedAmtA];ATM[a，b]}Bank（b）=acceptb（h）inh<${存款：h？（idB）in h？（amtB）in updateData; h！[balB];Bank[b]Q撤回：h？（idB）inh？（amtB）ingetOKAmtForIdB; h！[OKedAmtB];银行[b]}Fig. 1. 以ATM为例一些例子说明了会话类型的缺点由此产生的类型规则比会话类型的纯理论要丰富得多。更准确地说，一些“不安全”的程序，这些程序在纯会话类型理论中是良好类型的，将被我们的类型规则拒绝。据我们所知，这是第一次研究长期信道的对应断言理论。1.1动机考虑以下由三方组成的示例：客户端，ATM和银行[14]，如图1所示，我们简要描述如下：客户。请求一个会话（通过共享名称a），然后客户端发送其id号，选择一个存款操作，告诉金额然后等待新的帐户余额。自动取款机 首先，它侦听名称a，以获取请求会话的客户端，然后读入客户端在存款操作的情况下，ATM请求与银行（在名称b上）的会话，读取客户希望存入的金额（从a），然后选择银行的存款操作。然后，它向银行发送客户端的ID和存款金额，获取新的余额，将其报告给客户端，并返回到起点。 自动取款机的取款操作与此该行它在名字b（与ATM共享）上监听会话请求，然后等待ATM指示它希望执行的操作（存款或取款）。如果它是一个存款操作，它将读取在id和金额中，更新其数据，发回新的余额，然后返回到其起点。在撤回的情况下，它相应地进行。178E. Bonelli et al. / Electronic Notes in Theoretical Computer Science 97（2004）175-让ATM这个表达式|客户端|银行表示指定各方的同时执行。[14]中提出的类型系统断言这个表达式是良好类型的。实际上，将以下会话类型分配给a和b（其中σ（α）是由α及其对偶组成的对的缩写），我们可以键入ATM|客户端|银行a：σ（↓Int;{存款：↓Int;↑Int;1，Q撤回：↓Int;↑Int;1}）b：σ（{存款：↓Int;↓Int;↑Int;1，Q撤回：↓Int;↓Int;↑Int;1}）第一种类型是说，在a上建立的所有通信会话必须遵守在一个端点上的σ参数和在另一个端点上的其对偶参数所描述的通信模式。 可以读取内部参数类型如下：输入一个整数后，等待来自对端的两个操作之一存款或取款;如果选择存款，则输入一个整数，输出一个整数并禁止进一步的通信，如果选择取款，同样如此。请注意，这些类型表示长期通道a和b如何相互独立地工作，即使它们都属于一个共同的规范，即指定客户端、ATM和银行应如何交互以执行特定操作（存款或提款）的协议规范。这一点可以证明如下。考虑由ATM通过用以下变体替换存款而产生的ATMATM'实施例1.1[沉积物I]押金：在k中请求b（h）？（amtA）in H存款;h！[idA];h！[amtA−1.5];（1）h？（balA）在k！[balA];要求b（hJ）在hJ中存款;hJ！[di jiang];hJ！[1.5];hJ？（balAJ）（2）在ATM中[a，b]这个版本的存款操作存入客户的帐户1.5个通过新的存款方式，在与客户不同的账户中存入1.5个单位请求（2）银行，这是不存在于原来的自动柜员机。E. Bonelli et al. / Electronic Notes in Theoretical Computer Science 97（2004）175-179不幸的是，这种改进的ATM机与前一种ATM机的类型相同同样，如果正常ATM的存款操作被相同的ATM替换，除了没有通知银行，那么最终的ATM也在与正常ATM相同的类型假设下进行类型划分。示例1.2[存款II]以下存款的变体允许ATM保留客户的存款，而不将其存入账户。如果我们称这个系统为ATM，那么ATM|客户端|在与ATM完全相同的类型假设下，银行是良好类型的|客户端|银行存款：k？（amtA）在k！[1000];ATM[a，b]这些例子表明，虽然会话类型优雅地编码了消息交换的通信模式，但它们缺乏表达能力，从而限制了会话之间的本文介绍了一个基于对应断言的类型系统[22，10]，其中ATM可以与上面描述的变体1.2对应断言对应断言起源于模型检查的上下文中[22]。在[9]中，为spi演算提出了一个对应断言的类型系统;在[10]中，同一作者提出了异步π演算设置中的清晰说明。直观地说，对应断言用于形式化这样一种想法，即某个进程P中的某个执行点必须在某个其他进程中的某个其他执行点之前Q，在所有可能的执行P |Q. 断言用于标记执行过程中的点。与[10]一样，本文中的断言可能有两种形式之一：beginL或endL，其中L是断言标签。 一个进程被认为是安全的，如果每个结束L断言在任何执行中达到，有一个相应的开始L断言，这是达到之前的某个时候，可能在一些其他进程。通过在不受信任的代码（包括与可疑代码通信的代码）中插入适当的通信断言，并询问生成的代码是否安全性可以通过类型系统来确定，因此允许我们静态地执行这样的检查。例1.3[存款I（续）]对应断言允许我们证明例1.1中ATM的变体是不安全的，如果我们断言要存入银行的金额与由ATM给出的金额相同，则ATM180E. Bonelli et al. / Electronic Notes in Theoretical Computer Science 97（2004）175-客户端，并适当地增加会话a和b的类型。为了证明这一点，我们首先用包含begin断言的代码替换Client的代码以获得Clientrequesta（k）in begin_id，amt_k！[id];k存款;k！[amt];k？（bal）instop注意，begin断言的标签包含表达式id和amt的出现。这些值由客户端生成并传递给ATM。接下来，我们向Bank的deposit操作添加一个end断言(2)在图1中，获得Bank存款：h？（idB）inh？（amtB）在“amtB”结尾处，amtB“;updateData;h！[balB];Bank[b]最后，a和b的会话类型增加了适当的事件（见第3节中的图5），这样，如果ATM向银行请求存款操作，并发送idB和amtB的任意值，则必须通过与客户端的相应通信来支付所产生的信用：客户端必须提供这些值。ATM系统|当事人|“银行”应是安全的，如果每次执行银行的存款操作的id号码idB和金额amtB，客户要求在ATM上进行相同的操作，并且idB = id，客户输入的id，和amtA = amtB，客户输入的金额。我们可以通过强制ATM与银行进行通信来类似地解决例1.2，此外，还要求选择存款这是通过强制从银行检索ATM发送给客户端的余额信息来实现的。在这种情况下，begin断言插入到bank中，end断言插入到客户端中。详情请参阅[2我们在第2节中介绍的类型规则表明，例1.3的系统对于给定的对应断言是不安全的。类型系统如何强制Bank'中的end断言仅在Client '中相应的begin断言执行之后才执行的问题，通过通道上的潜在效应来为了（idB）inh？（amtB））。现在，h是银行和ATM之间共享的通道|客户'（通过ATM'）.通过在通道h上放置潜在断言，银行可以将匹配结束断言的义务传递回试图在该通道上发送值的任何人。类似地，ATM可以使用其与客户端共享的通道上的潜在效应来进一步传递义务。事实上，由于ATM的代码没有自己的断言，这就是它所E. Bonelli et al. / Electronic Notes in Theoretical Computer Science 97（2004）175-181有义务。 由于义务是通过潜在的影响传递回来的，因此必须根据作为在通道上传递的信息的结果而发生的替换来翻译义务。当债务从银行 当我们将义务传递回客户端时，它被进一步转换为begin_id，amt-1. 5，这与断言begin_id，amt_id不匹配。 因此，我们可以得出结论，该程序不安全。值得注意的是，如果我们将begin断言更改为begin_id，amt-1. 5*，则程序将类型检查并声明为安全了 我们将，在这方面，承认自动取款机贡献本文介绍了一种基于类型的会话类型对应断言理论。• 与之前用于此类断言的类型系统相比，会话类型允许输入/输出类型的结果依赖于在同一会话中之前被交换的消息在我们的分析中，我们还包括[14]中的分支/选择和委托构造。由此产生的类型系统将允许我们区分ATM的上述三种变体。这是通过在代码中引入适当的类型指令（即as-sertions）并将适当的类型分配给名称和通道，然后使用本文中提出的类型规则进行类型检查来• 我们定义了一个新的类型系统的依赖会话类型相结合的会话类型和通信断言。这种组合引入了许多技术难题。例如，通常将环境表示为假设序列[1，10]不能产生满足某些标准基本性质的微积分（参见：注2.6）。• 我们证明了求值保持了可类型性，并且在空对象下可类型化的进程是安全的。相关工作。这项工作可能包括在其他类型系统的π演算的研究[18，16，17，20]。 子类型介绍在[6]中的会话类型的设置中;然而，没有探索会话之间的同步的概念。作品[23]和[19]也没有探索会话类型：第一个研究了基于图类型的进程的类型化方案，第二个研究了限制并发对象中通信的类型系统;它们与会话类型的关系在[14]中讨论。 而[10]与这部作品有相当多的共同点，但有一个主要的区别。在[10]中，类型中的依赖关系是然而，在这方面，182E. Bonelli et al. / Electronic Notes in Theoretical Computer Science 97（2004）175-由于我们的设置是会话类型，因此我们允许 在这种情况下，针对z读取的值的类型可以取决于针对x和y读取的值中的任一个或两者。这些后面的值在同一通道中读取，但在时间上先于z。因此，在本工作中，依赖性跨越整个会话。最近，已经出现了使用类CCS进程来键入进程表达式的类型系统[15]的泛型类型系统就是一个例子，尽管它没有包含通信断言（参见第4节）。另一种方法是[4]，其中获得π演算表达式的模型（类型为CCS-过程），并通过模型检查技术分析时态公式的有效性，以推断过程表达式的性质他们提出了一个类型和结果系统，其中包括对应断言，但没有长期的通道类型。论文的结构。第2节定义了πs，一个结合了会话类型[14]和对应断言[10]的系统。第2.2.1节给出了一个带有πs效应的类型系统。安全性的证明在第3节中通过引入适当的标记转移语义给出。最后我们得出结论并提出进一步的研究方向。2πs-微积分2.1语法本节介绍πs的语法。 我们从一组名字开始 x，y，z，.. . .我们区分了两种不同的名称：表达式名称，我们将使用a，b，c，. （并且其范围在会话和整数上）;以及信道名称，对于信道名称，我们将使用k，h，kJ，.我们也有integercon-斯坦斯，−1，0，1，.. . ，（分支）标记l，LJ，.和写入的过程变量X，Y，.值是表达式名称或整数常量，表示为用字母v，vJ，.. . .断言标签，写为L，LJ，.. . ，是值的元组，并且被写为1，...，vn. 过程表达式，用P、Q、.，定义如下：P：：=在P中请求a（k）|在P中接受a（k）|k？（x）在P中|国王！[v]; P|throwk [kJ]; P|在P中捕获k（kJ）|（νa：T）P|（νk：e）P|Kl; P|kD{11：P1Q. Qln：Pn}|停止|P|Q|定义DinP|X[→v]|开始于L;P|结束L;P概率定义式D设f∈X1[a→1]=P1，且Xn[a→n]=Pn.Remark2.1P涉及这些结合结构。n→v表示E. Bonelli et al. / Electronic Notes in Theoretical Computer Science 97（2004）175-183v1， . . . ，vn，并且对于a→i，i ∈ 1，i ∈n n. 任何两个只在其束缚名的名称上有差异的概念（称为α-等价）应被认为是相等的。 我们用符号P {a <$v}表示用v代替P中所有自由出现的a的结果，对于P{k<$kJ}也是如此。 请注意，为了清楚地介绍，我们选择了一元微积分;对多元情况的扩展应该是直接的。request原语请求名称a上的会话。当建立该会话时，新的专用信道k将用于消息交换。accept接收同名a的请求，并生成一个新的专用通道，用于建立会话后使用的消息交换request和accept构造各自绑定后续进程P中紧随其后的通道变量k的所有自由出现。消息的同步发送和接收是通过k！[v];Q和k？（x）在P中，虽然，如[14]中，翻译为具有分支的异步演算是可能的。通过信道委托约束，实现了对信道使用的线性约束的受控侧步structsthrowk [kJ];P andcatchk（kJ）inQ.用于选择标记和分支的机制可作为kl; P和kD{11：P1Q. Qln：Pn}。符号P|Q已经解释过了，我们也用stop表示不动。对于name的通常构造，我们写（νa：T）P或（νk：e）P隐藏，前者用于表达式名称，后者用于通道名称。T表示一个类型表达式（定义2.2），而E是带有e的过程的定义也可以通过defDinP构造来实现，可能会引入递归。 begin和end断言应该在πs的类型系统中用作类型指令（第2.2.1节）：beginL;P简单地断言beginL，然后表现为P;同样地，endL;P断言endL，然后表现为P。2.2类型纪律本节用对应假设丰富了[14]的类型系统，以解决引言中提到的缺点。2.2.1会话类型和效果类型系统应该在一组给定的类型假设下给一个过程分配一个结果。流程的结果反映了其未决义务。形式为beginL的断言将通过从当前对象中删除断言标签L来减少这些义务;同样地，endL将用L来增加当前对象。因此，有效性决定了必须出现的开始断言数量的下限。如果进程有一个空的输出，184E. Bonelli et al. / Electronic Notes in Theoretical Computer Science 97（2004）175-则所有结束断言对应于匹配的开始断言。如上所述，为了使两个或多个进程共享关于它们的待决或潜在效应的信息，因此，添加到通道的效应被称为潜在效应。定义2.2[带谓词的类型]断言标签、谓词和类型由以下语法给出：普通类型T：：= Int|σ（α）通道类型α，β：：= ↓ [a：T] e; α| ↑ [a：T] e; α| ↓ [α] e; β| ↑ [α] e; β|&{11：α1，.，ln：αn}e| ⊕{l1: α1,..., ln：αn}e|1| ⊥eE选e，eJ：：=（|我...，L|）1N断言标签L，Li：：= 1，.，vn类型可以是普通类型或通道类型;我们使用U，Ui来覆盖类型。一个类型U的自由名的集合，写作fn（U），像通常一样定义（见[2]）。基类型Int是整型常量的类型。会话类型被表示为σ（α），并且可以非正式地被视为表示由通道类型α及其对偶α组成的对：↓[a：T]e;α↓[α]e;β&{li：αi}edef=↑[a：T]e;α↑[a：T]e;αdef= ↑[α]e;β↑[α]e;βdef={li：αi}e{li：αi}edef=↓[a：T]e;α1def=↓[α]e;βdef={li：αi}edef=1个类型α和α应分配给通信会话的两个端点。请注意，没有定义。 通道类型由一系列输入/输出类型的值或通道或分支/选择类型组成;假设该序列以通道类型终止符1终止。 每一个都伴随着一个潜在的效应。 一个事件是多个断言标签集;我们使用（|......这是什么？|）的多集构造函数。多集减法被定义为e\eJ，最小的多集eJJ使得e≤eJ+ eJJ，其中“+”是多集并。 特殊的信道类型ESTA对已经被两个现有端点使用的“完整”或“封闭”信道进行建模，因此通过该信道不可能进行进一步的通信（参见图1）。定义2.5）。2.2.2打字规则：环境Γ是一组类型假设x1：U1·. ·xn：Un，其中x1，.，xn是不同的名称。 我们用字母“Γ”，“”，... for environments环境. 的E. Bonelli et al. / Electronic Notes in Theoretical Computer Science 97（2004）175-185r的定义域，写作dom（r），是集合{x1，. ，xn}。此外，我们为Γ分配通道类型的名称子集写domCh（Γ），为Γ分配普通类型的名称子集写domPl 在假设x：U中，x被称为主语;如果分配给主语的类型是普通类型，则假设被称为普通假设，否则它是通道假设。我们将由扩展产生的环境写成Γ·x：U对于x∈/dom（Γ），Γ的类型是一个sump t i on x：U。旋转Γ\x：U表示从Γ中删除假设x：U所产生的环境（假设它存在）。定义2.3[依赖于]xi：Ui直接依赖于Γ中的xj：Uj（记为（xj：Uj）<$→d（xi：Ui）），如果xj∈fn（Ui）。如果xi：Ui<$→xj：Uj，则称xi：U i依赖于xj：Uj，其中<$→表示<$→d的传递闭包。我们说一个环境是良构的，如果它满足以下两个条件：C1. 对于每个i∈ 1.. n，fn（Ui）是随机的（Γ）\{xi}.C2. 第七章是不忠条件C1要求所有由Γ赋值的类型中的自由名必须在Γ内声明。注意，由于通道名称可能不会出现在断言标签中（因此不会出现在fn（Ui）中），因此类型可能仅依赖于被分配了普通类型的名称。由于通过通道名的交互在线性逻辑[8]的意义上受到线性条件的限制（参见下面的Type Par规则的解释），该限制声明我们不允许依赖于线性假设（然而，我们允许依赖于简单或“直觉”假设的类型）。我们的类型学科的预期应用不会受到这样一个限制的干扰，并且不清楚解除它所导致的元理论的技术复杂性是否超过了它的好处。事实上，这种限制已经出现在线性和直觉假设共存的其他环境中，例如[3]的线性逻辑框架。第二个条件C2要求Γ没有循环依赖。这是通常通过将环境表示为类型序列来保证假设，其中假设x：U仅取决于出现在其左侧的假设。这样的表示似乎不适合存在通道类型的环境，因为关于结构规则可容许性的基本结果失败了（注2.6）。7R <$A × A是非自反的i <$，对于每个x ∈ A，不是xRx的情况。186E. Bonelli et al. / Electronic Notes in Theoretical Computer Science 97（2004）175-πs型系统由以下四个判断组成：格式良好的环境Γ和过程协议ΘΓ格式良好的环境V：类型T的T良好类型化的值V当e为良型过程P的参数s→v时，r∈（→a：T→）r ∈θ P：e为良型过程P的参数s→v时，r∈ θ（→v）：（→a：T→）r∈ ΘP：e为良型过程字母Θ代表过程协议：一组形式为Xj：（→aj：T→j）的表达式，其中j∈1。n，其中a ch→aj：T→j i是向X j指示过程参数的类型的指示符。如果Γ是一个良构的虚拟机，并且在每个事件的协议Θ是良构的情况下，所有的虚拟机t→aj：T→j都成立，则判定Γπs的类型规则如图2所示。 规则Type Acpt和Type Rcv在环境中引入了一个新的通道名，从而保证了会话使用的是私有通道。请注意，双通道类型用于请求方和接受方。类型Bgn和类型Enda assertion通过消除或添加新的断言标签来处理效果 规则Type Snd和Type Rcv允许为发送和接收数据键入通信原语。请注意，数据仅通过通道发送和接收。此外，注意，类型Snd的右上判断中的k的类型是α{a ← v}，反映了信道类型的“其余”（即α）可以取决于输出值v的事实。同样的注释也适用于Type Rcv规则。 类型Brnch和类型Sel分别键入分支和选择原语;如果挂起的事件被视为信用，那么很明显，类型Brnch中的每个分支的事件必须被连接。通道委托是通过throw和catch原语来实现的，这些原语通过类型Thr和类型Cat来类型化。规则Thr型受到β1的限制;这限制了通道，通过这些通道可以进行通信，即没有频道8.通道和名称限制（对于非通道名称）按预期键入。Type Stop键入无动作停止;它要求通过通道名称的所有通信都已完成。Type Subsum规则允许增加过程术语的必需断言义务。 类型参数规则类型的两个进程的并行执行。 一个通道可以由两个进程P或Q中的一个进程使用。这个规则的唯一例外是当P和Q都使用双类型的通道k时。由于必须限制信道使用以保证这种线性使用，因此环境Γ和ΓJ[8]从技术上讲，这使我们能够纠正[14]中存在的一个问题，即主语同余的失败。E. Bonelli et al. / Electronic Notes in Theoretical Computer Science 97（2004）175-187必须兼容。定义2.4[兼容性=]关系=定义如下：=，且Γ= ΓJ意味着(i) Γ·a：T=ΓJ·a：T(ii) Γ·k：α=ΓJ·k：α(iii) r·k：α= rJ，ifk∈/dom（rJ）(iv) Γ= ΓJ·k：α，ifk∈/dom（Γ）请注意，兼容性的概念对于两组不一定构成良构环境的配置是有意义的一旦这个兼容性的概念到位，我们可以定义如何通过环境组合来组合两个环境。定义2.5[合成]设Γ，ΓJ是两个环境，使得Γ=rJ. 我们定义Γ rJ如下：(i)（Γ·a：T）（ΓJ·a：T）=（Γ ΓJ）·a：T(ii) （Γ·k：α）（ΓJ·k：α）=（ΓΓJ）·k：fnMult（α）(iii) （Γ·k：α）n（ΓJ）=（ΓΓJ）·k：α，ifk∈/dom（ΓJ）(iv) r∈（rJ·k：α）=（r∈rJ）·k：α，ifk∈/dom（r）集合fnMult（α）是一个多重集合，它包含了一个自由名在α中的每一次出现的标号。定义2.5的第二个子句的其他变体是可能的，只要“”的输出下标忠实地记录了它所产生的双通道类型的名称依赖性（即没有依赖性信息丢失）。为了可读性，在图2中，我们省略了假设，即规则的结论的环境是良构的，对于所有那些结论的环境与所有假设的环境不同的规则。请注意，在后面的一些规则中，条件是超连续的，即CRes型，Par型，Subsum型，PVar型和Def型。注2.6基于假设序列的环境表示，通常在依赖类型系统的文献中采用，不适用于我们的系统。 理由是，基本结果就可受理结构性规则失效。特别是，交换引理，它指出，独立假设的顺序是无关的，为了可导性，失败。实际上，考虑在以下公式中制定的以下可能的类型规则类型Snd：188E. Bonelli et al. / Electronic Notes in Theoretical Computer Science 97（2004）175-Γ·a：σ（α）·k：α<$ΘP：eΓ·a：σ（α）<$Θ在P：e中接受a（k）Γ·a：σ（α）·k：α<$ΘP：eΓ·a：σ（α）<$Θ在P：e中请求a（k）类型Acpt类型要求[001 pdf1st-31files][001pdf 1st-31files][001 pdf1st-31files][001 pdf 1st-31files]（|L|）Bgn型01-02|L|）式端Γ θ v：TΓ·k：α{a←v}<$Θ P：eΓ·k：↑[a：T]eJ;αθk！[v];P：e+eJ{a←v}r·a：T·k：αθP：efn（e\eJ）随机域（r）r·k：↓ [a：T] eJ; αθk？（y）在P中：e\eJ类型Snd类型Rcvr·k：α1<$ΘP1：e1... Γ·k：αn<$ΘPn：en_类型Brnchr·k：&{11：α1，.，ln：αn}eJθk{l1：α1，.，ln：αn}：（ei）\eJΓ·k：αj<$ΘP：e（1≤j≤n）r·k：n {l1：α1，.，ln：αn}eJ<$Θ k <$lj; P：e +eJr·k：αθP：e类型选择Γ·kJ：β·k：↑[β]eJ;αθthrowk[kJ];P：e+eJ类型ThrΓ·kJ：β·k：αθP：eP：e\eJ中的Γ·k：↓[β]ej;α<$Θcatchk（kJ）ranCh（Γ）<${1，<$e}r·k：e'θP：eΓ·a：TθP：eΓ ►Θstop：（||）类型止动件Γ θ（νa：T）P：e类型NResΓ θ P：erJθ Q：eJr=rJfn（eJ）随机数（Γ）ΓκΘ（νk：κe'）P：e型CRΓθP：e e≤eJfn（eJ）随机（Γ）ΓπθP：eJI|Q：e + eJ类型子和式停车Γθ（→v）：（→a：T→）X：（→a：T→）∈ΘranCh（Γ）<${1，<$e}[001 pdf 1st-31files]||)PVar型（1）A =（1）A=（1）A=（||)Θ（Xi）=（a→i：T→i）ΓθQ：eX1（a→1）=P1. . 和d. . . Xn（a→n）=PninQ：e类型定义E. Bonelli et al. / Electronic Notes in Theoretical Computer Science 97（2004）175-189图二. 格式良好的进程表达式190E. Bonelli et al. / Electronic Notes in Theoretical Computer Science 97（2004）175-1 2Θ1 2 Θ 1 2 Θ 1 2Θ1−→−→−→Γ·a：TθoΓ·a：TτΘa：TWf确认名称伊戈奥n∈Z中文（简体）Wf Val Int伊戈奥Γθ（）：（）Wf PP无Γθ（→v）：（→a：T→）Γθv：T{→a←→v}b∈/{→a}dom（Γ）Wf PP ConsΓθ（→v，v）：（→a：T→，b：T）图三. 格式良好的值和过程参数一种环境是序列的设置：Γ·Γ►v：TΓ ·k：α{a←v}·r►P：e<$·k：↑[a：T]eJ;α·<$r·k：↑[a：T]eJ;α· r ►国王！[v];P：e+eJ{a←v}假设r1= ΓJ·v：T.然后注意v：T和k：↑[a：T]eJ;α满足交换引理的条件，因为两者都不依赖于另一个。然而，当我们试图在中上判断中交换v：T和k：α{a<$v}时，我们失败了，因为α{a<$v}可能有v的自由出现。注意，这些问题并没有出现在并发/分布式演算的对应断言的先前类型理论公式中，因为没有考虑长期会话类型。3πs的安全性证明为了跟踪某些动作的执行，例如开始和结束断言，我们将为πs引入标记转换语义[10]（LTS）。LTS被定义为模结构同余，并将用于形式化安全进程的概念，并表明所有具有空对象的可类型进程都是安全的。过渡系统的作用，用字母φ，φ，.表示。. ，分别是：开始L• P−→PP到达开始L断言。• P端LPJP到达结束L断言。res（a：T）• P−→PP生成一个新的会话名a。• Pres（k：ke）PJP生成新的信道名称k。τP JP执行内部动作。因此，动作的集合是beginL，endL，res（a：T），res（k：ke），τ。 的πs的标号跃迁系ψ在图4中给出;我们写P-→PJ当P通过作用量PJ减少到Pj。同一个图形定义了动作的自由名和生成名• PJJE. Bonelli et al. / Electronic Notes in Theoretical Computer Science 97（2004）175-191−→−→−→−→−→−→−→−→−→−→fn（τ）def=deffn（beginL）=fn（L）fn（endL）=fn（L）fn（res（a：T）） ={a}fn（T）fn（res（k：k））= {k}fn（e）defgn（τ）gn（beginL）gn（L端）gn（res（a：=def=defdef=defdef={a}defgn（res（k：ke））={k}def（接受P1中的a（k））|（求P 2中的a（k））τ（νk：νe）（P1|P2）跨链路（k！[v]; P1）|（k？（a）在P2）τ中P1|P2{a ← v}传输通信（k <$li; P）|（k）{11：P1 Q. Q ln：Pn}）τP|Pi，如果i ∈ 1。n 跨线桥（throwk [kJ]; P1）|（catchk（kJJ）inP2）τP1 |P2 {kJJ<$kJ}跨接defDin（X[→v]|Q）τifX（→a）=P∈D开始LdefDin（P{→a←→v}|Q），TransDef1beginL;P−→PTrans Begin左末端P变速器端（νa：T）Pres（a：T）−→P反式ResNres（k：k）（νk：εe）P−→P反式ResChψP−→PJ反式Def2ψdefD inP−→ defDinPJψP−→PJTrans Par，ifgn（）fn（Q）=ψP|Q −→ PJ|QPPJPjQJQjψ反式P−→Q见图4。 πs的LTS可以用迹线来跟踪转变的序列。迹s是一个序列...一系列行动。我们使用空的跟踪。自由的名字（Resp.）生成的名称）的跟踪对象1. n被定义为fn（fn（（分别） gn（1）. [1]）。 跟踪转换是一系列操作：定义3.1[有迹跃迁]如果Ps，则P用迹s还原为PJPJ，其中s定义为：PPJPPJ跟踪PsJJ.S.J−→Q，Q−→PP−→P跟踪操作， 其中，fn（n）gn（s）=为了确定一个进程何时是安全的，我们需要计算def开始 第一个定义是开始（11... n）=def192E. Bonelli et al. / Electronic Notes in Theoretical Computer Science 97（2004）175-开始（1）. 第一个开始（n），第二个结束（1）。n）= ends（E. Bonelli et al. / Electronic Notes in Theoretical Computer Science 97（2004）175-193−→−→−→−→ΘΘ... --defdefbegins（beginL）begins（endL）begins（res（u））begins（τ）=（|L|） end（beginL）def=（||）结束（结束L）def=（||）ends（res（u））def=（||）ends（τ）=（||）def=（|L|）def=（||）def=（||）定义3.2[安全进程]一个进程P是安全的，当且仅当对于所有迹s和过程PJ，如果P sPJ，则结束（s）≤开始（s）。因此，如果每个结束L都被相应的开始L所占，则过程是安全的。例如，beginL;stop是安全的，但beginL;endL;endL;stop不是。现在我们来讨论安全性的证明，也就是说，一个类型为null的进程是安全的。这需要首先证明过程缩减保留了类型和效果。定理3.3设ΓθP：(i) （主语同余）如果P<$Q，则Γ <$ΘQ：e。(ii) （受试者减少）(a) 如果PτPJ，则ΓJ<$PJ：e，其中ΓJ和 Γdi仅在分配给通道类型“”的项（如果有）。开始L(b) 如果P−→PJ，则为Γ2016-05-2501：01：02（|L|）的。(c) 如果P结束LPJ，则为Γ2016 - 05- 2201：01：02 |L|）和L ∈ e.res（a：T）(d) 如果P −→PJ和a∈/dom（Γ），则nΓ·a：T∈PJ：e。res（k：k）(e) 如果P −→PJ和k∈/dom（Γ），则nΓ·k：n∈f►PJ：e。主语同余是在PQ的推导上用归纳法证明的;当环境被组合时，主语同余不会丢失这一事实（定义2.5）对证明是至关重要的。主语归约是根据所发生的动作用案例来证明的（见[2]）。最后，我们可以把结果放在一起，得到主要结果