Erlang程序的模型检查及抽象控制流分析

195理论计算机科学电子笔记64（2002）网址：http://www.elsevier.nl/locate/entcs/volume64.html25页Erlang程序的模型检查{抽象递归函数调用Frank Huch1德国基尔大学计算机科学研究所Christian-Albrechts D-24098 Kiel摘要我们提出了一种使用抽象解释和模型检查来验证Erlang程序的方法。在以前的工作中，我们为Erlang定义了一个数据抽象框架该框架的抽象操作语义保留了标准操作语义的所有路径.因此，抽象对于必须在系统的所有路径上保持的所有属性都是安全的，比如LTL中的属性。如果抽象操作语义是一个nite变迁系统，证明可以通过模型检查自动化。但是由于非尾递归函数调用，不能保证无中断性。即使对于nite域抽象解释，我们也得到了nite状态系统和模型检查是不可判定的。在本文中，我们正式抽象的控制流。它通过跳转到同一函数的最后一次调用来替换非尾部位置的递归调用。相应的返回被替换为跳转到可能的返回点。我们已经实现了这种方法作为一个原型，并能够证明适当的关系，如互斥或没有死锁和生命锁的一些Erlang程序。1引言对于并发和分布式系统的形式化验证，我们提出了一种扩展的模型检查程序编写的真正的编程语言。在[16，17]中描述了解决这个问题的直接方法。然而，模型检查问题一般是不可判定的系统实现使用的编程语言和表达时态或模态逻辑中描述的属性。模型检查的直接应用简单的计算已经使自动验证变得不可判定，因为这些计算的终止可能与属性的验证相关。因此，我们需要抽象[6，14，19]。1 电子邮件地址：fhu@informatik.uni-kiel.dec 2002年由Elsevier Science B出版。诉在CC BY-NC-ND许可下开放访问。F. 胡赫196在工业上，编程语言Erlang [1]用于实现分布式系统。我们在[11]中为Erlang的核心片段开发了一个抽象解释框架，其属性是由抽象操作语义（AOS）定义的转换系统包括标准操作语义（SOS）的所有路径。因为AOS有时可能比SOS有更多的路径，所以只能证明必须在所有路径上填充的属性，就像线性时间逻辑（LTL）一样。如果一个抽象函数完整地使用了一个用LTL表示的属性，那么程序也会完整地使用它，但反之则不然。如果AOS是一个nite transition系统，那么模型检验是可判定的[15，21]。使用逻辑LTL只是一种可能性。也可以使用在底层Kripke结构的所有路径上定义的其他逻辑。例子是计算树逻辑[5]的片段，其中属性只能为所有路径定义：ACTL和ACTL。在我们的原型中，我们使用表达逻辑LTL，并使用它作为任意逻辑的代表与所有量化。定义的抽象只为Erlang程序的一个子类产生一个nite转换系统，称为分层程序[11]。递归只允许在尾部位置。然而，在实践中，许多Erlang程序并不满足这个限制。 例如，append或length的标准定义已经不是分层的。因此，使用这种函数的程序不能用现有的抽象解释技术抽象成有限状态转换系统。原因是非尾递归函数调用。在[13]中，我们skeched非尾递归函数调用的抽象，我们在本文中形式化非尾递归调用被跳转到程序中的相关位置所取代返回被替换为跳转到函数调用的所有可能的继续。我们得到了一个nite态过渡系统。系统的性质可以通过LTL模型检验自动证明。在第2节中，我们定义了Erlang的核心部分的语法，并在第3节中概述了这种图表示的操作语义。抽象解释的框架将在第4其限制在第5节中介绍。在第6节中，我们提出了一个图的语义，提出的抽象的基础上。我们在第7节中形式化了我们的抽象。第8节介绍了它在模型检查中的使用，最后，我们在第9节中总结并讨论未来的工作2Core Erlang让是一个带有arity的预定义函数符号的签名。例如+/22.设Var=fX;Y;Z; ：：g是一组变量，A是一组原子，例如： f1;2;fail;fac; ：g. 设C为Erlang构造函数的签名函数：C=f[：|：]=2;[]=0g [f{：}=nj n2IN g [fa=0j a2一个构造器，用于构建列表的构造器，用于空列表的构造器，用于构建任意元数的元组的构造器，以及作为元数为0的构造器的原子。F. 胡赫197构造函数项的集合被定义为最小集合TC（S），使得：STC（S）andc=n2C，t1; ：;tn2TC（S）=）c（t1; ：;tn）2TC（S）：Core Erlang程序的语法定义如下：p：：=f（X1，：，Xn）->e. jppe：：=（e1，：，en）j Xj pat=ej selfj e1，e2j e1！e2j情况e的m端j接收m端 j生成n（f，e）M：：= p1-> e1;：; p n-> e npat：：=c（p1，：，pn）jX一个程序的所有定义函数，用它们的arity扩展，建立了集合FS（p）。=n是f=n 2 FS（p），F=n 2和c=n 2 C的缩写。在每个CoreErlang程序中，都定义了一个main函数：main=0 2 FS（p）。我们称核心Erlang项的集合为e ET（;）。集合ET（S）是通过为Core Erlang术语添加语法规则e：：= v 2 S来定义的。例2.1设Core Erlang程序p0为： main（）-> DB =spawn（dataBase，[[]]），spawn（client，[DB]），客户端（DB）。dataBase（L）-> receive{allocate，Key，P} -> case lookup（Key，L）offail-> P！自由，接收{value，V，P} -> dataBase（insert（Key，V，L））end;{succ，V} -> P！allocated，dataBase（L）end;{lookup，Key，P} -> P！lookup（Key，L），dataBase（L）end.insert（K，V，L）-> case L of[]->[{K，V}];[{K'，V'}| L ']->情况K'< K，true-> [{K'，V'}| insert（K，V，L'）]; false ->[{K，V}| L]端端该程序创建保持存储数据库信息的状态（L）的数据库进程。数据库由一个元组列表表示，每个元组由一个键和一个对应的值组成。数据库的接口由消息{allocate，Key，P}和{lookup，Key，P}给出。分配F. 胡赫198分两步进行首先，接收并检查密钥如果F. 胡赫199C与数据库中的键不冲突，则可以接收相应的值并将其存储在数据库中。这种在多个步骤中的消息交换必须保证数据库上的互斥，因为否则可能会有两个客户端进程向数据库发送键和值，并且它们以错误的组合存储。客户端可以相应地定义[11]。我们稍后将证明，数据库与两个访问客户端的组合满足此属性。3核心ErlangErlang是一种严格的函数式编程语言。它扩展了并发执行的进程。使用spawn（f;[ a1;：：：; an]）可以在程序中的任何位置创建新进程。该过程从f（a1;：; an）的求值开始。如果spawn的第二个参数不是ground，则在创建新进程之前对其进行评估。spawn的函数结果是新创建进程的进程标识符（pid）用P！任意值（包括PID）可以被发送到其他进程。这些进程通过它们的pid（p）来寻址 进程可以通过Erlang函数self/0访问自己的pid。 发送给进程的消息存储在邮箱中，进程可以通过receive语句中的模式匹配方便地访问它们。特别是，可以忽略一些消息并从更后面获取消息。更多详情请参见[1]。与其他函数式编程语言的主要区别是没有作用域。Erlang使用一次性绑定变量：首先，变量可以在指定函数的调用和派生中绑定。其次，它可以与pat= e、case和receive中的模式匹配绑定。如果在模式匹配中使用绑定变量，则这不是引入新变量，而是针对其实际绑定进行匹配在Erlang程序中，这种技术通常用于在运行时比较值例如，例2.1的内部接收状态中的模式{value，V，P}中的变量P已经绑定到请求客户端的pid对客户端的相同pid的这种隐式测试用于识别来自相同客户端的消息并忽略来自其他客户端的值在[11]中，我们提出了CoreErlang的形式语义。在下文中，我们将其称为标准操作语义（SOS）。 它是一组进程上的交错语义。形式上，一个进程由一个pid（2Pid：=f@nj n2IN g）、一个Core Erlang赋值项（e2ET（TC（Pid）和一个表示邮箱的word over constructor项（2 T（P id））组成。对于最左最内的求值策略的定义，我们使用求值上下文的技术[8]：E：：=[ ]j（v1，：，vi，E，ei+2， ：，en）j E，ej p=Espawn（f，E）j E！e j v！E j case Eofm endv表示求值表达式，E表示redex所在的子项，e表示M是无法评估的部分。[]被称为孔，标志着F. 胡赫2001BBBBBBBbBb下一次评估的重点。然后，我们将上下文E写成E[e]，其中洞被e替换，下一步的评估在这里进行。类似于集合S上的核心Erlang项ET（S），我们将核心Erlang上下文命名为EC（S）。集合S定义值的集合：v 2 TC（S）。 在[11]中定义的操作语义中，我们有（S = TC（P id））。对于本文中提出的抽象，S将是TC（Var）。语义学是一个非并发的转换系统。对过程的评价是交错进行的。只有沟通和过程创造才有副作用。为了对这些动作进行建模，涉及到不止一个过程。为了给人一种语义上的印象，我们给出了向另一个进程v =02 Pid！v2;（;E[v1！v2];q）（0;e;q0）=）;（;E[v2];q）（0;e;q0：v2）该值被添加到进程0的邮箱中，发送操作的功能结果是发送的值。4核心Erlang程序在[11]中，我们开发了一个Core Erlang程序的数据抽象框架。抽象操作语义（AOS）产生一个转换系统，其中包括所有路径的SOS。在抽象解释中，A=（A;;v;）对于Core Erlang程序，A是抽象域，它应该是我们在模型检查中应用抽象解释功能定义了预定义函数符号和构造函数的语义。其codomain是A。因此，例如不可能在Nite域抽象中自由地解释参数。 还定义了模式匹配在等式、case和receive中的抽象行为。在这里，抽象可以产生额外的非确定性，因为分支在抽象中可以变得不可判定。因此，产生了一组结果，这些结果定义了可能的解。此外，一个抽象的解释包含一个偏序v，描述了A的哪些元素比其他元素更精确 我们不需要完全偏序，因为我们不计算任何固定点。我们只是用这个抽象的解释来评估操作语义。一个抽象的例子是：INvfvj v 10gvfvj v5g。它是更精确地知道，一个值是5，比10比任何数字。A的最后一个组成部分是抽象函数：：T C（P id）！ A将每个实值映射到一个抽象表示。这通常是最精确的表示。 最后，抽象解释必须具有将抽象解释与标准解释联系起来的完整属性。它们保证SOS的所有路径都在AOS中表示，例如在分支中。下面是这些属性的示例BF. 胡赫201一(P1)对于所有=n 2[C; v1;：; vn2 TC（P id）和iv（vi）成立b（ev1; ：;n）v（A（v1; ： ：;vn））.它假定，评估一个predefened函数或构造函数的抽象值，这些抽象值是一些具体值的表示，产生了对同一函数在具体值上的评估的抽象其他属性假设了匹配和模式匹配，以及由抽象值表示的pid。更多细节和一些示例抽象可以在[11，12]中找到我们不会-又来了。 在下一节中，我们将定义这个语义的修改版本，它对我们的目标更有用5数据抽象例5.1考虑下面的Core Erlang程序：main（）-> f（42）。f（X）->f（f（X））。最小可能的抽象域是只包含元素的域？它代表了所有可能的值。有了这个抽象域，程序的抽象语义包含路径：（@1;main（）;（））！（@1;f（42）;（））！（@1;f（？）;（））！（@1;f（？））;（））！“ ……”（@1;fn（？）;（））！（@1;fn+1（？）;（））！* *它包含许多不同的状态。这种抽象语义相对于操作语义是正确的，在这个意义上，SOS的所有路径都被表示。但是我们不能使用简单的模型检查算法来证明这个抽象语义的属性，因为它有一个inite状态空间。这个例子在实践中似乎是无关紧要的，但是在nite转换系统中，对于nite域上的抽象语义，也会产生列表的常用函数，如append或length函数。我们在[11]中，ned的层次程序类，其中递归调用只允许在尾部位置。对于这个类，我们得到一个nite抽象模型。然而，这种限制对程序员来说太强了。一个函数的尾部递归版本，如果存在的话，可能是非常复杂和低效的。 这也可以在示例2.1中看到。函数insert/2将一个新元素插入到列表中，相对于键的排序，也是非层次的。因此，这个程序的抽象域对于每个抽象解释都有一个内部状态空间。问题的根源是非尾递归函数调用，这导致了具有上下文无关结构的nite转换系统。对于特殊类的上下文无关的转移系统，已经证明，模型检查是可判定的[4，3]，并且这些理论结果似乎可以在这里使用。F. 胡赫202但我们并不是只有一个与上下文无关的过渡系统。我们在多个进程中有几个这样的进程，它们可以相互通信一个行为类似堆栈的进程可以编程如下：stack（P）->receivepop -> pop;X -> stack（P），P！X，栈（P）结束。如果这个进程接收到消息pop，那么它会将堆栈中存储的最后一条消息发送给pid为P的进程。所有其他消息都被压入堆栈。有了两个像这个堆栈一样的进程，就有可能在不使用任何数据结构的情况下模拟图灵机。因此，同样的图灵机也可以用一个只包含ve个值的抽象域来模拟（pop，tap上的一个符号，blank和两个进程的pid）。在LTL中，可以指定一个特殊的状态是可达的。这个状态也可以是程序的最终状态，我们可以指定模拟图灵机的终止。因此，这些系统的验证一般是不可判定的，即使对于Nite域抽象也是如此。我们需要对nite或上下文无关模型的非尾递归函数调用进行抽象，该模型仅由一个上下文无关过程产生。第二种可能性对于实践来说似乎过于复杂，因为不清楚应该从哪个过程中保留与上下文无关的结构。因此，我们抽象出一个nite模型。抽象必须包含在nite模型中，因为我们想用线性时间逻辑（LTL）的模型检测来证明程序的性质。6图语义在[11]中定义的Core Erlang语义中，我们无法检测Erlang术语的哪些部分属于哪个函数调用。在应用函数定义之后，右侧在调用它的上下文中消失。我们无法探测到它的终点。调用堆栈未显式表示。为了使这些调用和返回更加可见，我们在某种程度上更接近实现。我们将一个Erlang术语拆分为一个Erlang上下文堆栈当一个函数被调用时，它的上下文被存储在堆栈上，对应的右手边是下一个需要计算的项。如果实际值是基础值（不能再计算），则从堆栈中弹出下一个上下文，并将值放入孔中。评估将继续此Erlang项。评估项的这些堆栈表示由SR（S）：= ET（S）（FS（p）EC（S））定义，其中S是可能的值。堆栈还包含了当这个上下文被压入时调用的函数的名称。这在图表示中是非常不合理的，但我们稍后将使用这些信息进行抽象。这种技术可以应用于Erlang语义。但是在Core Erlang的语义中，所有进程都是交错的，进程的关键调用和返回不能被轻易地识别和修改这里我们只F. 胡赫203一一Y =（a1;：;an）r：Y =a1n1n“啊！B1. （E[a;e]; W）！ （E[e]; W）2. （E[a！b]; W）！（英[b];西）3.（E[selfY =自身];W）！（E[Y ];W）P = a其中Y2=Vars（E）4. (E[p=a];W）！（E[a];W）（i;？pi）5. （E[receivep 1->e1;：; pn->enen d]; W）！（E[ei]; W）81in（i; pi = a）6. （E[caseaofp 1->e1;：; pn->enen d]; W）！（E[ei]; W）81in7.(E[（a 1;：; a n）];W）！（E[Y];W）其中Y Y =spawn（f; a）2=Vars（E）8. （E[spaw n（f;a）]; W）！（E[Y]; W）其中YIc：X= a9. （f（a）; W）！ （ef; W） 其中f（X）->ef. 2个pc：X=2=Vars（E）10. （E[f（a）]; W）！ （ef;（f;E）W）其中f（X）->ef. 2p和E6=[]11. （a;（f;E）W）！（E[Y]; W）其中a2TC（Vars）和Y2=Vars（E）图一： Core Erlang的堆栈图表示表示一个进程的行为这使得分析更容易。 我们定义了一个预编译，它将一个Core Erlang函数转换为一个转换系统，该系统描述了从该函数开始的进程的行为。这个想法是所有的行为都可以自由解释 这个转换系统中的弧被标记为过程可能执行的行为/动作。这些状态被标记为必须被评估的Erlang项与SOS的唯一区别是，变量也可能出现在CoreErlang术语中。这些变量稍后将使用值实例化因此，我们也可以将自由解释中的变量处理为值下一次求值的位置与具体的变量绑 定 无 关 。 结 果 就 是 关 系！ SR （ TC （ Var ） ） Act SR （ TC（Var））在图1中定义。所有行为的集合应该从图中清楚地前八条规则只是对行为的自由解释。在receive和case的规则中，我们必须考虑分支。图案的正确顺序很重要。因此，我们对相应弧中的模式进行编号并保持其顺序。 如果一个动作的结果必须在后续的状态中使用，那么我们引入一个新的变量Y。操作的结果绑定到Y，Redex被Y替换。函数的调用为上下文产生一个新的堆栈帧，函数在其中被调用（10）。 在SOS中，我们还必须在此时将变量绑定推送到运行时堆栈，并继续绑定被调用的函数f.这被转换标签c：X=2保留。 如果一个函数在空上下文中调用，我们使用尾递归优化（9）来保证-antee是一个只使用尾递归的程序的nite图表示，如[2]我们把X写成X;：;X的缩写，[A]： ]和c：X=为c：X1=a1; ： ： ： ;Xn =an. 从正文中可以清楚地看出。一一F. 胡赫204一一一B[一“！！ s 0;（;s;; ; ）;b ;;s0;; （请输入）Y =（a1;：; an）S！s 0;（; s; ; ;）;b ;（; s0; [Y =A（（a1）;：; （an））]; （请输入）Y =自身！ S;（; s; ; ;）;b0;（; s0; [Y = ]; ;）图2：图语义（顺序求值main（）-> main（）。如果我们不再有求值上下文，换句话说，Core Erlang术语是变量上的构造器术语，那么我们必须返回到最后一个上下文（11）。我们不能简单地将值a复制到洞中，因为a可能包含也出现在E中的变量。在SOS中，这些变量通常被绑定到不同的值。因此，在这里我们引入一个新的变量Y，它不会出现在E中，并将这个变量绑定到求值的结果a。这个图表示（GOS）的语义可以分别定义为AOS和SOS，只是我们用图表示中的状态和表示变量绑定的相应环境来此环境由实际变量绑定Subst：Var！A和调用堆栈上的帧的替换Subst堆栈。GOS的状态空间被定义为：State：=Pfin（Pdroc）;Pdroc：=PidSR（TCMcb：=Ab[（Var））SubstSubstMcbLa bel：=f！vbj bv2Abg [f？vbj2Ab g[f“ g我的天我们将GOS定义为;b 状态标签国家根据法律-belings of！. 它在图2{5}中定义。 这些规则只是将行动与抽象的解释结合起来。在分支的情况下，我们必须考虑s的所有后继者。对于它们的评估，我们使用函数allSuccs：SR（T C（Var））！Pfin（SR（T C（Var）：所有成功：=ftj sl tgSS0F. 胡赫205一一一一一一P = aS！ s 0且matchb（p;（a））=;（;s; ; ; ）;b ;（;s0;];;）（1; p1 = a1）（m; pm = am）allSuccc s（s）=fs1; ：;sm g ands！ s1; ： ;s！SM和（i;）2例病例匹 配 b（（p1; ：;pm）;v）;（; s; ; ; ）;b ;（; si;];;）（1;？p 1）（m;？（pm）allSuccc s（s）=fs1; ：;sm g ands！ s1; ： ;s！SM和（i;j;）2mbmatchb（（p1; ：;pm）;（v1; ：;vu））？VJ;（;s;（v1; ：;vj; ：;vu））0;b ;（;s;];;（v1; ：;vj1;vj+1; ：;vu））一图3： 图形语义{匹配一个！B！S和0！（b）第（1）款2pidb（（a））;（; s;; ; ）（0; t;0的整数;0）的范围内;;（;s0; ; ; ）（0; t;0的整数;0 ：（b））一Y =spawn（f; a）s0！s;init（f）=（sf;（X1; ：;Xn））且（a）=[v1; ：;vn];（;s; ; （请输入）;b;（; s 0; [Y = 0]; ;）;（0;s ; [X =v ;：X=v ];“;（））Af1 1n n图4：图语义{并发求值如果产生了一个新的进程，那么这个进程从产生的函数的图形表示的初始状态开始函 数 init：FS（p）！(SR(TC（Var）） Var）产生这个状态，也产生必须在函数调用中绑定：init（f）：=（（e f;“）; X）; if f（X）-> e f. 2个pS0BF. 胡赫206在函数调用和返回的规则中（图5），我们分别从堆栈中推送或弹出实际的替换。此堆栈始终具有F. 胡赫207一一一一;（; s; ; ;）;;（; s; [X=a]; ;）B0一c：X=！S;（;s;）;b ;（;s0;[X=a]; ：;）Ic：X =！ Sr：Y = a！ S;（;s;;（0： ）;）;b ;（; s0;0[Y =a]; ;）图5： 图语义{函数调用与我们在图中使用的大小相同。将未完成的求值推到堆栈中还可以确保变量的作用域正确。更名是超级乌伊。我们在这里省略了运行时错误的规则。[11]他们可以很容易地添加。图语义和AOS对于任意Core Erlang程序都是等价的.这并不奇怪，因为我们的翻译对应于编译器构造中的标准技术。我们使用堆栈类似于过程调用的实现。因此，等效性应该直观清楚。这种等价性不是本文的主要观点。等价性的形式化在技术上已经是昂贵的。等价性的形式因此，我们省略了形式化和证明。我们将使用这种图表示来进行抽象，但我们也可以使用它来更有效地实现抽象和模型检查。在第一个实现中，我们使用Core Erlang评估术语来识别状态。在构造抽象模型时，需要对循环进行检测。因此，必须存储状态。对于转换系统中的每个新状态，计算其后继状态并与存储的状态进行比较。只有对于新的状态，必须计算进一步的后继者。但是状态的存储需要大量的空间，状态的比较需要大量的时间。因此，状态的紧凑表示是期望的。图表示是一个转换系统，其中的转换表示一个进程的行为。状态的标签仅用于其构造，但在此之后，它们是超级有用的，请参见图2。5.我们可以用数字代替它们。然后我们用这些数字作为进程所处状态的名称来构造交错转移系统。这是一个更紧凑的状态表示，并允许更快的验证，甚至更大的系统。此外，我们不必在生成模型的过程中降低评估上下文接班人SSS000F. 胡赫208Ic：X=X（f（X）j“）（情况X为 ：j“）（2;N）（1;0）（bj“）“（bj“）（self！a，f（X-1），self！bj“）（P！b）、（P！a）、（f（Z），self！bj“）（Y，self！bj“）c：X=Z（1;0）r：Y=b（caseXof：j（f;[]，self！b））（bj（f;[]，self！（b））（2;N）（self！a，f（X-1），self！bj（f;[]，self！b））（P！b）、（P！a）、（f（Z），self！bj（f;[]，self！b）） （Y，self！b;（fj（f;[]，self！（b））c：X=Z（1;0）r：Y=b（caseXof：j（f;[]，self！b）2）（bj（f;[]，self！（b）（2）（2;N）P！B（self！a，f（X-1），self！bj（f;[]，self！b）2） （P！bj（f;[]，self！（b）（2）..图6： 示例6.1的图形表示可以更有效地评估状态。但是对于非层次化的Core Erlang程序，这个图形表示是在nite中的：例6.1考虑以下函数定义： f（X）-> case Xof0 -> b;N->self！a，f（X-1），self！b端。执行此函数的进程将X次原子a发送给自己，然后再发送X次b。结果的图形表示如图6所示。为了更好地区分核心Erlang术语和堆栈中的逗号，我们使用j将评估术语与上下文堆栈分开。为了保持图形更紧凑，只显示有趣的过渡。像引入新变量这样的转换被省略了。F. 胡赫209（f（X）j“）Ic：X=X（case Xof：j“）（2;N）（1;0）（bj“）“（bj“）（self！a，f（X-1），self！bj“）（P！b）、（P！a）、（f（Z），self！bj“）（Y，self！bj“）c：X=Z（1;0）r：Y=b（caseXof：j（f;[]，self！b）） （bj（f;[]，self！（b））（2;N）（self！a，f（X-1），self！bj（f;[]，self！b））（P！b）、（P！a）、（f（Z），self！bj（f;[]，self！b））（Y，self！bj（f;[]，self！（b））图七： 示例6.1的抽象图形表示7非尾递归函数调用非尾部递归函数调用的抽象思想类似于数据抽象的思想。我们构造了一个包含GOS所有路径的抽象变迁系统。因此，抽象对于用LTL表示的我们的方法是一种调用字符串方法[20]在程序层面。抽象是为Core Erlang程序的图形表示而定义的，并在[13]中通过多个示例进行了非正式描述和激励。 这个想法是在图形表示中的nite递归中削减o。我们可以检测到这种递归，因为我们在图表示中跟踪了调用的函数。如果一个函数被第二次调用，我们不展开递归。相反，我们跳回到图形表示中的状态，在这个状态中，这个函数之前已经被调用过了。 请参见图7中相应地，我们添加从抽象函数调用执行终止的状态（这些状态与抽象调用的目标状态具有相同的堆栈，并且它们的主体被减少为值或变量）到抽象函数调用结束的状态的返回跳转（参见图7中的虚线返回转换）。由这些状态诱导的图形表示表示抽象函数调用的上下文的动作。如果一个函数是从程序中的多个点递归调用的，那么这将导致可能的返回跳转的不确定性。然而，这是必要的，因为我们的控制流抽象是安全的在这个例子中，我们没有考虑在r（0）：Y=bc（0）：X=ZF. 胡赫210抽象函数调用的上下文。例7.1代替 b，我们发送变量X的值：f（X）-> caseXof0 -> b;N -> self！a，f（X-1），self！X端。这个进程发送n次a给它自己，然后它发送数字1;：; n，其中n2 IN是值，f被调用。在这个例子中，我们在抽象返回中为抽象函数调用的上下文的自由变量（在这个例子中是变量X）添加了一个绑定。因此，我们使用最少的元素？抽象域3：r：Y=b;[X =？]（b j（f;[];self！X））！ （Y，self！Xj（f;[];self！（X））在例6.1中，函数f的递归调用是直接的。在中间不调用但一般来说，间接递归也是可能的。在这种情况下，被调用函数的堆栈必须在抽象调用中缩短，并在相应的返回跳转中重构。因此，我们在抽象图表示中扩展了调用和返回标签，并在GOS中分别添加了删除的堆栈元素的数量。对于直接递归函数调用，它们为零。在堆栈的重建中，我们还必须重建变量的绑定。我们再次为这些绑定使用抽象域的最小元素，因为具体绑定无法重构。关于我们的ow-abstraction思想的更详细的讨论，请参见[13]。为了区分已经绑定到值的变量和未绑定的变量，我们在绑定变量时用标签（0）标记变量。这是必要的，因为Erlang没有作用域，只有绑定一次的变量。我们定义了一个函数标记，它标记了一组变量。（V; X）=x0的 ，如果X 2 V： X，否则这个函数也被规范地扩展到Core Erlang术语和上下文。图8中定义了Core Erlang的图形表示，其中包含堆栈和绑定变量的标记。每个绑定到值的变量都被标记。这种标记只是一种附加信息，标记的变量被视为未标记的变量。在转换标签中，我们只使用变量的名称，而忽略标签。他们对GOS来说是超级强大的。递归是通过跳回到同一函数的最后一次调用来抽象的。如果已经调用了相同的函数，则在调用堆栈中检测到它的3在我们的框架中，抽象域不能包含最小元素，但它总是可以添加的。F. 胡赫211一一8> （f;E）（W）;如果j（W） jf=0“啊！B1：（E[a;e]; W）！ （E[e]; W）2：（E[a！b]; W）！（英[b];西）3：（E[selfY =自身];W）！（E[YP = a0];W）其中Y2=Vars（E）4：（E[p= a];W）！（tag（Vars（p）; E[a]）;W）（i;？pi）5：（E[receivep 1->e1;：; pn->enend]; W）！（tag（Vars（pi）;E[ei]）; W）6：（E[caseaof p1-> e1;：：：;pn->enend];W）（i; pi = a）！（tag（Vars（pi）;E[ei]）; W）81inY =（a1;：; an）第七章： （E[（a 1;：; an）];W）！（E[Y0];W）其中Y2=Vars（E）8：（E[产卵Y =spawn（f; a）（f;a）];W）！（E[YIc：X=0];W）其中Y2=Vars（E）9：（f（a）; W）！ （ta g（fXg;ef）; W） 其中f（X）->ef。2个pc：X=10：（E[f（a）]; W）！ （ta g（fXg;ef）;（f;E）W）f（X）->ef.2p^E6=[]r：Y = a11：（a;（f; E）W）！（E[Y0];W），其中a 2 TC（V ars）和Y 2=Vars（E）图8：Core Erlang的图形表示，带有堆栈和标记的实例化变量此跳转的目的地状态具有比调用将产生的更小的调用堆栈。为了将图形表示中的调用堆栈与它们的抽象表示相关联，我们定义了一个抽象函数。这个函数产生调用堆栈，它是通过逐步执行抽象调用来构造的。如果已经调用了同一个函数，则堆栈减少。（“）=“（（f; E）W）=<（f;E0）V ;如果（W）=U（f;E0）V>：其中jU jf= jV jf=0从定义上看，并不能直接清楚地表明是全部的。通过下面的引理，我们看到（（f; E）W）的两种情况中总是有一种匹配。因此，是一个总函数，并为所有调用堆栈定义引理7.2对于所有调用栈W和所有函数f2FS（p），j（W）jf1. 证据关于W的简单归纳：W=“。琐碎F. 胡赫212W=（f;E）W0.通过归纳，我们知道，j（W0）jf1. 我们区分两种情况：F. 胡赫213ff一GgffF1Kct包含Act以及抽象调用和返回的操作。 +已定义j（W 0）j = 0.因此，（W）=（f; E）（W0）且j（W）j = 1。对于所有的g6 =fj（W）j = j（W0）j1、归纳假设。（W 0）= U（f; E 0）V，其中jU j = jV j = 0。 然后 （W）=（f;E0）V和j（W）jf = 1。再通过归纳假设得到j（W）jg= j（V）jg1.2当调用函数时，我们使用这个抽象函数来分析给定的调用抽象图表示+SR（TC（Var））CTSR（TC（Var））可以用该抽象函数来定义。 的行动根据规则（1）{（9）和（11）！. 我们不使用呼叫站（10），而是使用它们的抽象表征：c（n）：X =（E[f（a）];（W））+（tag（fXg;ef）;（（f;E）W））其中f（X）-> e。2 p和E 6=[ ]和n = j（W）jj（（f; E0）W）j如果函数调用没有被跳转抽象，我们得到n = 1。 这意味我们可以将实际的上下文添加到调用堆栈中，就像我们在没有抽象的情况下一样。在这种情况下，我们只写c而不是c（-1）。否则，我们就加一个跳回。这意味着，我们检测递归并且j（W）jf = 1。 对于所有2 TC（Var）：（a;（（f;E）W））r（n）：Y = a[标记（E）=？]（1;：;n）+（E[Y0];（W* *W））其中Wn+1：Wk =((f; E）W），W 1：W n+1：W k =（W），以及Wi=（fi;Ei）且i=[taged（E i）=？]81我 n注意，仍然n = j（W）jj（（f; E0）W）j和n0始终成立，如果j（W）jf = 1。在这种情况下，W1：Wn是必须在该返回跳转中重新存储的块。这些块和E中的绑定变量是未知的。我们用？，抽象域中的最小元素。函数taged产生所有标记的变量。对于这些，我们可以定义新的替代物，使它们与？结合。这些是替代品[标记（E）=？]和（1;：;n）。我们把它们加到标签上。F. 胡赫214（X0j（g;[]，self！X0））（f（X0）j“）Ic：X=X（caseX0of：j“）（2;N）（g（X0- 1），self！X0j“）Z=X 1（g（Z0），self！X0j“）c：X=Z（1;0）（bj“）（1;0）（f（X0- 1），self！X0j（g;[]，self！X0））Z=X 1（f（Z0），self！X0j（g;[]，self！X0））c：X=Z（caseX0of：j（f;[]，self！X0）（g;[]，self！X0））（2;N）（g（X0- 1），self！X0j（f;[]，self！X0）（g;[]，self！X0））Z=X 1（g（Z0），self！X0j（f;[]，self！X0）（g;[]，self！X0））c（1）：X=Z（bj（f;[]，self！X0）（g;[]，self！X0））（X0j“）r：Y = bP！X（Y0，self！X0j（g;[]，self！X0））（P！X0j“）P=自我（P0！X0j（g;[]，self！X0））（Y0，self！X0j“）P！Xr：Y=Xr（1）：Y=XX=？（[X=？]）（Y，self！X0j（f;[]，self！X0）（g;[]，self！X0））P=自身（P！X0j（f;[]，self！X0）（g;[]，self！X0））P！X（X0j（f;[]，self！X0）