The Maude System
The Maude System
复制标题
DOI：
10.1007/3-540-48685-2_18
复制
发表时间：
1999-07
期刊：
影响因子：
--
通讯作者：
M. Clavel;F. Durán;S. Eker;P. Lincoln;N. Martí-Oliet;J. Meseguer;J. F. Quesada
中科院分区：
文献类型：
--
作者：
M. Clavel;F. Durán;S. Eker;P. Lincoln;N. Martí-Oliet;J. Meseguer;J. F. Quesada
Maude是一种高性能的语言和系统，支持等式和重写逻辑计算，适用于广泛的应用，包括定理证明工具的开发，语言原型，并发和分布式系统的可执行规范和分析，以及逻辑框架应用程序，其中其他逻辑表示，翻译和执行。Maude的功能模块是隶属方程逻辑[8，1]中的理论，这是一种Horn逻辑，其原子语句要么是等式t= t，要么是形式为t：s的隶属断言，说明项t具有某种排序s。这样的逻辑扩展了OBJ 3的[4]顺序排序的等式逻辑，并支持运算符的排序、子排序、子排序多态重载，以及用等式定义的域定义部分函数。Maude的功能模块被假定为Church-Rosser;它们由Maude引擎根据[1]中开发的重写技术和操作语义来执行。隶属方程逻辑是重写逻辑的一个子逻辑[6]。重写理论是一对（T，R），其中T是隶属关系方程理论，R是涉及T的签名中的项的标记和可能的条件重写规则的集合。Maude的系统模块就是这种意义上的重写理论。R中的重写规则r：t−→ t不是等式。在计算上，它们被解释为可能并发系统中的局部转换规则。在逻辑上，它们被解释为逻辑系统中的推理规则。这使得重写逻辑既是一个通用的语义框架来指定并发系统和语言[7]，也是一个通用的逻辑框架来表示和执行不同的逻辑[5]。（T，R）中的重写以T中的方程公理为模发生。Maude支持对结合性、交换性、同一性和幂等性公理的不同组合进行模重写。R中的规则不需要是Church-Rosser，也不需要是终止的。许多不同的重写路径是可能的，因此，选择适当的策略是执行重写理论的关键。在Maude，这种策略不是语言的逻辑外部分。
Maude is a high-performance language and system supporting both equational and rewriting logic computation for a wide range of applications, including development of theorem proving tools, language prototyping, executable specification and analysis of concurrent and distributed systems, and logical framework applications in which other logics are represented, translated, and executed. Maude’s functional modules are theories in membership equational logic [8, 1], a Horn logic whose atomic sentences are either equalities t= t or membership assertions of the form t: s, stating that a term t has a certain sort s. Such a logic extends OBJ3’s [4] order-sorted equational logic and supports sorts, subsorts, subsort polymorphic overloading of operators, and definition of partial functions with equationally defined domains. Maude’s functional modules are assumed to be Church-Rosser; they are executed by the Maude engine according to the rewriting techniques and operational semantics developed in [1]. Membership equational logic is a sublogic of rewriting logic [6]. A rewrite theory is a pair (T, R) with T a membership equational theory, and R a collection of labeled and possibly conditional rewrite rules involving terms in the signature of T. Maude’s system modules are rewrite theories in exactly this sense. The rewrite rules r: t−→ t in R are not equations. Computationally, they are interpreted as local transition rules in a possibly concurrent system. Logically, they are interpreted as inference rules in a logical system. This makes rewriting logic both a general semantic framework to specify concurrent systems and languages [7], and a general logical framework to represent and execute different logics [5]. Rewriting in (T, R) happens modulo the equational axioms in T. Maude supports rewriting modulo different combinations of associativity, commutativity, identity, and idempotency axioms. The rules in R need not be Church-Rosser and need not be terminating. Many different rewriting paths are then possible; therefore, the choice of appropriate strategies is crucial for executing rewrite theories. In Maude, such strategies are not an extra-logical part of the language.