异步方法调用：面向对象并发模型的运行时环境和操作语义

理论计算机科学电子笔记117（2005）375-392www.elsevier.com/locate/entcs具有异步方法调用的并发对象运行时环境Einar Broch Johnsen，Olaf Owe，and Eyvind W.阿克塞尔森信 息 学 系 ， 奥 斯 陆 大 学 POBox 1080Blindern，N-0316 Oslo，Norway电子邮件：{einarj，olaf，eyvindwa}@ifi.uio.no摘要分布式系统可以由并发运行的对象建模，每个对象都有自己的处理器，并通过远程方法调用进行通信。 然而，对象可能不得不等待对外部调用的响应;这可能导致处理器容量的低效使用，甚至导致死锁。本文通过异步方法调用和条件处理器释放点来解决这个限制。虽然以对象中额外的内部不确定性为代价，但这种方法在异步或不可靠的分布式环境中似乎很有吸引力。 这些概念由小型面向对象语言Creol及其操作语义来说明，该操作语义是使用重写逻辑作为语义框架来定义的。因此，Creol规范可以用Maude作为语言解释器来执行，这允许在Maude中测试支持的语言结构及其操作语义的增量开发。然而，对于高度不确定性系统的原型，Maude的确定性引擎可能会限制实际测试。为了克服这个问题，提出了一种基于伪随机数发生器的重写策略，为Maude提供了不确定性行为。关键词：面向对象，异步方法调用，操作语义，重写逻辑，非确定性重写策略1介绍随着分布式计算的发展，进程间通信的重要性正在迅速增加，无论是在互联网上还是在本地网络上。面向对象似乎是并发和分布式系统的一个有前途的框架[20]，但通过方法调用进行的对象交互通常是同步的，因此不太适合分布式环境。需要直观的高级编程结构以自然的方式统一面向对象和分布。本文编程1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.06.012376E.B. Johnsen等人理论计算机科学电子笔记117（2005）375基于处理器释放点和异步方法调用，用面向对象的设计语言Creol提出了并发对象的构造。处理器释放点用于加强并发对象中的隐式内部控制流。这减少了在分布式环境中等待对方法调用的响应所花费的时间，并允许对象在活动和响应行为（客户端和服务器）之间动态更改。我们考虑如何面向对象的方法调用，返回输出值响应输入值，可以适应分布式设置。在远程过程调用（RPC）模型中，一个对象是通过一个过程调用来激活的[6]。控制权随调用一起转移，因此在调用方和被调用方之间存在主从关系。并发是通过多个执行线程来实现的，例如Hybrid [26]和Java [19]。在Java中，当线程在同一对象中并发操作时，与共享变量相关的干扰问题再次出现，并且在这种设置下对程序进行推理是一件非常复杂的事情[1，11]。推理考虑建议所有方法都应该序列化[9]，这是Hybrid采用的方法。但是对于序列化方法，调用者必须等待调用的返回，从而阻塞对象中的任何其他活动。 在分布式设置中， 由于分发造成的延误和不稳定可能造成相当长的等待时间。相反，消息传递是一种没有控制转移的通信形式。对于同步消息传递，就像Ada的Renault机制一样，发送方和接收方都必须在通信发生之前准备好。方法调用可以由成对的消息来建模，两个对象必须同步[6]。对于分布式系统，这种同步仍然会导致大量等待。在异步设置中，无论接收方何时接受消息，消息都可以被发送。通过异步消息传递的通信是公知的，演员模型[2，3]。然而，方法调用意味着在Actor模型中不容易捕获的通信顺序。本文将方法调用作为并发对象的通信原语，给出了一种由异步消息对反映的操作语义，允许消息超越。其结果类似于使用所谓的未来变量进行编程[8，10，16，28，29];计算可以继续，直到代码中显式需要调用的返回值。为了避免在这一点上阻塞对象，我们建议通过使用内部保护在方法体中定义潜在的处理器释放点来在对象因此，当前的活动可能被挂起，允许对象Creol的操作语义已经在重写逻辑[23]中定义，这是由可执行建模和分析工具Maude[13]支持的。E.B. Johnsen等人理论计算机科学电子笔记117（2005）375377重写逻辑是一种并发变化的逻辑重写逻辑和Maude [23，24]中已经成功地表示了许多并发模型，包括ODP计算模型[25]和结构操作语义[17]。我们已经使用重写逻辑和Maude作为一种工具，用于开发分布式并发对象的高级编程结构。由于我们的目标是考虑传统命令式设置的构造，重写规则捕获抽象机器的行为，而不是重写逻辑和Maude [13，23]的对象模型中的方法调用。我们的实验表明，重写逻辑和Maude提供了一个非常合适的框架，实验语言结构和并发环境。然而，为了捕捉分布式系统的非确定性，Maude的确定性引擎可能是一个限制。为此，提出了一种基于伪随机数发生器的Maude重写策略。这允许非确定性执行，不仅根据随机数选择重写规则，而且还根据应用的位置选择重写规则。该策略似乎非常适合测试任何不确定的Maude规范，因为相同规范的多次运行会导致不同的执行。文件概述。第二节介绍克里奥尔语的祈使句层次。第3节提供了一个例子。第4节使用重写逻辑定义Creol第5节提出了一个不确定性重写策略的Maude。第6节考虑相关工作，第7节结束。2编程构造本节提出了基于异步方法调用和处理器释放点的分布式并发对象的编程结构。并发对象是潜在的活动对象，封装执行线程;但基本数据类型的元素不被视为对象。在这个意义上，我们的对象类似于顶级对象，例如。混合动力[26]。对象有显式标识符：通信发生在命名对象之间，对象标识符可以在对象之间交换所有的对象交互都是通过方法调用实现的。Creol对象由抽象接口类型化[21，22]。这些类似于CORBA该语言支持强类型，例如。被调用的方法由被调用的对象支持（当不为null时），并且形式参数和实际参数匹配。为了集中讨论异步方法调用和方法体中的处理器释放点，将不详细讨论其他语言方面，包括继承和类型。为了简化说明，我们假设可以传递的基本数据值的公共类型Data378E.B. Johnsen等人理论计算机科学电子笔记117（2005）375作为方法的参数，包括作为对象标识符Obj和数据类型（如Bool）的子类型。ExpressionsExpr计算为Data。我们用Var表示程序变量的集合，用Mtd表示方法名的集合，用Label表示方法调用标识符的集合。2.1类和对象在编程级别，属性（对象变量）和方法声明以标准方式组织在类中。对象是类的动态创建的实例。对象的属性是封装的，只能通过对象的方法访问。 在声明的方法中，我们区分了init和run两个方法，它们在操作上被给予了特殊的处理。init方法在对象创建时被调用以实例化属性，并且可能不包含处理器释放点。初始化后，如果提供了run除了init和run之外，声明的方法可以被适当接口的其他对象调用。这些方法反映对象中的被动或反应行为，而run反映主动行为。 对象活动是围绕外部消息队列和包含挂起进程的内部进程队列组织的。 方法不需要终止，除了init之外，所有方法都可以在内部进程队列上暂 时 挂 起 。2.2异步方法一个对象将方法传递给它的环境，通过一些接口来指定。与对象的所有交互都是通过其接口的方法进行的。在异步设置中，总是可以发出方法调用，因为接收对象不能阻止通信。方法超越是允许的，因为如果对象所引用的方法以一种顺序被调用，则对象可以以另一种顺序对调用做出反应。方法，粗略地说，是由嵌套的保护命令G−→C实现的，在局部绑定变量的上下文中进行计算。受保护的命令将在2.3节中详细讨论。由于不同方法执行的可能交错，如果方法实例在完成之前挂起，则对象的实例变量的值不完全由方法实例控制。但是，方法可以创建补充对象变量的局部变量。特别地，形式参数的值被本地存储，但是其他局部变量也可以被去clared。从语义上讲，实例化的方法是一个进程，表示为一对其中GC是（受保护的）命令序列，L：Var→Data本地变量绑定。 考虑一个对象，它继承方法E.B. Johnsen等人理论计算机科学电子笔记117（2005）375379opm（inx：Dataouty：Data）==varz：Data：= 0;G−→C.对环境接受来自对象oJ的调用invoc（l，oJ，o，m，2）会将对<$G-→C，{label<$→l，caller<$→oJ，x<$→2，y<$→nil，z<$→ 0}<$添加到对象o的内部进程队列中，其中挂起进程等待对象处理器。一个对象可以有多个对同一方法的挂起调用，这些调用可能具有不同的局部变量值。局部变量label和caller被保留以标识调用和应答的调用方，应答在方法终止时发出异步方法调用是用命令l！o.m（e），其中l∈Label是对调用的唯一引用，o是对象标识符，m是方法名，e是带有实际参数的表达式列表。 标签用于标识回复，如果没有明确请求回复，则可以省略标签。由于不涉及同步，流程执行可以在调用外部方法之后继续，直到流程需要返回值为止。为了从队列中获取返回值，比如在变量列表x中，我们要求对调用的回复：l？（十）.如果回复已经到达，则返回值被分配给x，并且执行没有延迟地继续。如果没有收到对调用的应答，则进程现在必须等待。 l的解释？（x）给出了与将x视为未来变量相同的结果。然而，通过为应答请求引入处理器释放点，可以完全避免异步情况下的等待。在没有回复的情况下，执行被挂起，将活动进程及其局部变量放在内部进程队列中。虽然远程和本地调用可以以相同的方式操作处理，但很明显，对于本地调用的执行，调用进程甚至必须挂起自己的执行。特别地，同步本地调用被给予对对象处理器的直接访问。 语法o.m（e;x）用于同步（RPC）方法调用，在等待答案。 本地调用不需要由对象标识符来前缀。2.3一种具有处理器释放点的语言在Creol中，并发对象内部的控制流可能会受到潜在处理器释放点的影响。这些在方法体中使用保护命令显式声明，如Dijkstra [18]所介绍的那样，并且可以嵌套在同一个局部变量范围内。当内部防护在进程执行期间评估为false处理器释放后，从内部进程队列中选择一个已启用的进程执行。定义2.1类型Guard归纳构造如下：• wait∈Guard（explicit release）380E.B. Johnsen等人理论计算机科学电子笔记117（2005）375句法分类。定义。C inComGC 在 Gcom中G在Guard 中 x在VarList中ExprList中的e我在Mtd在Objl标签C：：= ε|x：= e|GC|C1; C2|新类名| if G then C 1 else C 2 fi| 而G做C od| m（e; x）|l！m（e）|！m（e）|我吗？（十）| o.m（e; x）|l！o.m（e）|！o.m（e）GC：：=G−→C| GC 1 Q GC 2| GC2|||GC 2Fig. 1.建议的语言克里奥尔语的语法大纲，重点是命令的主要语法类别Com和保护命令的Gcom• 我吗？（x）∈Guard，其中l∈Label且x∈Var• φ∈Guard，其中φ是局部变量和对象变量的布尔表达式这里，wait是一个用于显式释放处理器的构造。回答守卫l？（x）检查是否收到对方法调用的回复，因为进程的进一步执行通常取决于某个回复的到达。如果是这样，我？（x）返回true并使用返回值实例化x。警卫的评估是原子地完成的。受保护的命令可以以不同的方式组成，反映对象中内部控制流程的要求。设GC1和GC2表示保护命令G1−→C1和G2−→C2。防护的嵌套是通过顺序组合获得的;在程序语句GC1;G2−→C2中，防护G2对应于潜在的内部处理器释放点。保护命令之间的非确定性选择由GC1QGC2表示，如果G1评估为真，则GC 1 QGC 2可以计算C1，如果G2评估为真，则计算C2，否则被挂起。非确定性合并由GC1表示|||GC2，可以定义为（GC1; GC2）Q（GC2; GC1）。普通的控制流由if和while结构表示，对局部和对象变量的赋值表示为x：=e，用于程序变量的列表x和表达式的列表e。图1总结了语言语法。使用嵌套的处理器释放点，处理器不需要主动等待响应。这种方法比未来变量更灵活：挂起的进程或新的方法调用可以被评估，而不是阻塞处理器。但是，当回复到达时，原始进程的继续必须与内部进程队列中的其他已启用和挂起的进程竞争。3英文名：The Dining Philosophers著名的用餐哲学家现在被认为是克里奥尔语。该示例稍后将用于实验语言解释器。一个管家E.B. Johnsen等人理论计算机科学电子笔记117（2005）375381告知哲学家其左邻居的身份。一个哲学家可以借他邻居的钱，然后还回去。哲学家和管家之间的互动受到界面的限制。 这导致了内部方法和外部方法之间的明显区别，这些方法可以通过所谓的cointerfaces类型化[21，22]。它们表示接口之间的相互依赖性，并通过with构造在接口中声明。 强类型和协接口保证了只有哲学家才能调用这些方法。接口菲尔接口巴特勒开始与PhilopstickopgetNeighbor（ outn：Phil）操作返回斗杆末端末端在这种方法中，哲学家对象显示主动和被动的特性。每个哲学家都控制着一个盘子，为了吃饭，他们必须借用邻居的盘子。因此，哲学家有他们的内部活动，以及回应来自环境的呼吁。用餐哲学家的标准配置最容易通过一个管家获得。3.1实施哲学家Philosophers是活动对象，因此Philosopher类将包含一个run方法。这种方法是根据代表哲学家内部不同活动的几种无休止的内部方法来定义的：思考，吃，消化。在run中，内部方法被异步调用，并且将以不确定和非终止的方式交错，说明了处理器释放点构造。这三种方法都依赖于内部变量hungry的值。think方法是一个循环，它在每次迭代之前暂停自己的评估，而eat则试图抓住对象在这种情况下，哲学家必须等到两个筷子都可用。为了避免阻塞对象处理器，eat方法在请求邻居的守护后被挂起消化方法代表饥饿的动作。类可以包含类参数，这些参数在创建对象时成为实例属性，就像在Simula中一样。哲学家阶级的定义如下：类Philosopher（butler：Butler）实现Phil开始var饿了：bool，饿了：bool，邻居：Philop init == hunger：= true; hungry：= false; butler.getNeighbor（;neighbor）.操作运行== true −→！认为|||true −→！吃|||true −→！消化OPthink == not hungry −→饥饿的思考. ;wait −→！想的382E.B. Johnsen等人理论计算机科学电子笔记117（2005）375op eat == var l：label; hungry−→l！neighborhood. neighborhood.neighborhood stick;（邻居？())−→吃东西. 饿了么：=false;！neighbor.returnStick;wait−→！吃吧opdigest == not hungry −→（hungry：= true; wait −→！digest）。与菲尔opwStick == − →：= false.op returnStick ==：= true.端此实现支持隐式控制对象的活动行为。Caromel和Rodier认为，在处理并发编程的语言中需要隐式和显式控制的设施[10]。显式活动控制可以通过在run方法中使用while循环在Creol中编程。然而，在异步分布式系统中，我们认为通信引入了如此多的不确定性，以至于显式控制结构很快导致程序过度指定，并可能导致不必要的主动等待。与积极的哲学家相比，管家是被动的。在初始化期间创建哲学家之后，管家等待哲学家请求其邻居的身份。butler类的代码很简单，因此这里省略了。4Creol语言的逻辑语义重写使用重写逻辑（RL）提供的语义框架给出了建议的语言结构的操作语义。重写理论是一个4元组R=（E，E，L，R），其中签名E定义了语言的函数符号，E定义了术语之间的等式，L是一组标签，R是一组标签重写规则。从计算的观点来看，重写规则t→tJ可以被解释为允许模式t的实例演变成模式tJ的对应实例的局部转变规则。 重写规则适用于状态配置的局部片段。规则可以并行应用于不重叠的子配置。我们假设RL是已知的读者和目前的操作语义的语法Maude。重写规则将捕获Creol抽象机的行为，而不是Maude对象模型中的Creol对象。因此，配置是组合了Creol对象、消息、队列和类的多集。辅助函数在等式逻辑中定义，并在重写步骤之间进行评估[23]。通常，多集的关联和交换构造函数以及列表的关联构造函数都是用空白表示的。一个RL对象是一个类型为CAMO：C的项|a1：v1，. ，an：vn，其中O是对象我们采用这种形式E.B. Johnsen等人理论计算机科学电子笔记117（2005）375383表示和定义Creol对象，类和外部消息队列作为RL对象。省略RL类型，Creol对象由RL对象的URL ID表示|Cl，Pr，PrQ，Lvar，Att，Lcnt，其中Id是对象标识符，Cl是类名，Pr是活动进程代码，PrQ是允许各种队列排序的挂起进程的多集（见2.2节），Lvar和Att分别是局部变量和对象变量。最后，Lcnt是对应于语言中标签的方法调用标识符。因此，对象标识符Id和本地标签值为每个方法调用提供了全局唯一的标识符。外部消息队列有一个名称，并包含一组未处理的消息。每个外部消息队列都与一个特定的Creol对象相关联。Creol类由RL对象表示|Att、Ocnt、init、run、Mtds，其中Cl是类名，Att是属性列表，Ocnt是类实例化的对象数，Mtds是一组方法。 当一个对象需要一个方法时，它从它的类的Mtds集合中加载（本文忽略了与继承相关的重载和虚绑定问题在RL的对象模型[ 23 ]中这导致了处理对象创建的特殊机制，我们通过在配置中表示Creol类来避免。Creol命令new C（args）将创建一个新的对象，该对象具有唯一的对象标识符，对象变量列在类参数列表中，值在args和Att中定义，并将方法init和Pr中的代码放在Pr中运行。对象标识符的唯一性是通过将数字Ocnt附加到类名并增加Ocnt来确保的。有四种不同的重写规则：• 从活动进程执行代码的规则：对于每个程序状态，至少有一个规则。例如，程序X：=E的赋值规则将表达式E的值绑定到局部变量列表或对象变量列表中的X。• 挂起活动进程的规则当活动进程防护值为false时，进程及其局部变量被挂起，Pr为空。• 激活挂起进程的规则：当Pr为空时，可以激活挂起进程。当进程被加载时，它的局部变量也被加载到内存中。• 传输规则：这些规则将消息移入和移出外部消息队列。因为外部消息队列被表示为一个单独的RL对象，所以它可以属于与对象本身不同的子配置。因此，消息可以与384E.B. Johnsen等人理论计算机科学电子笔记117（2005）375物体中的其他活动RL中的规范可以在Maude工具上执行，因此Creol的操作语义可以用作语言解释器。整个解释器由700行代码组成，包括辅助函数和等式规范，它有32条重写规则。解释器的详细介绍可以在[7]中找到。异步方法调用和保护命令的规则现在被更详细地考虑。4.1异步方法调用对象通过异步方法调用进行通信。在操作语义中，两个消息用于对方法调用进行编码。 如果对象o1调用对象o2的方法m，参数为in，并且m（in）的执行导致返回值out，则调用由两个消息invoc（l，o1，o2，m，in）和comp（l，o1，out）响应，这两个消息分别表示调用的调用在异步设置中，调用消息必须包括调用方的应答地址，这样完成就可以传输到正确的目的地。由于一个对象可能有几个对另一个对象的挂起调用，完成消息包括一个由调用者生成的唯一标签l当一个对象调用一个外部方法时，一个消息被放置在配置中。传输规则最终将消息移动到被调用方在方法执行之后，一个完成消息被发送到配置中，最终到达调用者解释器检查Creol对象的外部消息队列中的方法调用，并将对象类中相应的方法代码加载rl [receivecall]：中文（简体）|Cl：C，PrQ：W|Ev：Qinvoc（N，OJ，O，M，I）氯：氯|中文（简体）中文（简体）|Cl：C，PrQ：（get（M，MT，（N OJI）W|Ev：Q氯：氯|- 是的辅助函数get从类的方法集合MT中获取方法M，并返回一个包含方法代码和局部变量的进程实际参数I、调用者OJ和消息标签N的值存储为局部变量。(The标签不能被进程修改。）规则对于本地异步调用也是类似的，但是调用来自活动进程代码Pr而不是外部消息队列。用于同步E.B. Johnsen等人理论计算机科学电子笔记117（2005）375385本地调用时，代码被直接加载到活动进程代码Pr中，因为在这种情况下主动等待会导致死锁。4.2守护命令Creol有三种类型的守卫代表潜在的处理器释放点：标准布尔表达式、等待守卫和返回守卫。目前正在审议评价现行进程中的返回警卫的规则。返回保护允许进程在等待方法完成时挂起，因此对象可以在等待时处理其他任务。如果外部消息队列包含方法调用的完成，则返回保护的计算结果为true，并且进程的执行继续。crl [returnguard]：中文（简体）|Pr：X？（J）−→ P，Lvar：L q（O）：QId |Ev：Q comp（N，O，K）中文（简体）|Pr：（J：= K）; P，Lvar：L|Ev：Q如果N==val（X，L）.该条件确保识别正确的回复消息。辅助函数val从局部变量L获取与标签变量X相关联的值。如果消息不在队列中，则挂起活动进程。在这种情况下，在等待方法调用完成时，其他启用的进程可能会被激活。crl [returnguard notinqueue]：中文（简体）|Pr：X？（J）−→P，PrQ：W，Lvar：L q（O）：QId |Ev：Q中文（简体）|Pr：空，PrQ：W（X？（J）−→ P，L），Lvar：no，q（O）：QId |Ev：Q如果不在队列中（val（X，L），Q）。其中函数inqueue在消息队列Q中查找完成。如果没有活动的进程，则可以再次针对外部消息队列测试具有返回保护的挂起进程。如果存在完成消息，则返回值与本地或对象属性匹配，进程被重新激活。crl [return guard st]：中文（简体）|Pr：空，PrQ：（X？（J）−→ P，LJ）WQiq（O）：QId|Ev：Q comp（N，O，K）中文（简体）|Pr：（J：= K）; P，PrQ：W，Lvar：LJ|Ev：Q如果N==val（X，LJ）.否则，可以激活来自多集合PrQ的386E.B. Johnsen等人理论计算机科学电子笔记117（2005）3754.3在MaudeCreol的操作语义可以在重写逻辑工具Maude上执行，作为Creol程序的解释器。这使得Maude非常适合尝试编程结构和语言原型，结合Maude虽然操作语义是高度不确定的，但Maude在选择应用于给定配置的规则时是确定的。第3节的哲学家就餐程序用于测试口译员的表现在解释器上运行示例，我们观察到Maude以不公平的方式从内部进程队列中选择进程。即使使用这意味着，尽管在每个哲学家中启用了摘要的挂起实例，但它不会被执行。 为了探索上述程序的完整状态空间，Maude提供了广度优先搜索工具。然而，对于高度不确定性的系统，这种搜索机制的天真使用往往会变得非常资源需求，难以在实践中应用。5非确定性执行本节介绍了Maude规范的非确定性执行方法。该方法是基于莫德的反应能力，以控制重写过程。非正式地，Maude规范的配置C和重写规则的集合R可以表示为元级的项C和R，并且元级重写规则可以用于从R中选择哪个规则应用于C的哪个子项。这是通过一个顺序解释器函数来完成的，它把一个有限表示的重写理论R、一个项C和一个确定性策略S作为参数。关于重写逻辑和Maude中反射的理论和使用的细节可以在[12，15]中找到。 使用伪随机数生成器的规则选择策略现在用Maude语法定义。存在用于生成伪随机数的大量算法选择为了简单起见，我们从Press等人[ 27，p. 278]中选择了一个简单的在[27]中，作者认为选择a=75和m=231− 1产生的生成器已经通过了所有重要的理论测试，并且已经在各种 实 际 应 用 中 成 功 使 用 。 该 算 法 在 Maude 中 编 程 为 功 能 模 块RANDOM：E.B. Johnsen等人理论计算机科学电子笔记117（2005）375387fmod RANDOM正在保护NAT。op rand：Nat→Nat .ops a m：→Nat.方程式a = 16807。* = 7 5方程式m = 2147483647。 * = 2 31− 1varN：Nat.等式rand（N）=（a N）remm. endfm非确定性重写策略被定义为保护内置模块META-LEVEL的Maude模块META-ENGINE。元级重写是由一个有条件的规则执行，如下所述。Engine对象跟踪当前状态，定义如下：操作系统引擎|curTerm：，curModule：，labels：，failedRules：，numRules：，randomNumber：，randomNum2：术语Qid QidList QidList Int Int Int →引擎对象。该对象包含几个属性，其值在运行时设置;curTerm包含当前配置的元表示，cur- Module是将执行重写的基本级别模块名称的元表示，labels是来自模块curModule的规则标签的QidList，failedRules包含无法应用于curTerm的规则的规则标签的QidList，numRules是标签列表的长度，出于性能原因而包括在内，最后random和random-Num 2是由上面定义的伪随机数生成器生成的数字。实际的元级重写步骤由Maude的内置下降函数metaXapply（R，t，l，σ，n，b，m）处理，其中R是模，t是项，l是规则标签，σ a（部分）替换，n是匹配数，b是边界，m是解决方案数[ 14 ]。最后一个参数，解决方案编号m，对于非确定性执行特别重要。我们执行重写的策略有两个方面：(i) 引擎将使用伪随机数生成器来选择与R中的规则相对应的规则标签l。(ii) 由l标识的规则可以在项t内的几个不同位置处适用于项t，在Maude中称为解。为了允许对象内部以及对象之间的“深度”随机化，我们还将伪随机地选择解决方案编号。条 件 重 写 规 则 exec 使 用 metaXap- ply 和 一 个 辅 助 函 数ExciseSolution（R，t，l，r）来实现这个策略。后者照顾388E.B. Johnsen等人理论计算机科学电子笔记117（2005）375并使用伪随机数r选择有效解数。它利用了metaXapply（R，t，l，σ，n，b，m）在没有解m时返回失败的事实。 因此，很容易找到可能的解决方案的数量s，通过反复调用metaXapply，增加m的值，直到它返回失败。 利用这一信息，随机选择一个解决方案就变成了计算r mod s的问题。如果找不到解（即规则不适用），则ExciseSolution返回-1。exec的代码如下：crl [exec]：发动机配件|curTerm：T，curModule：MOD，labels：L，failedRules：FR，numRules：NR，random rule：R，randomNum2：R2错误⇒if AdverseSolution（MOD，T，findItem（L，Rrem NR），R2）== −1然后发动机配件|curTerm：T，curModule：MOD，labels：L，failedRules：if findItem（L，Rrem NR）in FR thenFR else FR findItem（L，Rrem NR）fi，numRules：NR，randomNumber：rand（R），randomNum2：rand（R2）其他发动机配件|curTerm：getTerm（metaXapply（[MOD]，T，findItem（L，Rrem NR），none，0，unbounded，Boundary Solution（MOD，T，findItem（L，RremNR），R 2），curModule：MOD，labels：L，failedRules：nil，numRules：NR，randomNumber：rand（R），randomNum2：rand（R2）fi如果长度（FR）

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