Maude中的Erlang程序模型检测及形式验证

理论计算机科学电子笔记176（2007）147-163www.elsevier.com/locate/entcsMaude中核心Erlang程序的抽象与模型检测MartinNeuhüaußer1Thoma sNoll2软件建模与验证组亚琛工业大学D传真：+49 241 80 22217摘要本文提供了一个贡献的并发函数编程语言ERLANG，这是专为电信应用程序编写的程序的形式验证。我们在重写逻辑框架中提出了这种语言的形式化，采用方程来定义系统状态空间上的抽象映射。此外，我们给出了一个草图的实现在MAUDE系统，并演示了使用其模型检查器来验证简单的系统属性。保留字：形式验证，函数式编程，ERLANG，MAUDE，重写逻辑1引言在本文中，我们将在函数式编程语言ERLANG[1]的背景下讨论软件验证问题，Ericsson公司开发该语言是为了解决在并发和分布式环境中开发大型程序的复杂性。我们对这种语言的兴趣是双重的。 一方面，它经常被成功地用于电信系统的设计和实现。另一方面，它相对紧凑的语法和干净的语义支持形式化推理方法的应用在这里，我们尝试采用虽然模拟和测试探索了系统的一些可能执行，但模型检查对其所有行为进行了详尽的探索。在本文中，我们集中在验证过程的第一部分，即要检查的（过渡系统）模型的构造1 电子邮件地址：neuhaeusser@cs.rwth-aachen.de2 电子邮件地址：noll@cs.rwth-aachen.de1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.06.013148M. 诺伊豪瑟河Noll/Electronic Notes in Theoretical Computer Science 176（2007）147更具体地说，我们的方法是基于C核心 ERLANG[3，4]，一个中间语言正在使用的ERLANG编译器，然而，是非常接近原来的语言。我们使用重写逻辑框架正式描述其语义，该框架在[9]中提出，作为并发的统一语义框架它已被证明是许多具体规范和编程语言的适当建模形式主义[8]。在这种方法中，一个系统的状态因此，重写逻辑支持编程形式主义的定义，并通过使用（等式）项重写方法来执行或模拟具体系统。我们将看到，这些方程可以用来定义抽象映射，这些抽象映射减少了系统的状态空间。此外，我们将表明，通过采用重写逻辑框架的可执行实现，MAUDE[6]，可以自动导出给定ERLANG程序的转换系统，并使用MAUDE模型检查器验证其属性。本文的其余部分组织如下。第2节介绍了C核 ERLANG编程语言的语法结构和它们的直观意义。第三节简要介绍了重写逻辑框架。最后，第四、五节是本文的主体部分，研究了CORE ERLANG操作语义的重写逻辑规范及其在MAUDE中的2核心ErlangERLANG/OTP是一个编程平台，它为编程开放分布式（电信）系统提供了必要的功能：支持通信和并发的功能语言ERLANG，以及提供即用组件（库）和服务的OTP今天，许多由爱立信公司生产的商用产品至少有一部分是用ERLANG实现的。这种产品的软件通常被组织成许多相对较小的源模块，这些源模块在运行时作为并行操作并通过异步消息传递进行通信的动态变化数量的进程来执行。这种软件的高度并发性和动态下面我们考虑在[3]中介绍的ERLANG编程语言的核心版本，它在ERLANG编译器中用作中间语言。它支持对数据类型（如原子常数（atoms），整数，列表，元组和进程标识符（pid））进行操作的进程的动态网络的实现，通过称为邮箱的无限有序消息队列使用异步，FullER-LANG有几个额外的特性，比如进程的分布（到节点上），M. 诺伊豪瑟河Noll/Electronic Notes in Theoretical Computer Science 176（2007）147149模块：：=模eatom[Fnamei1，. . ，Fnameik]属性s[atom1=Cn st1，. . . ，atomm=Cn stm]FDEF1... FdefnFdef：：=FunName=FunFunName：：=原子/整数常量（c）：：=Lit-[常量1|常数2]-{常数1，. ，Constn}-Fun Val（v）：：=Const-Const1，.<. ，常数n>Lit：：=integer-numeroat-atom-char-string-[]Fun：：=fun（var1，.，varn）->ExpsExps：：=Exp-Exp1，..<. ，Expn>Exp（e）：：=var-Fname-Lit-Fun—[实验1|实验2]-{实验1，. . ，实验n}—设变量=实验2中的实验1-做实验1实验2—letrecFdef1... 实验中的Fdefn—应用Exps0（Exps1，.. ，实验n）—callExpsn+1：Expsn+2（Exps1，. . . ，Expsn）—primopatom（实验1，.. ，实验n）—tryExps1catch（var1，var2）->Exps2—病例失效日期条款1.. 第n条结束—收到第1条... 在Exps1->Exps2Vars之后的子句n：：=var-var1，.<. ，varn>条款（cl）：：=当实验1->实验2时的PatsPats：：=Pat-Pat1，.<，专利号n>Pat（p）：：=var-Lit-[Pat1|Pat2]-{Pat1，.. . ，Patn}-var=PatFig. 1. 铁矿石开采moduleletLockerPid=calllcall’{' re q '，Clien t } whe n ' tru e ' - > do call l ' erlan g'：'！’{after’letMe=calll呼叫l' erlan g '：'！’'o k ' whe n ' tru e ' - > call l ' erlan g '：'！' （Locker，{apply结束图2。COREERLANG中的资源锁并且支持健壮的编程和与非E语言代码的互操作C或Java。CORE ERLANG的语法由图1中的上下文无关语法3定义有关详细说明，请参阅[3，4]。作为一个介绍性的例子，我们考虑一个短程序，它实现了一个简单的资源锁，即，仲裁器，其在接收到来自客户端进程（在这种情况下为两个）的对应其代码如图2所示。任何一个C语言程序都是由一组模块组成的。 每个模块3为了简化符号，让占位符c、v、e等表示由相应的非终结符生成的语言元素。此外，设a和x分别表示原子和变量150M. 诺伊豪瑟河Noll/Electronic Notes in Theoretical Computer Science 176（2007）147由名称标识，后跟导出函数列表和函数定义列表。在我们的例子中，系统被定义在一个名为locker的模块中。它使用start函数初始化。通过调用spawn内置函数，后者生成两个额外的进程，这两个进程都运行来自locker模块的客户端函数。在这里，self内置函数返回locker进程的进程标识符（pid），然后将其作为参数传递给客户端，这些都能与储物柜locker进程在非终止循环中运行locker函数。它使用receive构造来检查请求是否已经到达。后者应该是由req标记和客户端进程标识符（由变量Client匹配）组成的一对。after子句可用于指定在特定时间限制内没有匹配请求到达时进程的行为;这里通过将无穷原子作为超时值来停用它然后，通过发送一个ok消息，客户端被授予访问资源的权限。最后，在接收到来自相应客户端的rel（释放）消息之后，锁定器返回到其初始状态。客户端进程展示了互补行为。通过发出请求，它要求访问资源。在这里，self内置函数再次用于确定客户端进程的pid，然后由locker进程将其用作客户端的句柄。在接收到ok消息后，它访问资源，然后释放它。这种系统的理想正确性属性是简单的：无死锁：不存在等待彼此继续的循环进程链，即，储物柜应该总是能够接收新的请求或释放，互斥：没有两个客户端可以同时访问资源，无饥饿：所有能够进入临界区的客户端最终都应被授予其所要求的访问权。稍后我们将举例说明如何通过构造上述程序的转换系统来检查第二个3重写逻辑框架重写逻辑框架由J. Meseguer在[9]中提出。在[8]中可以找到对这种方法的介绍以及广泛的参考书目。重写逻辑旨在作为一个统一的数学模型，并使用重写系统中的概念而不是等式理论。它分别描述了并发系统的静态和动态方面更确切地说，它区分了描述系统状态结构的定律和规定系统可能的跃迁的规则。这两个方面分别形式化为一组方程和作为（条件）项重写系统。这两种结构的运作M. 诺伊豪瑟河Noll/Electronic Notes in Theoretical Computer Science 176（2007）147151在状态上，表示为（的等价类）项更具体地说，在Meseguer的方法中• 签名是签名，即，功能符号的分级字母表• ET（X）×T（X）是一个有限的方程组，在T（X）的一个集合T（X• R是一组有限的（条件）转换规则，其形式为c1−→d1.. . ck−→ dkl−→r关于重写逻辑的语义，Meseguer定义重写理论T需要一个E− [s]E−→[t]E，并写T[s]E−→[t]E如果这个概率可以通过有限次地应用特定的演绎规则来获得，这些规则指定了如何应用上述过渡规则。用这种方法，就有可能推理出状态由项表示并通过变迁演化的并发系统。在这里，状态是根据签名和等式来构造的，等式用于识别仅在其语法表示中不同的术语。稍后我们将看到，它们也可以用来定义状态空间上的抽象映射。然而，（条件）项重写模方程理论通常过于复杂，甚至是不可判定的，这是一个事实。因此，在E中不可能存在任意的方程。根据P.在[11]中，我们提出为了将E分解成一组有向方程（即，项重写系统），ER，并到一个集A表示的结合性和交换性的某些二元运算符在ER。给定ER是模A终止的，通过R模E的重写可以通过通过ER的归一化和通过R的重写的组合来实现，两者都是模A。这里，由R引起的步骤表示系统的实际状态转换，而由ER定义的约简必须被视为内部的、4Core Erlang给定一个CORE ERLANG程序和一个初始表达式，我们首先只考虑局部求值步骤来定义它的转换系统语义。在第4.2节中，我们扩展了我们的转换，以捕获并发语义，即，评价的语义是用边项表示的。有关小步操作语义的[4]在MAUDE中，重写逻辑规范由一个具有多种签名的隶属方程逻辑理论参数化，参见。[2]的文件。152M. 诺伊豪瑟河Noll/Electronic Notes in Theoretical Computer Science 176（2007）147−→ee2−→e2αdove eer[·]：：=-·-[r[·]|e]--一种[v|r[·]]{v1， . . . ，vk−1，r[·]，ek+1， ..... . . 你 好 。 ，en}（1≤k≤n）--let =r[·]ine（1≤k（n∈≤n））--c l 1的caser[·]， . .... . . 你 好 。 ，clnend收到c11， . . . ，clnafterr[·]->e（n∈（n∈））--dor[·]eapplyr[·]（e1， . . . ，en）（n∈）-应用f（c1， . . . ，ck−1，r[·]，ek+1，. . ，en）（1≤k≤n）-callr[·]：en+1（e1， . . . ，en）（n∈）-calla1：r[·]（e1， . .... . . 你 好 。 ，en）（n∈）-调用la1：a2（c1，. . . ，ck−1，r[·]，ek+1，. . ，en）（1≤k≤n）-primopa（c1， . . . ，ck−1，r[·]，ek+1， . . . ，en）（1≤k≤n）图三. C核 E语言表达式的约简上下文4.1顺序语义学令Exp表示根据图1的有效CORE ERLANG表达式的集合，并且fv（e）表示在项e中具有至少一个自由出现的变量序列。然后，我们形式化封闭C核 ERLANG表达式的语义，即，没有自由变量的表达式，通过相关的转换系统Te：第四章. 1Lete0∈Expandfv（e0）=ε. 该分类变换系统 为Te=（E，e0，Acte，→e），其 中 E ： ={e∈Exp| fv （ e ） = ε}{ε} 表 示 具 有 特 殊 初 始 表 达 式 e 0 的 状 态 集 ，→eεE×Acte×E表示跃迁关系。转换是根据以下推理规则定义的，并由来自集合Acte的动作标记，其中τ∈Acte表示不可观察的动作，其他标签表示可观察的评估步骤。表示在表达式计算过程中发生错误而产生的未定义值。CORE ERLANG的标准实现采用最左-最内求值策略。 为了使论证评估形式化，我们使用了重-在[7]中首次引入的约简上下文：直观地，约简上下文是具有占位符的核心概念，其中，如果占位符是子项，则确定下一个评估步骤发生的用一个可简化的表达式来代替形式上，约简上下文集由图3中的上下文无关语法定义令Ctx表示约简上下文的集合。下面的推理规则将最左最内的求值策略形式化：定义4.2设e，eJ∈Exp，α∈Acte和r∈Ctx使得不存在e∈Exp\Val和r∈Ctx\{·}，满足ate=r∈[e]。下面的规则适用：e−α→eeJr·（上下文）r[e]αr[eJ]根据定义4.2中的条件，（上下文）规则仅适用于wrt。最大缩减上下文，即，e可以直接计算，而不需要进一步下降到其子项。使用这个概念，排序运算符的语义由以下推理规则捕获：−→eeJ（上下文）（Seq）做r[e]eαdor[eJ]eτ2−→e2M. 诺伊豪瑟河Noll/Electronic Notes in Theoretical Computer Science 176（2007）147153e根据定义4.2，第一个规则5的迭代应用计算第一个子表达式。一旦它被完全求值，第二个规则就变得适用，它形式化了排序语义，结果被丢弃，求值继续使用第二子表达式。4.1.1模式匹配语义为了形式化CORE ERLANG模式匹配的语义，使用替换来在语法上用它们各自的值替换自由出现的变量（取自集合Var）。定义4.3置换是一个部分映射σ：VarFunName→Const。[x1] →c1，.，xn<$→cn]表示有限替换，其中对于1 ≤ i ≤ n，xi被常数ci替换。将置换推广到任意核的代数上.第6类：• xσ：=ciifσ（x）=cixifσ（x）=• {e1，.，en}σ：={e1σ，.，enσ}• [e1|e2]σ：=[e1σ|e2σ]• （令=eine2）σ：= 1e.t=eσine2σJ其中σJ：VarFunName→Const：x›→σ（x）如果x/∈ {x1，.，xn}否则，模式匹配语义使用以下句法子项形式化：子句pwheng->e匹配值v，如果（i）存在替换σ使得pσ=vholds和（ii）gardexpress iongσ evalueto“tru e”. 对于小的，这通过以下定义来捕获定义4.4设p∈Pat，e，g∈Exp，v∈Val。然后匹配：Val×Clause→Exp{\fnSimHei\bord1\shad1\pos（200，288）}（v，pwheng->e）›→.eσifσ。（v=pσgσ−→否则，CORE ERLANGcase运算符根据给定值进行控制分支i。 （ma tch（v，cli）=eJjetrecv（q，c）−−→ee（接收1）如果在时间界限ct内没有接收到匹配消息，则评估et根据我们的<$qma tch（q，cl1， . . . ，clk）ct∈（接收器2）timeout（q）收到cl1· · ·clkafterct->et−→eet4.1.3Higher–Order函数抽象被视为值，并使用apply运算符应用于一系列为了捕捉它的语义，我们将参数变量的每个自由出现替换为相应的值：σ：=[x1<$→c1， . . . ，xn <$→cn]应用 fun（x1， . .... . . 你 好 。 ，xn）->e（c1， . . . ，cn）−τ→eeσ（应用程序1）请注意，参数求值由图3中定义的约简上下文隐式指定。letrec运算符支持它的语义由以下规则形式化m.eJ：= letrec. . . aj/nj=fun（xj）->ej。 . . 伊内埃伊ih i（LRec）莱特雷角 . . aj/nj=fun（xj）->ej。 . . ine−τ→ee。 . . ，aj/nj> →fun（xj）->eJ， . . .函数名ai/ni被视为在函数抽象的特殊域范围内的变量。一个letrec表达式的求值产生一个新的绑定，其作用域超过了e和e1，.，em.这种扩展的作用域通过将letrec语句传播到函数抽象的主体中而反映在语义中（参见在前提中定义eJ）4.2并发语义为了推理用CORE ERLANG实现的并发系统，我们现在将顺序表达式的语义提升到系统级别，在系统级别上，也有副作用，即，进程生成和通信。定义4.5过程集由P：= Exp给出联系我们×常数×2×。一个进程用（e，i，q，L，t）∈P表示，其中e是要计算的表达式，i是进程标识符，q是进程的7匹配失败会导致非τc1的情况c.. . ckend−→ eeJct∈{JM. 诺伊豪瑟河Noll/Electronic Notes in Theoretical Computer Science 176（2007）147155为了描述整个系统的可能行为，我们将这个定义扩展到过程集：定义4.6有限子集S∈2P称为过程系统。S是良好的形式若对任意p，p1，p2∈S，p1p2Pid（p1）/=Pid（p2）和 Links（p）pJ∈S，p=/Pid（pJ）PJ这里，Pid：P→和Links：P→2分别表示进程标识符和链路组件上的投影;此外，映射Pid为以自然的方式扩展到一组过程。通过将良好形成的过程系统视为建模的反应系统的状态，我们获得了以下定义4.7设p0∈P是一个初始过程。相应的转移系统定义为Ts=（S，S0，Acts，−→s），其中S：=2P是状态S的集合，其中S0：={p0}，并且其中−→sS×Acts×S表示由来自集合Acts的动作标记的转移关系。同样，τ∈Acts表示局部（不可观察）评估步骤，其他标签反映侧效应。将局部评估步骤形式化的推理规则直接从序列级提升到系统层语义：e−τ→eeJ（Sequ）S<${（e，i，q，L，t）}τS<${（eJ，i，q，L，t）}−→s这里，结论中的并运算符以集合论的方式反映交织语义。在大多数情况下，在4.1节中介绍的不确定性可以在考虑过程系统时解决，其中有关系统状态的信息是可用的。4.2.1创建新流程新进程是通过计算spawn内置函数创建的。在顺序层中，新创建的进程的pidj不能被推断出来;因此，它被非确定性地选择，并被转换标签所反映，侧面效果：（Spwn）spawn（a1，a2，c）~jcall实际的流程创建由系统层规则捕获，其中引入了新的流程术语并固定了pid：spawn（a1，a2，[c1，.，ck]）~je−→eej/∈Pid（S）<${i}（Spawn1）S<${（e，i，q，L，t）}spawn（j）−→sS<${（e，i，q，L，t），（calla1：a2（c1， . .... . . 你 好 。 ，ck），j，ε，ε，false）}[8]一个例外是新过程的创建，其中新标识符是非确定性地选择的J156M. 诺伊豪瑟河Noll/Electronic Notes in Theoretical Computer Science 176（2007）1471SSS4.2.2消息传递发送消息会影响发送者和接收者的状态;这在系统层上由推理规则（发送1）捕获：你好！CJei−−→e ei（Send）send（i，j，c）S{（ei，i，qi，Li，ti），（ej，j，qj，Lj，tj）}J−−→sS<${（ei，i，qi，Li，ti），（ej，j，qj·c，Lj，tj）}引入非确定性来形式化局部求值，接收项在系统层上完全解析：recv（q1，c）e−→ee（接收）S<${（e，i，q·c·q，L，t）recv（i，c）S<${（eJ，i，q·q，L，t）}1 2}−−→s1 2这里，在推理规则（Rcv1）的前提中应用qmatch谓词确保了从邮箱中选择第一个匹配的消息c4.3State–Space转换系统Ts通过考虑局部求值步骤以及带有边值的求值步骤来捕获并发C核 E语言为了推理整个系统的行为，我们主要对进程间通信以及进程的创建和终止感兴趣因此，我们忽略局部τ第四章. 图8等式i=i=i。通过迁移到商转移系统T/T，我们从局部τ.Σ第四章. 9L etT：=S/N，[S0]N，ActN，−→Ndentt itit|S∈S}不表示动作的集合，[S0]是初始状态，Actτ：=Acts\ {τ}是动作的集合，其中转移关系−→S/×Act×S/isdefineedbyy[S]−α→∼ [T]：T_j ∈S， T_J∈S.S←−τ→<$S J−α→TJ←−τ→τT。关于可能的状态空间减少，以下引理成立：引理4.10令S={p1，. ，pn} ∈ S是一个过程系统，pj=（ej，ij，qj，Lj，tj），其中1 ≤ j ≤ n. 进一步地，设kj表示过程pje对于a−→τe-normalf∈reahinga−→τe-normalf∈re的连续τ-步数。 P_（st）（S，τ）：={SJ∈S|S−τ→SJ}是由y生成的：|Post（S，τ）（千美元）+1）。S| ≤1≤j≤kj根据引理4.10，过程系统S的1≤j≤k（kj+1）个后继状态由T∈内的一个等价类表示。 最重要的是，在T中，我们不再考虑τJSM. 诺伊豪瑟河Noll/Electronic Notes in Theoretical Computer Science 176（2007）147157排序过程。操作<_|_|_|_|_|_|_|_>：标签SysResult Expr PidPidSequence BoolModEnv-> Process[ctor]。排序过程。subsort进程<进程。op#empty-processes：-> Processes[ctor].op_||_:ProcessesProcesses->Processes[ctorassoccommid：#empty-processes]。对ProcessEnvironment进行排序。op（（_，_））：SysLabel进程ModEnvPidSequence -> ProcessEnvironment [ctor]。见图4。 签名定义5在Maude在第4节中介绍的小步操作语义将给定的具有初始进程p0的CORE ERLANG程序与商转移系统Tn联系起来，从而形式化了可能的系统行为。为了自动推理关于这类系统的性质，在本节中，我们使用我们语义的重写逻辑规范来操作T的计算。根据重写逻辑框架，在图4中，我们首先定义了流程和流程系统的符号性质：为了实现我们的语义，我们扩展了流程P=Exp{x}××Constantx2×的表示（参见定义4.5）。由三个额外的组成部分：(i) 一个进程标签，概括了进程(ii) SysResult项，指示最后一次侧检的结果，以及(iii) 已知函数声明的集合ModEnv相应地，过程系统是过程项的多集合，其由抽象和复杂性概念表示。||“.5.1CORE ERLANG签名除了这些基本的操作符声明，一个稍微受限制的9C核 ERLANG语法（参见。第2）节被指定为多种签名，以便它可以被Maude解释器解析。允许任意多个参数（例如，当考虑应用表达式时），我们定义一个参数列表操作符：Subsort Expr NeExprList[ctorasynchronous].因此，无界参数列表在内部被NeExprList排序的单个参数替换。然而，请注意，由于省略了连接运算符在MAUDE系统中，术语使用多种签名构建这里排序表示语义概念，而种类指的是在传统的多排序签名的上下文中的排序的概念在句法层面上，每个格式良好的术语被分配一个种类，而它对指定种类的归属必须使用底层隶属度方程理论的隶属度公理来推断（cf. [2]详情。9需要额外的空格158M. 诺伊豪瑟河Noll/Electronic Notes in Theoretical Computer Science 176（2007）1475.2过程层的规范原则上，将商变迁系统语义映射精确度是从以下公式开始的：等式关系式：=←→τ∗s已转换转化为一个模拟局部τ评估步骤的方程理论在操作上，这些方程被分成一组方程A和一组有向方程ER，方程A是根据算子的结合性和交换性属性推断的，有向方程ER构成一个终止项和连续项重写系统。偏离C核 ERLANG语义，在我们的实现中，我们指定了顺序语义已经wrt。项表示单个过程而不是考虑封闭C核 ERLANG表达式仅10.在底层的顺序语义中，我们使用非确定性来模型侧评估一个简化的评估步骤。然而，该实现要求有向方程的集合ER收敛模A。因此，我们用一个标签和一个组件来避免不确定的选择。作为第一个例子，考虑排序运算符do的语义：var ESL：StopLabel.塞克<陶|RES|执行EX1 EX2 |PID|MBOX|链接|陷阱|我>=<#filterExit（ESL）|RES1|做EX1' EX2 |PID |MBOX|链接|陷阱|ME> ifnot（EX1：：Const）/\：= |ME >:=< tau|RES |EX1 |PID|MBOX|链接|陷阱|ME>.这个有向方程适用的必要条件是第一个子表达式EX1还不是一个值。只有这样，在第二条件内进行进一步的求值，产生新的表达式EX1标签变量ESL的排序在这里是至关重要的：如果EX1的求值产生了一个副效应，则进程的标签将更改为排序StopLabel的等式重写因此，侧面效应的结果是不可猜测的non–deterministically within the “local” process layer, but is resolved later by therewrite5.2.1取代模式匹配语义基于C核 ER-LANG表达式的语法替换;单个绑定表示为排序绑定项。然后，环境被构造为排序绑定环境op_-->_：Var Const -> Binding[ctor].子排序绑定<环境op#empty-env：-> Env[ctor].op_，_：Env Env -> Env [ctorasynchronid：#empty-env].给定一个CORE ERLANG表达式，#subst函数通过递归下降到子项来指定根据给定环境的自由变量的替换。因此，基本情况包括[10]因此，莫德的评价策略不能具体说明论证评价M. 诺伊豪瑟河Noll/Electronic Notes in Theoretical Computer Science 176（2007）147159eq#subst（V，（V-->C），ENV）=C.eq#subst（E，ENV）=E[owise].这里，第一条规则指定了根据环境绑定的变量的替换请注意，由于涉及AC匹配，因此我们可以不失一般性地假设相应的绑定项是环境中的第一个绑定。当考虑引入新的变量绑定，环境必须相应地缩小ceq#subst（letVS=EX1inEX2，ENV）=letVS=#subst（EX1，ENV）in#subst（EX2，ENV1）ifVSET：=#projectVarSet（VS）/\ENV1：=#restrictEnv（VSET，ENV）.通过计算let表达式引入的新绑定的作用域仅在EX2表达式范围内。因此，该替换被应用于EX1子项，而没有任何修改。根据let的语义，在EX2中，序列VS的变量的自由出现是绑定的，并且不能被替换。在ENV1中，这样的基于变量序列VS，函数#projectVarSet和#restrictEnv计算新绑定的变量集并相应地缩小5.2.2模式匹配模式匹配由部分函数#match形式化。匹配失败是通过引入一个常数#nomatch与一个新的排序环境？它被声明为变量环境的超级分类。在模式匹配过程中，我们递归地下降到给定模式的子项，并试图构建一个统一的变量环境。在冲突失败11的情况下，#nomatch常数被包括在指示匹配失败的环境中。因此，我们有：子排序环境<环境？ .op #match：Pat Const ~> Env.eq#match（VAR，CONST）=（VAR-->CONST）。eq #match（CONST，CONST）= #empty-env.eq#match（[PAT1|PAT2]、[C1|C2]）=#match（PAT1，C1），#match（PAT2，C2）. 等式#match（PAT，CONST）=#nomatch [owise]。根据CORE ERLANG的语义，模式中的所有变量都是自由的以同样的方式，两个相同的值彼此匹配，而不需要新的绑定。在更复杂的模式（如列表）中，#match函数递归地下降到相应的子项。最后，第四个等式涵盖了匹配失败，并且#subst和#match函数允许指定CORE ER-LANGCORE ERLANGcase表达式具有cl1···clkend的casev形式，其中求值继续表达式ei11由于C核 ERLANG160M. 诺伊豪瑟河Noll/Electronic Notes in Theoretical Computer Science 176（2007）147当序列cl 1，.中的gi-> ei时，第一个匹配子句cli= pi。，clk.这由以下有向方程指定：侧旗<头乌|#no-res|当保护D->EX条款Send时，|PID|MBOX|联系我们|TRAP|ME>=ifENV：=#match（PAT，C）// \< 抗 辩 （ exit ， tom （ “normal“ ） ） |#no-res|Ex1|PID|#empty-mbox| 联 系 我 们|TRAP|ME>：=<达乌|#no-res|#subst（GUARD，ENV）|PID|#empty-mbox|林克斯|TRAP|ME>/\EX2：=ifEX1==tom（“true“）then#subst（EX，ENV）否则，条款C的情况结束于fi。根据第一个条件，只有当模式PAT与值C匹配时，该等式才适用。第二个条件形式化了警卫评估。根据其结果，评估继续使用子句的右手表达式，或者-如果保护没有评估为“true”-修改的case项被重新评估，此外，模式匹配本身可能失败：侧旗<头乌|#no-res|当保护D->EX条款Send时，|PID|MBOX|联系我们|TRAP|ME>=ifnot（#match（PAT，C）：：Env）.如果序列中的第一个子句不匹配常数C，则#match函数计算的环境包含#nomatch常数;因此#match（PAT，C）的排序为Env？成员资格公式没有被填满。 在这种情况下，将移除失败的子句，并继续与子句序列5.3系统层语义到目前为止介绍的有向方程描述了不可观察的局部评估步骤。我们现在考虑的可观察到的转换模型之间的相互作用，ERLANG过程和形式化的重写规则。从操作的观点来看，这些规则作用于正规形式wrt。等式重写涵盖流程创建的规则提供了第一个示例。 当符号化地计算表达式调用'erlang'：'spawn'（a 1，a 2，c）时，进程'标签被更改为指示侧效应。这就产生了一个标准形式wrt。等式重写;然后crl（SL，||PRCS,ME’,PIDS)=>（sys-newproc（PID，pid（INT），A1，A2，LIST），||<达乌|#no-res|Ex1|pid（INT）|#empty-mbox|#empty-pid-seq|法尔斯河|我'>||PRCS，ME'，pi d（IN T），PID S）ifINT：=#getNewPid（PIDS）/\EX1：=ifLIST==[]ncallA1：A2（）否则调用A1：A2（#getListElements（LIST））fi。当计算表达式时，调用'erlang'：'！' (Pid，Msg），则消息被附加到由Pid标识的进程的邮箱。这个信息从方程理论中传递到相应的重写规则俄克陶乌#no-re s call l ato m（"erlan g"）：ato m（"!<||“）（int（INT），C）|PID|MBOX|联系我们|TRAP|ME>=.M. 诺伊豪瑟河Noll/Electronic Notes in Theoretical Computer Science 176（2007）147161ER/A∗系统级的转换规则通过从进程的标签中提取接收方的PID和消息并将消息附加到接收方的邮箱来对此范式进行操作crl（SL，||||PRCS,ME’,PIDS)=>（sys-sendmsg（PID，pid（INT），C），

下载后可阅读完整内容，剩余1页未读，立即下载