基于会话类型的全局演算：通信为中心的程序设计与业务协议形式化描述

理论计算机科学电子笔记171（2007）127-151www.elsevier.com/locate/entcs基于会话类型MarcoCarbone Kohei Honda2，b Nobuko Yoshida3aa联合王国伦敦大学玛丽皇后学院计算机科学系英国伦敦摘要本文提出了一个演算描述通信为中心的程序，并讨论了它的使用，通过正式描述的几个用例，从真正的业务协议。形式主义，称为全球演算，旨在表示全球信息流结构化的通信。全局演算起源于编排描述语言（CDL），它是由W3C的WS-CDL工作组开发的一种Web服务描述语言。它的类型规则基于会话类型，这些会话类型在π演算的背景下已经研究了多年[15，10，22，6]。会话类型为复杂的通信行为提供了高层次的抽象和衔接，并在指导程序员对业务协议进行清晰、结构良好的描述方面保留字：Web服务，以通信为中心的编程，π演算，会话类型。1引言本文的目的是介绍一种基于通信的演算，从根本上区分现有的并发形式主义。这种演算是与W3C的Web服务标准工作组对话的结果，它基于交互的全局描述的思想。正如它在W3C标准化中的起源所表明的那样，这种形式主义是描述可能发生在现实世界业务流程中的复杂交互的工程需求的升华。相关的长版本[9]提出了广泛的例子，1电子邮件地址：carbonem@doc.ic.ac.uk2电子邮件地址：kohei@dcs.qmul.ac.uk3电子邮件地址：yoshida@doc.ic.ac.uk1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.12.041128M. Carbone等人理论计算机科学电子笔记171（2007）127以建议的全局形式主义编写的业务协议，以及与标准过程形式主义（π演算）的本 工 作 的 直 接 工 程 背 景 是 Web Services Chore- ography DescriptionLanguage，通常缩写为WS-CDL [23]，这是一种基于XML的Web服务描述语言，由W3C的WS-CDL工作组与包括本作者在内的受邀科学家合作开发WS-CDL具有为了满足在万维网上开发业务协议的工程需要而开发WS-CDL的核心工程思想体现在其名称中的术语编排中。基本的直觉可以概括为：“舞者在没有单一控制点的情况下跟随全球场景跳舞。WS-CDL是关于写下这样一个“全局场景”的：在计算术语中，它是一种从全局角度描述业务协议的语言，这样描述就可以通过分布式进程之间的通信来执行，而无需单点控制。换句话说，如果设计者在WS-CDL中编写全局描述，那么它应该可以实现为没有任何中央控制代理的通信进程（这与编排的概念形成对比，其中一个主组件因此，编排的概念本质上要求在每个位置正确实现全球协议的实施框架为此，类型在WS-CDL中扮演着基础性的角色目前工作的一个更广泛的背景是互联网和世界范围内的爆炸性增长这种工程背景使得开发将参与两方或多方之间的复杂交互序列的应用程序另一个背景是以π-演算及其类型为中心的过程理论的成熟。引入的形式主义是基于结构化通信的概念，称为会话。会话将两方之间的一系列通信绑定为一个，将它们与属于其他会话的通信区分开来。这是商业协议（其中协议的实例应该与相同或其他协议的另一实例区分开）和分布式编程（其中两个交互方使用多个TCP连接来执行一个单元的会话）中的标准实践。会议的类型纪律已经研究了多年，π演算的背景[15，10，22，6]，其中已经表明，它们不存在通信行为的高级抽象，可以在此基础上建立进一步的细化推理技术。不仅会话OCHELER一个自然的关节的描述复杂的交互行为的全局描述，但也会话类型在所提出的理论指导程序员走向正确的实现业务协议中发挥着至关重要的作用。本文介绍了形式演算和会话类型的概念，并通过实例对那些没有进程演算及其类型系统背景的人进行了说明。第2节和第3节介绍并说明了全局形式主义（WS-CDL的精简版本）。第4节说明了演算的会话类型。最后，第5节通过展示一个受M. Carbone等人理论计算机科学电子笔记171（2007）127129WS-CDL的用例及其作为通信过程的实现进一步的例子和形式主义理论基础的完整技术发展可以在[9]中找到。相关工作。除了WS-CDL之外，用于描述通信的全局方法已经在不同的工程场景中代表性的例子包括消息序列图（MSC）[14，1]和UML图。这些符号在设计/规范阶段提供了有用的帮助，但并不打算作为完全边缘化的编程语言，缺乏例如通用控制结构和/或值/状态操作的符号。Petri网[21]也可以被看作是一种全局描述，尽管它们作为一种规范/分析工具更有用DiCons是一种用于互联网应用程序全局编程的符号[2]。Di-Cons选择使用接近用户体验的编程原语，例如Web服务器调用，电子邮件和Web表单归档，而不是一般的其语义由MSC或直接操作语义给出。DiCons不同于我们的全局演算，因为它不使用面向通信的类型，并且它旨在用于特定的应用领域，而不是作为通用演算呈现。目前的工作与许多最近的作品在其使用类型的良好结构的通信为中心的编程[19，3]。特别是，我们的工作是基于会话类型学科的研究[20，15，11，10，22，6]，并将其扩展到全局描述和会话内并行通信。所有以前的工作都是基于端点语言和演算。Fournet、Gordon、Bhargavan和Corin研究了Web服务的安全相关方面。在他们最近的工作[5]中，作者使用ML方言实现了部分WS-Security库，并展示了如何通过转换为安全增强的π演算来分析这些安全库的注释应用程序级使用的安全属性。Laneve和Padovani [16]给出了一个Web服务编排的模型，使用π演算的扩展来连接模式。他们提出了一种类型系统，用于保证平滑度的概念，即对输入连接模式的约束，使得它们的主题（通道）位于同一位置，以避免通信期间的经典全局共识问题。Busi等人[8]研究了Web服务上下文中的编排和编排之间基于双模拟的对应关系，其中在编排模型的语义中使用了状态变量的概念。它们在操作上将编排与编配联系起来。在[12]中，同一作者介绍了SOCK，一种基于端点描述的Web服务演算。这种形式主义模型网络的参与者和他们的本地行为增强了一种机制，用于控制通信在运行时的基础上的逻辑条件的参与者在我们的工作中，通信结构被抽象为会话类型。使用会话类型，可以通过类型推断算法静态地保证错误自由度。他们的动态控制允许具体的推理130M. Carbone等人理论计算机科学电子笔记171（2007）127通信值，但可能需要大量的运行时机制。这是一个有趣的话题，整合这两种方法的相互作用的有效和灵活的控制。正如我们所指出的，全局标记法经常用于表示安全原型，最近有几个作品对此进行了形式化。Briais和Nestmann [7]提出了一种用于表示协议叙述的全局 符 号 ， 并 将 其 与π 演 算 联 系 起来 。 由 于 他 们唯 一 的 重 点 是 加 密pro-toeconomy，他们的全球形式主义并不打算作为一个完全表达的语言来描述通信为中心的软件行为。具体地说，他们的形式主义不包括诸如基于通道的通信、条件、分支/选择、循环以及通信的类型纪律等概念串空间[13]是分析密码学原型性质的数学结构。它将密码协议建模为交互的因果链，并且通常以类似于UML序列图的全局符号表示。串空间本身并不是以通信为中心的程序的描述语言然而，他们的安全分析方法可能适用于我们的全球演算。2全球微积分2.1基本思路在本节和下一节中，我们将介绍全局演算的语法、动态语义和静态语义。语法定义了一组术语，其中每个术语描述了两个或多个参与者之间的交互在全局演算中，对交互的描述集中在会话的概念上，在会话中，两个交互方建立一个私人连接，用于进行一系列交互，可能与其他会话交织。更具体地说，进程首先为新创建的会话交换新的会话通道，然后将它们用于属于会话的交互（这相当于更隐式的框架，其中消息内容中的身份令牌用于表示会话）。例如，卖方和买方之间的一个简单协议可以表示为一个术语，称为交互：买方→卖方：serve（vs）。买家→卖家：sRequestQuote，productName，x.Seller→ Buyer：sReplyQuote，productPrice，y. 0（一）在上述（1）中，买方要求服务器创建新的会话信道s，该信道将用于会话中消息交换。因此，买方要求对产品报价，指定产品名称，并通过相同的渠道，M. Carbone等人理论计算机科学电子笔记171（2007）127131a卖方回复报价值。 在一次互动中：买家→卖家：sRequestQuote，productName，x这里Buyer指定发送者，Seller指定接收者，s指定会话标识符，RequestQuote指定操作名称，productName指定要发送的值，x指定接收者端的变量，一旦发送完值，该变量就会被填充。一旦给定了术语，动态语义就具体化了全局演算背后的“计算”的抽象概念。这被表示为从全局描述到另一全局描述的转换，执行交互的每个步骤（例如，消息的交换）。由于每个参与者可以拥有其自己的局部变量，因此这种转换还可以涉及所涉及的参与者的局部变量的收集。动态语义使用直观的符号来定义（σ，I）→（σJ，IJ）这意味着状态σ（参与者的所有局部状态的集合）中的全局描述I将被改变为IJ，并产生新的配置σJ。这个想法来自命令式语言的小步语义。全局演算的静态语义将类型分配给格式良好的术语。由于演算是基于会话的，我们使用一个类型discpline，在这里我们将会话中双方之间的交互的结构化序列表示为一个类型。这里的“类型”是指对交互描述的语法注释：在本例中，该注释描述了服务接口（或共享服务通道）的抽象概念，并且通过遵循其语法结构的每个描述的类型规则来推断。例如，以上面的示例1为例，s处的交互可以通过以下会话类型来抽象：Strings（String s）. s↓ReplyQuote（Int）（2）（2）中的会话类型抽象了在ch处执行的动作序列，指定了以下抽象行为：首先发送（“↑“）一个操作名为RequestQuote的字符串，然后接收（“↓“）一个操作名为ReplyQuote的整数。请注意，此抽象是从买方的角度给出的同样，我们可以从卖方的角度提出抽象Strings（String s）. s↑ReplyQuote（Int）（3）这只是颠倒了信息流的方向注意，这样，就有了与会话类型相关的二元性的自然概念[15]。132M. Carbone等人理论计算机科学电子笔记171（2007）1272.2形式语法全局演算的形式语法由标准BNF给出 下面的符号I，IJ，. 表示全局演算的项，也称为相互作用。术语从全局的角度描述两个或多个当事人之间的信息交换过程.I：：=A→B：ch（νs）。I（ini t）| A → B: s⟨op, e, y⟩. I（com）| x @ A := e. I（分配）| if e @ A then I1else I2(ifthenelse)| I1+ I2(sum)| I1|I2（标准杆）| (νs)I(new)| X(recVar)| rec X. I（rec）| 0(inaction)上面的语法使用以下符号4：• a，b，c，ch，. 在服务信道（也称为会话发起信道）的集合Ch上的范围。它们可以被认为是网络服务的共享通道。• s，sJ，. 在会话信道的集合S上的范围。会话通道desig- nate通信通道新鲜生成的每个会话。它们可以以各种方式实现：在TCP中，相同的概念通过所谓的连接（也称为会话）实现。在Web服务中，它们是通过将新生成的身份信息作为消息的一部分发送来实现的。• A，B，C，. 在参与者的集合P上的范围。参与者是那些与他人进行通信的人，每个人都有自己的地方状态。每个参与者可以具有使用多个通道的多于一个的交互线程。• x，y，z，. range在变量的集合Var上，这些变量接近于传统编程语言（如Pascal和C）中的变量，因为它们的内容是可更新的。• X，Y，Z，.在一个术语变量的集合上的范围，这些术语变量用于与递归recX.I.注意，术语变量出现时带有参与者注释。• e，eJ，. 在表达式上的范围，由语法e给出：：=X|v| f (e1,...，e，k），其中f的范围在适当的函数符号集合（包括标准算术/布尔运算符）上，并且v，w，. 原子值比如自然数和布尔数。4 作为标准，我们假设在每个句法范畴中有无限的不同符号供应。M. Carbone等人理论计算机科学电子笔记171（2007）127133以上语法中的每一个结构都将在下一小节中进行说明。我们写A → B：sop。当表达式e和变量x在A → B中不重要时：sop，e，x。 I.2.3插图：这是一个新的工作流程，它会导致重复的通信。首先，A→B：b（νsε）. I指示A在B处调用服务通道b，并且发起将使用由I进行的会话的新会话。子会话中的子会话导致这些会话被记录在子会话中（我可以拥有属于不同会 话 的 子 会 话 ） 。 在 本 研 究 的 主 要 部 分 ， 我 们 将 讨 论 A 和 B 的情 况 。Asshouldbe l oc a l t o the sssi on（i. e. 我们不知道我们是谁），我们是一个chsi∈st o bbondI。其次，A→B：s op，e，y表示A的发送动作，A的消息由一个选定的操作符op组成，接收者B。 表达式e的值（只能使用位于A的变量）被赋值给变量y（必须位于B）。第三，另一个基本操作是赋值x @ A：= e。I.该操作在指定参与者（上面的A）处是本地的，其中A处的变量x使用也位于A处的e的评估结果进行更新。我们可以使用条件ife@AthenI1elseI2或求和I1+I2来分支动作过程。第一个操作对e求值一次，如果它的值为真，则执行分支I1，否则执行分支I2。注意，条件e位于A。第二个操作通过非确定性地表现为I1或I2来隐式地选择其中一个分支。求和算子+是交换的和结合的，所以我们经常把相互作用的n重和写为iIi术语I1|I2表示平行组成。但是，与标准的进程演算不同，I1和I2之间没有通信：I1|I2仅仅意味着两个独立的交互线程。（νs）I表示会话通道的限制（或隐藏），其中（νs）绑定I中s的自由出现。这用于指定新创建的会话通道，其中会话正在初始化d。 这是一个非常重要的问题。由于只有当最外层的初始化前缀减少时才添加限制，因此很自然地假设限制永远不会在前缀初始化、通信和赋值时发生，也不会在求和的被加数中发生。可以无限重复的相互作用是通过递归实现然后是术语rec X。 I是标准的递归结构，其中rec X被称为recur- sor，其中X是递归变量，将其自由出现绑定在I中。最后，0是不作为，代表缺乏行动。5如果我们希望描述参与者之间的交互，这是一个自然的约束，这通常是许多业务协议的唯一焦点。当我们允许参与者内部的互动时，本研究的理论框架完好无损。134M. Carbone等人理论计算机科学电子笔记171（2007）1272.4示例我们通过简单的例子来说明语法。这些示例将在整个论文中作为运行示例使用。例1（1）考虑以下交互作用：{买方→卖方：B2 Sch报价接受，100，x。 I1}+{买方→卖方：B2 Sch报价单，xAbortNo，y. I2}（四）在本例中，Buyer和Seller是参与者，B2Sch是会话通道名称，QuoteAccept和QuoteExcept是操作名称。因此，作为一个整体，（4）可以读作如下：通过会话通道B2Sch，买方选择卖方提供的两个选项之一，报价接受和报价。 如果选择了第一个选项，买方发送报价“100”，卖方将其存储在x中，并继续进行I 1。在另一种情况下，Seller发送存储在变量x AbortNo中的中止号，该变量将由Seller存储在y中，并继续进行I2。我们将sum +解释为买方的内部sum（即买方发起此选择）和卖方的外部sum（即卖方被动地等待环境选择其中一个分支（操作符））。实施例2（1，2）以下是对上述描述的改进：如果x报价≤1000 @买方，则{买方→卖方：B2 Sch报价接受，100，x。 I1}其他{买方→卖方：B2 Sch报价单，xAbortNo，y. I2}（五）这个描述现在具体说明了为什么每个分支被采用的“原因”。请注意，条件分支中的条件x≤1000是明确定位的：描述中说这个判断发生在买方。还请注意，描述仍然是卖方的外部选择：买方选择其中一个选项，卖方被动地等待。通过添加首字母，M. Carbone等人理论计算机科学电子笔记171（2007）127135在服务通道（比如CH）处的会话调用以及对报价的请求。买方→卖方：ch（ν B2Sch，S2Bch）. Seller→ Buyer：S2BchQuote，100，y. 如果x报价≤1000 @买方，则{买方→卖方：B2 Sch报价接受，100，x。 I1}其他{买方→卖方：B2 Sch报价单，xAbortNo，y. I2}（六）在这里，买方调用卖方发起与会话通道B2SchS2Bch。示例3（C，3）一个会话可以有多个会话名称用于通信。这是业务协议和其他以交互为中心的应用程序中的标准实践，对于在单次会话。例如，假设买方希望在通道访问中启动会话，在该会话中，买方在会话名称Op上传达报价接受，并在会话名称Data上并行发送其地址。这可以表示为：买方→卖方：acc（νOp，Data）。{买方→卖方：OpQuoteAccept，100，x. 0|买方→卖方：数据库报价接受，地址，y. 0}（七）这里，两个会话信道Op和Data在信道acc处的会话发起时被传送。其他构造的例子，如递归和隐藏，将在最后一节给出3全球微积分3.1Reduction的基本思想从工程的角度来看，动态语义确定了一个数学概念，设计者，实现者和用户可以参考，当他们希望讨论的动态行为的描述与严谨。例如，这将允许我们精确地陈述一个实现的程序是否符合描述。另一个例子是在监视中，监视器将根据给定描述的规定的形式化动态语义来检查执行。全局演算中的计算由一步一步的转换来表示，每一步都由执行一个原语操作组成，例如通信、赋值或条件，这些操作对所涉及的参与者的局部状态有影响。136M. Carbone等人理论计算机科学电子笔记171（2007）127为了形式化这个想法，我们使用了一个配置，它是一对状态（所有参与者的局部状态的集合）和一个相互作用，写为（σ，I）。 形式上是一个状态，范围为σ，σJ，.。. 是从V ar× P到V al的函数，即每个参与者处的变量在存储中被分配一个值。我们将写σ@A来表示σ局部于A的部分，而σ[y@A<$→v]表示一个新的状态，除了σJ（y，A）等于v之外，它与σ相同。动力学定义为以下形式：（σ，I）→（σJ，IJ）这意味着在配置σ中，I执行一步计算（可以是赋值、交互等）。并变为具有新配置σJ的IJ。这个关系称为归约或归约关系6。例如通信action将改变状态和词形：（σ，A→B：s send，3，x.I）→（σ[x@B<$→3]，I）表示：“A变量x在B处，剩余相互作用为I注意，通信动作是自动发生的，而不是先单独进行发送和接收动作，然后再进行同步。分配的处理方式类似。（σ，x@B：= 3.I）→（σ [x@B<$→ 3]，I）由于定位了一个赋值，因此只有B处的x被更新，并且下一个交互我是展开的。相互作用可以涉及选择，其中一个分支是非确定性选择的，即我们可以有：（σ，I1+I2）→（σ，I1）或（σ，I1+I2）→（σ，I2）这两个都是合理的削减。条件依赖于表达式的求值。例如，当x在A存储0时，我们有（σ，如果x @ A = 0，则A → B：s= 0，3，x= 1，否则. ）→（σ[x@B<$→ 3]，I1）但如果A处的x存储为1，则将选择第二个分支对于递归，我们期望一个重复的行为。例如，下面的行为只是继续将1赋值给变量：（σ，recX.x@B：= 1.X）→（σ[x@B<$→ 3]，recX.x@B：= 1.X）在下面的小节中，我们将逐一说明每个构造的归约概念。[6]“归约”一词虽然它并不完全适合交互计算，我们使用的术语从公约和我们的尊重的基本形式主义，开始语义研究。M. Carbone等人理论计算机科学电子笔记171（2007）1271373.2减少规则。约简关系的定义是每个结构有一个规则，以及相关的规则。首先，我们有一个会话发起通信的规则：（INIT）−（σ，A→B：b（νsε））. I）→（σ，（νsε）I）其中，视频是一种针对新的或更高级别的视频的矢量，它会使视频内容变得更紧凑。规则是，在A与B通信以用于利用新会话信道S进行会话发起之后，A和B共享呼叫（通过新会话信道来标识），并且该索引未被实现。状态σ保持原样，因为没有值的通信发生。我们已经看到了一个表示通过会话通道进行通信的约简示例。我们现在报告正式规则：（COMM）σe@Av（σ，A → B：sop，e，x. I）→（σ [x @ B <$→ v]，I）上述规则的前提使用判断（称为评价判断）：σe@Av它说：表达式e被求值为状态σ的A部分中的值v。例如，如果σ表示A存储3时的x，则我们有σ（x+x）@A6。因此，要传递的表达式在状态的源部分中求值：而传递的值在状态的目标部分中赋值赋值的形式规则如下：（ASIGN）σe@Av（σ，x @ A：= e. I）→（σ [x @ A <$→v]，I）其更新参与者A处的状态并展开下一交互。条件表达式的规则再次使用求值判断，假设条件表达式的求值结果是tt（表示真）或tt（表示假）。在前者中：（IF TRUE）σe@Att（σ，如果e@A，则Ielse1I2）→（σ，I1）对称地，当条件计算为false时：（IF FALSE）σe@A（σ，ife@AthenIelse1I2）→（σ，I2）求和的规则是标准的：（SUM）−（σ，I1+I2）→（σJ，I1）138M. Carbone等人理论计算机科学电子笔记171（2007）12711对称规则包含在结构同余中，结构同余将在后面介绍。对于并行合成，该规则仅通过考虑两个分量的交织来定义。因此，我们定义：（PAR）（σ，I1）→（σJ，IJ）（σ，I1|I2）→（σJ，IJ|（二）在这里我们减少左手边。对称规则又被我们后面规定的结构规则所包含。对于限制，我们有：（RES）（σ，I）→（σJ，IJ）（σ，（νs<$）I）→（σJ，（νs<$）IJ）也就是说限制并不是一种彻底的减少。对于递归，我们使用标准的展开规则。（REC）（σ，I[recX.I/X]）→（σJ，IJ）（σ，recX.I）→（σJ，IJ）规则规定：如果recX.I，I [recX.I/X]（用recX.I代替I中的每个自由X）在σ下的开折约化为IJ，其结果状态为σJ，则recX.I本身在σ下将达到（σJ，IJ）。最后，不作为0没有任何减少。我们还使用下面的规则，它说当我们减少时，我们采取一定的平等，遵循[4，17]。（S结构）I<$IJJ（σ，I）→（σ，IJ）IJ<$IJJJ（σ，IJJ）→（σJ，IJJJ）其中，结构平等由以下规则定义：• IIJ（IαIJ）• I+II，I1+I2I2+I1，（I1+I2）+I3I1+（I2+I3），• 我|0I，I1|I2I2|I1，（I1|（二）|I11 2 3|（一2）|I3），（（νs）I1）|I2（νs）（I1|I2），其中s/∈ fn（I2））在最后一条规则中，fn（I）表示I中出现的自由名称（包括变量、通道和会话通道）。关系式是包含上述方程的项的最小同余。 虽然在约简规则中使用结构规则的好处在目前的上下文中是有限的（与标准过程演算相比），但考虑到最大的项通常是自然的，并在实践中增加了清晰度。M. Carbone等人理论计算机科学电子笔记171（2007）127139121=03.3减少的例子例4（约简：沟通）回想例1中的以下术语：defI0={买方→卖方：B2 Sch报价接受，100，x。I1}+{买方→卖方：B2 Sch报价单，xAbortNo，y. I2}（八）我们推断出I0的减少。每个分支有一个减少。对于第一个被加数，我们记为σ100@Buyer100，并使用（COMM）分两步进行推断：（σ，I0）→. →（σ[x@Seller <$→ 100]，I1）（9）类似地，我们对第二分支有以下约简。假设xAbortNo在σ中的买方处存储（例如）28，因此σxAbortNo@Buyer 28，（σ，I0）→（σ[y@卖方<$→ 28]，I2）（10）实施例5（还原：条件）我们现在显示实施例2的还原。首先，我们重新定义术语。J定义0如果x报价≤1000 @买方，则{买方→卖方：B2 Sch报价接受，100，x。I J}其他{买方→卖方：B2 Sch报价单，xAbortNo，y. I J}（十一）如果我们选择σ@Buyr（xquote）=800，则新的w可以在feryrule（IFTRUE）中：σ（800≤ 1000）@买方交货（σ，IJ）→（σ，买方→卖方：B2SchQuoteAccept，100，x. （ 12）01进一步将（C OMM）应用于所得到的配置，我们得出：（σ，IJ）→（σ，买方→卖方：B2 SchQuoteAccept，100，x。 I J）01→（σ[x@Seller<$→ 100]，IJ）在这种情况下，这是来自（σ，IJ）的仅有的约简序列 假设另一个h和σ@Bu yer（xquote）=1200。新版本有以下规则（如有）：σ（1200≤ 1000）@买方交货期（σ，IJ）→（σ，买方→卖方：B2Sch报价单，x，y。（13）0因此，在这种情况下，我们有：AbortNo2（σ，IJ）→（σ，买方→卖方：B2 Sch报价单，xAbortNo，y。I J）02我140M. Carbone等人理论计算机科学电子笔记171（2007）127→（σ[y@Seller<$→ 28]，I2）这也是在该假设下唯一可能的归约序列。M. Carbone等人理论计算机科学电子笔记171（2007）127141=实例6（约简：Init、Par和Struct）接下来考虑实例3：J0=买方→卖方：acc（ν Op，Data）.{买方→卖方：OpQuoteAccept，100，x. 0|买方→卖方：数据库报价接受，w地址，y。0}（十四）我们用J1和J2表示平行合成的两个分量.然后，通过（INIT），我们得到：（σ，J0）→（σ，（νOp，Data）（J1|（15）通过（COMM），我们有：（σ，J1）→（σ[x@Seller<$→ 100]，0），因此通过（PAR），我们得出结论：（ σ ， J1|J2 ） → （ σ [x @ Seller <$→100] ， 0|J2 ）（ 16）对于对称情况，假设σ @ Buyer（wAddress）= adr（其中adr是代表地址的字符串）然后通过（C OMM）我们有（σ，J2）→（σ [y @ Seller<$→adr]，0），因此通过（P AR）我们得到：（ σ ， J2|J1 ） → （ σ [y @ Seller <$→ adr] ， 0 |J1 ）（ 17）注意到J1|J2-J2|J1，我们现在可以应用（（S TRUCT））来获得：（σ，J1|J2）→（σ [y @ Seller <$→adr]，J1）（18）注意，我们还简化了结果项。总而言之，我们有两个降阶序列，最高降阶到0：（σ，J0）→（σ，（ν Op，Data）（J1|J2））→（σ [x @ Seller<$→ 100]，（νData）J2）→（σJ，0）和（σ，J0）→（σ，（νOp，Data）（J1|J2））→（σ [y @ Seller<$→adr]，（νOp）J1）→（σJ，0）其中，r∈etσJd=efσ[x@Seller<$$> →100][y@Seller<$→adr]。例7（归约：递归）最后我们给出一个递归归约的例子，以recX为例. （x@B：= 1.X）之前。注意到：（x@B：= 1.X）[recX.x@B：= 1.X/X]defx@B：= 1;recX.x@B：= 1.X因此，我们有：（σ，recX.x@B：= 1.X）→（σ[x@B<$→ 1]，recX.x@B：=1.X）142M. Carbone等人理论计算机科学电子笔记171（2007）127→（σ[x@B<$→ 1]，recX.x@B：= 1.X）→....果然M. Carbone等人理论计算机科学电子笔记171（2007）1271434全局演算4.1会话类型正如在2.1节中提到的，我们使用会话类型[15]作为全局演算的类型结构。在高级Web服务和业务协议中，服务/参与者参与的交互结构可能不限于单向消息或类似RPC的请求-应答。这就是为什么全局演算的类型抽象需要捕获服务的复杂交互结构，从而导致使用会话类型。通过将交互结构明确地作为类型抽象，程序员被鼓励在更抽象的层次上思考以通信为中心的程序，而不是将交互视为不相关通信的集合，专注于它们的高级结构。类型的语法如下。θ：：= bool | int | ...α：= α is↓opi（θi）。αi|i s↑opi（θi）。αi|α1|α2|不|反射α|0高于θ，θJ，. 在本例中，值类型仅包括原子数据类型。 α，αJ，. 是会话类型。注意会话通道s、sJ、. 自由发生在会话类型中（这是必要的，因为在单个会话中有多个会话信道，参见[15]）。我们采取|是交换的和结合的，0的情况。递归类型在标准方式中被视为正则树[18]。每个结构的简要说明如下。•is ↓ opi（θi）。 αi是在s处的分支输入类型，表示从{opi}接收任何具有类型θ i的值的运算符的可能性（这应该是两两不同的）。•is↑opi（θi）。αi，在s处的分支输出类型，是上述的精确对偶。• α1|α2是α1和α2的平行合成，抽象出两个会话的平行合成。我们要求α1中的会话通道和α2中的会话通道是不相交的。• t是一个类型变量，而rec t.α是一个递归类型，其中rect绑定了t在α中的自由出现。递归类型表示具有循环的会话。我们假设每个递归都是受保护的，即，在rec t.α中，类型α应该是输入/输出类型或输入/输出类型的n• 0是不活动类型，表示会话终止。 0经常被忽略。每次在共享服务通道上发生会话时，会话通道都是新生成和交换的。因此，服务的接口应该指示要交换的会话通道的向量，以及如何使用它们。这由抽象会话类型或服务类型来表示，其中，会话信道的具体实例是一个抽象的会话类型，其中，会话信道是一个成对不同的会话信道的向量，它应该覆盖所有的会话信道，并且会话信道不一定是不可见的。 （S）在数据库中存储数据集的副本，这会导致数据集和所有数据集的质量问题。144M. Carbone等人理论计算机科学电子笔记171（2007）127在用例子说明这些类型之前，我们引入一个自然的对偶概念。α的余型或对偶，记作α，如下所示。isi↑ opi（θi）。αi= α isi↓ opi（θi）。αi<$i si↓ opi（θi）。αi= α isi↑opi（θi）。αi雷克湾 α = rec t。 αt = t0= 0例如，s↓QuoteReq（string）的co-type。0是s↑QuoteReq（string）。0，交换输入和输出。给定一个术语I，我们以下面的方式使用服务/会话类型键入IIDΔ其中，r是从服务信道到服务类型的映射，并且Δ是从会话信道到会话类型的映射。我们称之为Γ IDΔ，一个类型的π。一个类型rID Δ表示I中的服务/会话通道的使用分别符合这样的一个XML是使用类型化规则导出的，这些规则为术语I构造服务/会话类型化，遵循后者的语法结构。我们将类型规则的介绍留给[9]，在其中我们还证明了它们满足标准属性，如主语归约和主体类型。在这里，在下一小节中，我们将通过具体的例子来说明类型4.2会话类型示例8（会话类型：基础）考虑以下交互（参见示例1），假设adr和prd是字符串类型的变量，位于买方和卖方。买方→卖方：s1QuoteReq，prd，prd.卖方→买方：s2QuoteRep，100，y. 买方→卖方：s1购买，adr，adr. 0（十九）卖方提供的接口（就这种交互而言）可以通过以下会话类型来描述：s1↓ QuoteReq（string）. publicintfindDuplicate（int p）. s1↓购买（string）. 0（2M. Carbone等人理论计算机科学电子笔记171（2007）1271450）相同的交互可以从买方的角度进行类型抽象：s1↑ QuoteReq（string）. publicintfindDuplicate（int p）. s1↑ Purchase（string）. 0（21）146M. Carbone等人理论计算机科学电子笔记171（2007）127它只不过是（20）的同类型现在让我们在（20）中添加一个会话初始化买方→卖方：ch（s1s2）.买方→卖方：s1QuoteReq，prd，prd.卖方→买方：s2QuoteRep，100，y. 买方→卖方：s1QuoteAcc，adr，adr. 0（二十二）那么Seller在通道sh的服务类型如下：（s1s2）s1↓ QuoteReq（string）. publicintfindDuplicate（int p）. s1↓购买（string）. 0（23）其表示：首先，交换两个新的会话信道S1、S2（按此顺序）;然后，使用这两个信道，进行所表示的形状的通信因此，服务类型（23）描述了从ch开始的整个行为，尽管是抽象的。例9（会话类型：分支）让我们用分支来完善（19）买方→卖方：s1QuoteReq，prd，prd.卖方→买方：s2QuoteRep，100，y.⎛ ⎞买方→卖方：s1购买，adr，adr. 0⎟（二十四）⎜ ⎟ +⎝ ⎠买方→卖方：s1Nothanks。0从卖方的角度来看，这可以抽象为：s1↓ QuoteReq（string）.publicintfindDuplicate（int p）.（s1↓购买（string）. 0+ s1↓ Nothanks（）.0个）（二十五）注意，（25）中的和+意味着输入方（这里是卖方）等待两个选项，购买和不谢：另一方面，（25）的共同类型（从买方s1↑ QuoteReq（string）.publicintfindDuplicate（int p）.（s1↑ Purchase（string）. 0+ s1↑Nothanks（）. 0个）（二十六）