Maude1的不变量驱动策略：通用、参数化的系统控制和逻辑表达，以及Maude作为策略参数的特性

理论计算机科学电子笔记124（2005）17-28www.elsevier.com/locate/entcsMaude1的不变量驱动策略FranciscoDur'an2Manue lRolda'n3AntonioVallecillo4Dp到。deLenguajesyCienciasdelaComputacio'nUniversidadeMa'laga马拉加、斯帕因摘要我们提出了通用的不变量驱动的策略，通过保证给定的不变量得到满足来控制系统的执行。我们的策略是通用的，在这个意义上，他们是参数化的系统的执行，他们控制，由逻辑表达的不变量，并由不变量本身。我们说明了在命题逻辑中表达的不变量的情况下使用的策略。然而，Maude作为一个逻辑和语义框架的良好特性，其中可以表达和执行许多不同的逻辑和形式主义，允许我们使用其他逻辑作为我们策略的参数保留字：执行策略，莫德，重写逻辑，反射。1介绍为了处理非终止和非连续系统，我们需要好的方法来控制重写推理过程。在这条线上，不同的语言或不同的机制，包括基于元编程的方法，如Maude [2，3]，或基于策略语言，如ELAN [1]。然而，尽管逻辑和控制的分离大大简化了这样的任务，但这些机制有时很难使用，特别是对于初学者，并且通常包含基本属性，如可扩展性，可重用性和可维护性。1由TIC 2001-2705-C 03 -02和2002-04309-C 02 -02项目部分支助2电子邮件：duran@lcc.uma.es3电子邮件：mrc@lcc.uma.es4 电子邮件地址：av@lcc.uma.es1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.11.01818F. Durán等人/理论计算机科学电子笔记124（2005）17像Z和UML这样的形式主义提出了一个有趣的替代方案，因为它们允许将不变量或约束定义为系统规范的一部分。虽然执行或模拟Z规范可能很难，但我们仍然可以找到像Possum [9]或Jaza [12]这样的工具，它们可以对此类规范进行合理的模拟。我们在UML中发现了一些类似的东西，在那里，通过在我们的规范上指定OCL约束，它们可以被执行[13]。执行或模拟具有约束不变量的规范通常基于以某种方式将不变量集成到系统代码中。然而，这样的集成显然不能令人满意：不变量在代码中丢失，并且变得难以定位、跟踪和维护。此外，程序和在它们上面满足的不变量通常用不同的形式主义来表示，并且存在于不同的抽象层次上：不变量是在程序上定义的。因此，有趣的是有某种方式来分别表达它们，从而避免不变量和代码的混合。Maude不提供对表示执行不变量的直接支持。然而，它确实提供了相应的能力和支持来控制执行过程，也是一个很好的工具，可以为各种逻辑和计算模型创建可执行的环境[4]。因此，它被证明是支持不同类型的不变量的一个非常好的候选者，这些不变量可以用不同的形式表示。在本文中，我们提出了通用的不变量驱动的策略，通过保证给定的不变量总是满足来控制系统的执行。我们的策略是通用的，在这个意义上，他们是参数化的系统的执行，他们控制，由逻辑表达的不变量，并由不变量本身。Maude作为一个逻辑和语义框架的良好特性[8]，其中可以表达和执行许多不同的逻辑和形式主义，这使我们可以说其他逻辑和形式主义可以用作我们策略的参数。在本文中，我们将使用命题逻辑的情况下，虽然我们也尝试了未来时间线性时态逻辑。本文件的结构如下。第二节简要介绍重写逻辑和莫德。第3节介绍了Maude对策略的定义，并作为第4节介绍不变指导策略的基础。第5节作为一个例子描述了使用命题演算表示的不变量的情况。最后，第6节得出了一些结论。F. Durán等人/理论计算机科学电子笔记124（2005）17192重写逻辑与莫德Maude [2，3]是OBJ [5]代数规范家族中的高级语言和高性能解释器和编译器，支持成员方程逻辑[11]和重写逻辑[10]规范和系统编程。隶属等式逻辑是一种霍恩逻辑，其原子语句是等式t=tJ和形式为t：S的隶属断言，声明项t具有排序S。这样的逻辑扩展了序排序的等式逻辑，并支持排序、子排序关系、子排序多态运算符重载以及具有等式定义域的部分函数的定义重写逻辑是一种变化逻辑，可以自然地处理状态和高度不确定的并发计算。在重写逻辑中，分布式系统的状态空间被指定为一个代数数据类型，用一个等式指定（E，E）表示，其中E是一个排序（类型）和操作的签名，E是一组（条件）等式公理。 重写逻辑中系统的动力学可以通过重写规则t→tJ来具体化，其中t和tJ是项。 这些规则描述了系统中可能的局部并发转换，即当系统状态的一部分符合模式t时，它可以改变为一个新的局部状态符合模式tJ。规则可以是有条件的，在这种情况下，守卫充当阻塞的先决条件，在这个意义上，条件规则只能在条件满足时才能被触发。在Maude中，面向对象系统由面向对象模块指定类是用语法声明的C类|a1：S1，. ，an：Sn，其中C是类的名称，ai是属性标识符，Si是相应属性的排序。类C的对象则是类似记录的结构，其形式如下：< O：C |a1：v1，. ，an：vn>，其中O是对象的名称，vi是其属性的当前值。对象可以以多种不同的方式进行交互，包括消息传递。消息在Maude中在msg子句中声明，其中定义了消息的语法和参数。在面向对象的系统中，一个被称为配置的状态具有由对象和消息组成的多集结构，该多集结构通过使用描述通信事件的结果的规则进行重写而演化。20F. Durán等人/理论计算机科学电子笔记124（2005）17JI1IkJJJJ对象和消息。 这种重写规则的一般形式是crl [r]：< O 1：C 1 |attts 1>. < On：Cn|联系我们M1... MmJ J=>. < Oik：Cik|联系我们< Q 1：CJJ|attsJJ>. < Q ：C | atts >>11pp pJ JM1... MQ如果条件。其中r是规则标签，M1. M m和MJ... MJ是信息O1n和1Q1... Q p是对象标识符，C1... Cn，CJ. CJQJJJJ荣登福布斯中国慈善榜榜... C是类，我1. Iki1ik1p是1的子集... n，Cond是布尔条件（规则的保护）。 的应用这样的规则的结果是：（a）消息M1. 我消失了，也就是说，它们被消费;（b）状态，以及可能的对象类O i1. O ik可能改变;（c）所有其他对象O j消失;（d）新对象Q1. Q p是创建;以及（e）新消息MJ. MJ被创建，即， 它们被发送。规则1Q标签和防护装置是可选的。例如，下面的Maude模块DINING-PHYSSOPHERS具体说明了饥饿哲学家的众所周知的问题。这个问题假设五个哲学家围坐在一张桌子旁，桌子上摆着五个盘子和五根筷子。哲学家可以做两件事，要么思考，要么吃饭。 哲学家思考的时候，不需要筷子;反之，思考的时候，他却会感到饥饿。吃饭时，他需要两只筷子，筷子放在盘子的两边。 一旦他吃完了，哲学家就松开筷子，开始思考，然后又会饿，等等。哲学家使用一个具有两个属性的类进行建模。贡品状态表示哲学家的状态--可以是思考、饥饿或进食--而属性sticks表示他持有筷子的数量此外，还定义了一个消息（N），表明N是自由的。哲学家和筷子都是用从1到5的数字来命名的，这样一来，除了哲学家i之外的筷子就是i和i+1，或者如果i是5，则是i和1注意子排序声明Nat Oid使自然数成为有效的对象标识符。系统行为由四个规则定义，每个规则代表系统的一个局部转换例如，标记为grab的规则可以在哲学家对象I饿了并且它接收到一条消息时被触发，该消息指示该对象是空闲的，该对象是我可以抓住的筷子之一结果，信息被消耗了，哲学家抓住筷子的数量增加了规则和条件规则的语法分别是rl[l]：t=>tJ和crl [l]：t=>tJifc，其中l是规则标签，tt是J项，c是规则条件。(omod餐饮-PHYSSOPHERS是JF. Durán等人/理论计算机科学电子笔记124（2005）1721保护NAT。subsort Nat< Oid. *自然数有效对象标识符排序状态。操作思考饥饿进食：->状态[ctor]。哲学家阶级|state：Status，sticks：Nat.msg：Nat -> Msg.Vars I JK：Nat.op _can 'use_：Nat Nat -> Bool。等式I可以使用J=（I == J）或（s（I）== J）或（I == 5且J == 1）。rl[饿了]：<第一章哲学家|状态：思考>=>。crl[grab]：<第一章哲学家|状态：饥饿，棍子：K >（J）=> if Ican use J.rl [eat]：<第一章哲学家|状态：饿了，坚持：2>=>=>思考（一）（1）.endom）在Maude中，对象的那些与公理无关的属性不需要被提及。未出现在规则右侧的属性将保持其先前的值不变。3Maude的执行策略Maude中的系统模块和面向对象的模块不需要是Church-Rosser和终止的，因此系统状态可以根据我们应用描述这样一个系统的规则的顺序向不同的方向Maude提供了两种内置策略：rewrite命令遵循自顶向下的惰性规则公平策略，而frewrite命令遵循自底向上的位置公平策略。虽然在许多情况下足够，重写推理过程不能终止或进入许多不希望的方向。由于Maude提供的响应能力，我们可以定义自己的策略，实际上是使用普通模块中的语句定义的Maude为元编程和编写执行策略提供了关键的元级功能。一般来说，策略是在预定义模块META-LEVEL的扩展中定义的，通过使用其中的预定义函数，如MetaReduce，MetaApply，MetaXapply等作为构建块。META-LEVEL还提供了对术语和模块进行排序的功能，因此术语T22F. Durán等人/理论计算机科学电子笔记124（2005）17模M的和分别是类项T和项Msort模块。常数（分别为变量）元表示为包含常量名称的引用标识符（分别为变量）及其类型（分别用点分隔）。 结肠），例如， ’true.Bool’B:Bool然后，以通常的方式构造一个项，通过将运算符符号应用于 逗号分隔的术语列表。例如，术语S| = True of sort下面模块PL-SATISFACTION中的Bool元表示为术语'_|=_['S：State，'True.Formula]排序项。对于我们当前的目的特别感兴趣的是部分函数MetaReduce和MetaXapply。5操作MetaReduce：Module Term ~> Term。opmetaXapply：Module Term Qid ~> Term.MetaReduce采用一个模M和一个项T，并返回T在M中的规范形式的元表示，即使用M中的方程尽可能减少T的结果。metaXapply以模块M、项T和规则标签L作为参数，并返回将M中标签为L的规则应用于项T所产生的项的元表示。为了说明一般的方法，作为我们最终目标的第一步，让我们假设我们对一个策略感兴趣，该策略通过以任何顺序将给定模块中的所有规则应用于给定项来重写给定项。策略应该只是尝试在当前术语中逐个应用规则，直到重写。一旦规则可以应用于它，从这样的应用中产生的术语就成为当前术语，我们重新开始。如果没有规则可以应用于术语，则将其作为重写过程的结果返回。这种策略可以具体如下：op rew：Module Term -> Term.op rewAux：Module Term ContStruct -> Term.eq rew（M，T）= rewAux（M，T，N（M））。ceq rewAux（M，T，C）= T如果最终（C）。ceq rewAux（M，T，C）=ifTthen rewAux（M，FiifC/\T '：=metaXapply（M，T，getLabel（C'））.操作rew有两个参数：描述我们希望控制其执行的系统的模块（的元表示），以及[5]为了便于表达，我们简化了这些函数的形式，因为这里我们不需要它们的全部功能。见[3]，见[4]，见[5]。F. Durán等人/理论计算机科学电子笔记124（2005）1723表示系统初始状态的术语。rewAux有三个参数：描述系统的模块，被重写的术语，以及带有模块中规则标签的延续结构，它允许我们以某种顺序对标签进行扩展。因此，该战略提出了一个无法进一步改写的术语。在定义rew和rewAux的等式中，我们假设一个函数rew，它接受一个模块并为其返回一个延续结构，这个结构包含模块的规则标签并控制最后一个我们还假设在continuation结构的排序ContStruct上有以下函数：final，返回一个布尔值，指示结构中是否有更多的标签; reset，返回结构，即返回下一个标签设置为第一个的结构; next，返回下一个标签设置为下一个的结构;getLabel，返回序列中的下一个标签。请注意，我们没有假设一个具体的结构;根据所使用的特定结构和这些操作的定义，标签被考虑的顺序可能是不同的，这为我们的策略提供了额外的适应性。注意metaXapply函数的使用重写步骤T−L→TJ是只有当标记为L的规则适用于项T时，才能完成，因为TJ是由meta Xapply（M，T ， L ） 返 回 的 项 。 成 员 关 系 断 言 请 注 意 ， 如 果 无 法 应 用 该 规 则 ， 则metaXapply将返回一个超级排序为Term的错误术语。4使用不变量指导系统执行基本上，不变量是一个规范或程序总是要求为真的属性。我们建议使用不变量作为我们的规范的一部分，而不是使用外部监视器来验证给定的系统规范是否与不变量一致，使其成为内部规范。我们建议利用定义执行策略的可能性来驱动系统执行，以保证每个获得的状态都符合不变量，从而避免执行将系统引导到不满足不变量的状态的操作。如果我们想定义一个保证不变量的策略，我们可以使用第3节中策略的变体：我们只需要检查不变量是否被初始状态和重写步骤中新状态的每个候选状态所满足。为了实现这一新的策略，我们假设一个满意的布尔预测_|=_使得，给定系统S的状态和不变式I，则S| =I根据状态S是否满足而计算为true或false24F. Durán等人/理论计算机科学电子笔记124（2005）17不变量I新的策略需要两个额外的参数，即不变谓词（的元表示），以及在用于表达这种不变式的逻辑中定义满足关系的模块（的op rewInv：Module Module Term Term ~> Term.oprewInvAux：Module Module Term Term ContStruct-> Term.ceq rewInv（M，= rewInvAux（M，如果MetaReduce（M'，'_|=_[T，I]）='true.Bool.ceq rewInvAux（M，= T如果最终（C）。ceq rewInvAux（M，=ifT然后是MetaReduce（M'，'_|=_[T'，I]）=='true.BoolthenrewInvAux（M，M'，T'，I，reset（C））else rewInvAux（M，ifL：= getLabel（next（C））/\T '：=metaXapply（M，T，L）.现在，如果初始状态满足不变式，则调用辅助函数。请注意，操作符rewInv是使用~>声明的，这意味着如果不减少，它将返回sort[Term]的错误项，它表示排序Term的类型及其连接组件中的所有排序。[6]一个kind在语义上被解释为一个集合，它包含了确定它的排序中的所有格式良好的表达式，以及错误表达式。此外，该策略只有在项可以使用特定规则重写并且它产生满足不变量的下一个状态时才进行重写步骤。不变量I的检验是通过对T j上的expressi进行求值来实现的|=I，对于gi ven候选跃迁T-L→TJ。但是请注意，重写过程发生在元级别，我们使用MetaReduce来评估属性的满意度还要注意，描述系统的规则可以独立于应用于它们的不变量来编写，并且指定系统的模块独立于表达不变量的逻辑，从而在系统定义和系统不变量之间提供了正确的独立性和模块性。实际上，策略是由要执行的系统（M）、要保留的不变量（I）和定义满足关系的模块（MJ）参数化的。这允许使用不同的逻辑来表达不变量，而无需执行策略或系统。6注意，第3节中的操作符rew在排序时使用->声明，因为它总是返回一个项。在rew的情况下，原始项是有效状态，因此is总是可以作为结果给出。F. Durán等人/理论计算机科学电子笔记124（2005）17255定义驱动系统执行的逻辑：命题演算表达不变量的逻辑与要执行的系统无关。这将允许我们根据需要使用一种或另一种逻辑来表达我们的不变量。我们用命题逻辑来说明我们的方法。如果我们想用一个特定的逻辑来表示不变谓词，我们需要定义这样一个逻辑的语法和它的满足关系。一组原子命题，对应于排序命题，下面的模块PROPOSITIONAL-CALCULUS定义命题演算的公式。(fmod命题演算是排序命题公式。subsort命题<公式。ops True False：->公式。op _and_：公式公式->公式[asshopprec 55]。op _or_：公式公式->公式[asshopprec 59]。op _xor_：公式公式->公式[assumptionprec 57]。opnot_：公式->公式[prec 53]。op _implies_：公式公式->公式[prec 61 gather（e E）]。op_iff_：公式公式->公式[ascurprec 63]。变量A B C：公式。Eq True和A = A。q为False，A = False。等式A和A = A。eq假异或A = A。eqA xor A =假。等式A和（B xor C）= A和B xor A和C。eq not A = A xor True。等式A或B = A和B xor A xor B。等式A意味着B = not（A xor A andB）。等式A当且仅当B = A xor Bxor True。endfm）PROPOSITIONAL-CALCULUS模块介绍了良构命题公式的排序公式，指定了True和False两个公式，具有明显的意义。对应于原子命题集合的排序命题被声明为公式的子排序. 命题此时还没有被具体化;我们将在下面看到，对于一个给定的系统模块，这样的原子命题是如何被定义的。然后，声明常用运算符。这些声明非常接近Maude和OBJ3 [5]中布尔值的定义，它们基于Hsiang [7]提出这个过程减少有效的命题公式为常数真，和所有其他的一些规范形式，其中包括一个排他性或合取。下面的模块PL-满意度定义了满意度关系，26F. Durán等人/理论计算机科学电子笔记124（2005）17命题公式(fmod PL-满意度是保护PROPOSITIONAL-CALCULUS排序状态公式。操作_|=_：状态公式->布尔值。var S：State。变量F F '：公式。方 程 式S| =（ F 和 F ' ） = （S| =F ） 和 （ S| = F'）。方程式S| =（F xor F '）=（S| =F）xor（S|= F '）。eqS|= notF=notS|=F.方程式S| =真=真。方程式S| =假=假。endfm）如上所述，满意度关系--|=_是一个布尔谓词，这样，给定一个状态（将为每个特定问题定义排序状态）和一个公式，根据给定的状态是否满足这样的公式，计算为true或false。 注意到--|=_将一个命题公式作为第二个参数，并返回一个布尔值，即Maude中的预定义排序。如果我们想使用命题演算来定义给定问题的不变谓词，我们需要定义这样一个问题感兴趣的原子命题。例如，我们可以定义一个不变谓词来指导我们的哲学家示例的执行，以避免死锁情况。如果我们达到每个哲学家都有一个哲学家的状态，系统就会陷入僵局。我们定义了什么是状态--在这个例子中，是一个配置--以及命题fork（P，N），如果哲学家P有N根筷子，这个命题成立，在下面的模块中：(omod DINING-PHYSSOPHERS-PL-PREDS是保护食客。包括PL满意度。子排序配置<状态。op forks：Oid Nat -> Proposition.varsI N M：Nat.var C：配置。等式 C |= forks（I，M）= N == M。endom）一旦我们定义了原子命题forks，它就可以用来定义用于指导执行的预定不变量。因此，避免死锁状态的不变量可以表示如下：deadlock-free = not（forks（1，1）和叉子（2，1）和叉子（3，1）和叉子（4，1）和叉子（5，1））让我们把t和M表示为项t和模的元表示F. Durán等人/理论计算机科学电子笔记124（2005）1727M. 我们可以重写DINING-PHYSSOPHERS系统的初始状态，由一个常数初始状态给出，使用策略rewInv，具有前一个不变量，如下所示。redrewInv（DINING-PHYSSOPHERS，DINING-PHYSSOPHERS-PL-PREDS，初始状态、无死锁）。使用这个命令，我们通过允许模块中规则的非确定性应用来执行系统，但要保证不变量被跟踪中的所有状态所满足6总结发言我们提出了通用的不变量驱动策略，通过保证给定的不变量得到满足来控制系统的执行。我们的策略是通用的，在这个意义上，他们是参数化的系统，其执行，他们控制，由逻辑表达的不变量，并由不变量本身。这种参数化以及方法的模块化水平可以提高质量因素，如可扩展性、可理解性、可用性或可维护性。我们已经用命题演算中的不变量说明了它的用途。然而，Maude作为逻辑和语义框架的良好特性[8]，其中可以表达和执行许多不同的逻辑和形式主义，允许我们使用其他逻辑作为我们策略的参数第4节中给出的策略rewInv，虽然对于像命题逻辑这样的逻辑是有效的我们已经尝试了未来时间线性时态逻辑（简称LTL）。在这种情况下，LTL公式的满足不能考虑特定的状态，但我们需要看看完整的痕迹。例如，考虑不变约束[]P（P总是成立）。这个不变量需要任何未来的状态来保持属性P，显然这不能仅仅考虑实际状态来保证。我们的方法是基于Havelund和Roransu在[6]中提出的监视Java程序的一种新方法，即当系统状态变化时，不变量约束的渐进变换，可能在系统状态变化时获得新的不变量.引用[1] P.Borova n sky' ，H. Cir st ea，H.杜博 伊斯，C。 K irchn er，H.Kir chn er，P. - E.Moreau，C. R i n g eisseen和M.维特克ELAN v 3.3用户手册，第三版。技术报告，INRIALorraine LORIA，法国南希，12月15日。1998年28F. Durán等人/理论计算机科学电子笔记124（2005）17[2] M. Clavel，F. 杜兰，S。 Eker，P. Lincoln，N. 我的天啊-我的天啊。梅塞格尤尔和J。你好。Maude：重写逻辑的规范和编程。理论计算机科学，（285）：187[3] M. Clavel，F. 杜兰，S。 Eker，P. 林科林，N。 妈的-哦，J。 我是你，还有C。 Talcott. 马友德2.0手册. 可在www.example.com上http://maude.cs.uiuc.edu，2003年6月[4] M. Clavel，F. 杜兰，S。 Eker，J. Meseguer和M. -O. STEHR。 Madesaformalmeta-tool. 在J.Wing、J. Woodcock和J. Davies编辑的FM'99 - Formal Methods（第II卷），计算机科学讲义第1709卷，第1684-1704页中。Springer，1999年。[5] J. Goguen，T. Winkler，J. Meseguer，K. Futatsugi和J. - P. Jouannaud。 介绍OBJ。在Goguen和G. Malcolm，编辑，Software Engineering with OBJ：Algebrafish Specification inAction。Kluwer，2000年。[6] K. HavelundandG. Rosu. 基于重写的查询需要用于运行时间验证。自动化软件工程杂志。[7] 香子兰使用项重写系统的反驳定理证明。Arti ficial Intelligence，（25）：255[8] N. 我的天啊，我的天啊。Meseguer. 重新写入逻辑是一个逻辑调用和语义帧w或k。第9卷，第1-87页Kluwer Academic Publishers，第二版，2002年。[9] T. McComb和G.史密斯使用Z动画器制作Object-Z规格的动画。第一届软件工程和形式化方法国际会议（SEFM[10] J. Meseguer。条件重写逻辑是并发的统一模型。理论计算机科学，96：73[11] J. Meseguer。隶属代数作为一个逻辑框架的方程规格。在F. Parisi-Presicce，编辑，《代数发展技术的最新趋势》，第1376卷，计算机科学讲义，第18-61页。Springer，1998年。[12] M. Utting.贾扎的动画师该系统及其文档可在http://www.cs.waikato.ac.nz/~marku/jaza/网站。[13] J. Warmer和A.克莱珀对象约束语言：为MDA准备好模型。Addison-Wesley，2003年。