Maude工具详解与Linux环境使用指南

需积分: 50 198 浏览量更新于2024-07-20 收藏 2.63MB PDF 举报

"Maude工具使用手册 - Linux环境下学习Maude的指南" Maude是一种强大的反射性编程和形式化验证环境，主要用于实现、模拟和验证复杂计算系统的高级数学模型。这个手册是Maude Version 2.6的使用指南，由Manuel Clavel, Francisco Durán等多位专家编写，旨在帮助用户在Linux系统中有效地学习和应用Maude系统。 1. **简洁性、表达力和性能** - **简洁性**: Maude设计时考虑了易用性和可理解性，使得代码更易于阅读和编写。 - **表达力**: 它支持高度抽象的表示法，能够描述各种复杂的计算和变换，包括重写逻辑和类型理论。 - **性能**: Maude具有高效执行模型的能力，可以处理大规模的计算任务。 2. **逻辑基础** Maude基于一种称为“ Rewriting Logic”的逻辑基础，这是一种非常灵活的形式化框架，允许表达广泛的计算和转换规则。 3. **编程、规范与验证** - **编程**: Maude可以用来编写程序，不仅支持传统的命令式和函数式编程，还支持并发和反射机制。 - **规范**: 用户可以用Maude来指定系统的数学模型，用于清晰地表述系统的行为。 - **验证**: 通过Maude的模拟和推理能力，可以对系统进行形式化验证，确保其行为符合预期。 4. **高性能逻辑框架** Maude构建在一个高性能的逻辑框架之上，能够快速地执行重写操作，这对于大规模系统的建模和分析至关重要。 5. **核心Maude与完整Maude** - **核心Maude**: 是Maude的基础部分，包含基本的重写逻辑和元语言特性。 - **完整Maude**: 增加了更多的模块系统、类型系统和其他高级特性，提供了更广泛的功能。 6. **手册结构** 手册的结构包括多个章节，逐步引导用户从基础概念到高级特性的理解和使用，方便用户根据需要查阅。 7. **Maude书籍** 除了手册外，可能还有一本关于Maude的书籍，提供更深入的理论背景和实例解析。手册接下来的内容很可能是详细介绍Maude的基本语法、如何使用Maude进行编程、如何定义和使用模块、如何进行系统验证等实际操作教程。Maude的用户可以通过这个手册深入理解Maude系统，并掌握其在Linux环境下的实际应用。由于Maude的开源性质，用户还可以自由地分发和修改软件，以适应自己的需求。然而，Maude不提供任何明示或暗示的保修，用户需自行承担使用风险。

4 CHAPTER 1. INTRODUCTION

< ’A-001 : Account | bal : 175 >

< ’A-002 : Account | bal : 200 >

Note that the rewriting performed is multiset rewriting, so that, regardless of where the

account objects and the messages are placed in the soup, they can always come together and

rewrite if a rule applies. In Maude this is speciﬁed in the equational part of the program (system

module) by declaring that the (empty syntax) multiset union operator satisﬁes the associativity

and commutativity equations:

X (Y Z) = (X Y) Z

X Y = Y X

This is not done by giving the above equations explicitly. It is instead done by declaring

the multiset union operator with the assoc and comm equational attributes (see Section 4.4.1

and Section 1.1.2 below), as follows, where Configuration denotes the multisets or soups of

objects and messages.

op __ : Configuration Configuration -> Configuration [assoc comm] .

Maude then uses this information to generate a multiset matching algorithm, in which the

multiset union operator is matched modulo associativity and commutativity.

Again, a program involving such rewrite rules is intuitively very simple, and has a very simple

rewriting semantics. Of course, the systems speciﬁed by such rules can be highly concurrent

and nondeterministic; that is, unlike for equations, there is no assumption that all rewrite

sequences will lead to the same outcome. For example, depending on the order in which debit

or credit messages are consumed, a bank account can end up in quite diﬀerent states, because

the rule for debiting can only be applied if the account balance is big enough. Furthermore,

for some systems there may not be any ﬁnal states: their whole point may be to continuously

engage in interactions with their environment as reactive systems.

1.1.2 Expressiveness

The above examples illustrate a general fact, namely, that Maude can express with equal ease

and naturalness deterministic computations, which lead to a unique ﬁnal result, and concurrent,

nondeterministic computations. The ﬁrst kind is typically programmed with equations in

functional modules, and the second with rules (and perhaps with some equations for the “data”

part) in system modules.

In fact, functional modules deﬁne a functional sublanguage

of Maude. In a functional

language true to its name, functions have unique values as their results, and it is neither easy

nor natural to deal with highly concurrent and nondeterministic systems while keeping the

language’s functional semantics. It is well known that such systems pose a serious expressiveness

challenge for functional languages. In Maude this challenge is met by system modules, which

extend the purely functional semantics of equations to the concurrent rewriting semantics of

rules.

Although certainly declarative in the sense of having a clear logical semantics, system

modules are of course not functional: that is their entire raison d’ˆetre.

Besides this generality in expressing both deterministic and nondeterministic computations,

further expressiveness is gained by the following features:

This sublanguage is essentially an extension of the OBJ3 equational language [67], which has greatly inﬂu-

enced the design of Maude.

As explained in Section 1.2, mathematically this is achieved by a logic inclusion, in which the functional

world of equational theories is conservatively embedded in the nonfunctional, concurrent world of rewrite theo-

ries.

1.1. SIMPLICITY, EXPRESSIVENESS, AND PERFORMANCE 5

• equational pattern matching,

• user-deﬁnable syntax and data,

• types, subtypes, and partiality,

• generic types and modules,

• support for objects, and

• reﬂection.

We brieﬂy discuss each of these features in what follows.

Equational pattern matching

Rewriting with both equations and rules takes place by matching a lefthand side term against

the subject term to be rewritten. The most common form of matching is syntactic matching, in

which the lefthand side term is matched as a tree on the (tree representation of the) subject term

(see Section 4.7). For example, the matching of the lefthand sides for the equations deﬁning

the length and _in_ functions above is performed by syntactic matching. But we have already

encountered another, more expressive, form of matching, namely, equational matching in the

bank accounts example: the lefthand side

< I : Account | bal : M > credit(I, N)

has the (empty syntax) multiset union operator __ as its top operator, but, thanks to its assoc

and comm equational attributes, it is matched not as a tree, but as a multiset. Therefore,

the match will succeed provided that the subject multiset contains instances of the terms

< I : Account | bal : M > and credit(I, N) in which the variable I is instantiated the

same way in both terms, regardless of where those instances appear in the multiset, that is,

modulo associativity and commutativity.

In general, a binary operator declared in a Maude module can be deﬁned with any

combina-

tion of equational attributes of: associativity, commutativity, left-, right-, or two-sided identity,

and idempotency. Maude then generates an equational matching algorithm for the equational

attributes of the diﬀerent operators in the module, so that each operator is matched modulo its

equational attributes. This manual will illustrate with various examples the expressive power

aﬀorded by this form of equational matching (see Section 4.8).

User-deﬁnable syntax and data

In Maude the user can specify each operator with its own syntax, which can be preﬁx, postﬁx,

inﬁx, or any “mixﬁx” combination. This is done by indicating with underscores the places where

the arguments appear in the mixﬁx syntax. For example, the inﬁx list cons operator above is

speciﬁed by _._, the (empty syntax) multiset union operator by __, and the if-then-else operator

by if_then_else_fi. In practice, this improves readability (and therefore understandability)

of programs and data. In particular, for metalanguage uses, in which another language or logic

is represented in Maude, this can make a big diﬀerence for understanding large examples, since

the Maude representation can keep essentially the original syntax. The combination of user-

deﬁnable syntax with equations and equational attributes for matching leads to a very expressive

capability for specifying any user-deﬁnable data. It is well known that any computable data

type can be equationally speciﬁed [8]. Maude gives users full support for this equational style

of deﬁning data which is not restricted to syntactic terms (trees) but can also include lists

Except for any combination including both associativity and idempotency, which is not currently supported.

6 CHAPTER 1. INTRODUCTION

(modulo associativity), multisets (modulo associativity and commutativity), sets (adding an

idempotency equation), and other combinations of equational attributes that can then be used

in matching. This great expressiveness for deﬁning data is further enhanced by Maude’s rich

type structure, as explained below.

Types, subtypes, and partiality

Maude has two varieties of types: sorts, which correspond to well-deﬁned data, and kinds,

which may contain error elements. Sorts can be structured in subsort hierarchies, with the

subsort relation understood semantically as subset inclusion. For example, for numbers we can

have subsort inclusions

Nat < Int < Rat

indicating that the natural numbers are contained in the integers, and these in turn are con-

tained in the rational numbers. All these sorts determine a kind (say the “number kind”) which

is interpreted semantically as the set containing all the well-formed numerical expressions for

the above number systems as well as error expressions such as, for example, 4 + 7/0. This

allows support for partial functions in a total setting, in the sense that a function whose appli-

cation to some arguments has a kind but not a sort should be considered undeﬁned for those

arguments (but notice that functions can also map undeﬁned to deﬁned results, for example

in the context of error recovery). Furthermore, operators can be subsort-overloaded, providing

a useful form of subtype polymorphism. For example, the addition operation _+_ is subsort

overloaded and has typings for each of the above number sorts. A further feature, greatly

extending the expressive power for specifying partial functions, is the possibility of deﬁning

sorts by means of equational conditions. For example, a sequential composition operation _;_

concatenating two paths in a graph is deﬁned if and only if the target of the ﬁrst path coincides

with the source of the second path. In Maude this can be easily expressed with the “conditional

membership” (see Section 4.3):

vars P Q : Path .

cmb (P ; Q) : Path if target(P) = source(Q) .

Generic types and modules

Maude supports a powerful form of generic programming that substantially extends the param-

eterized programming capabilities of OBJ3 [67]. The analogous terminology to express these

capabilities in higher-order type theory would be parametric polymorphism and dependent types.

But in Maude the parameters are not just types, but theories, including operators and equations

that impose semantic restrictions on the parameterized module instantiations. Thus, whereas a

parametric LIST module can be understood just at the level of the parametric type (sort) of list

elements, a parameterized SORTING module has the theory TOSET of totally ordered sets as its

parameter, including the axioms for the order predicate, that must be satisﬁed in each correct

instance for the sorting function to work properly. Types analogous to dependent types are

also supported by making the parameter instantiations depend on speciﬁc parametric constants

in the parameter theory, and by giving membership axioms depending on such constants. For

example, natural numbers modulo n (see Section 17.7), and arrays of length n, can be easily

deﬁned this way. The fact that entire modules, and not just types, can be parametric provides

even more powerful constructs. For example, TUPLE[n] (see Section 15.3.1) is a “dependent

parameterized module” that assigns to each natural number n the parameterized module of

n-tuples (together with the tupling and projection operations) with n parameter sorts.

1.1. SIMPLICITY, EXPRESSIVENESS, AND PERFORMANCE 7

Support for objects

The bank accounts example illustrates a general point, namely, that in Maude it is very easy to

support objects and distributed object interactions in a completely declarative style with rewrite

rules. Although such object systems are just a particular style of system modules in which object

interactions (through messages or directly between objects) are expressed by rewriting, Maude

provides special support for object-based programming and for fair execution of object-based

applications (see Chapter 8). Furthermore, the Full Maude extension provides special syntax

in object-oriented modules (see Chapter 17). Such modules directly support object-oriented

concepts like objects, messages, classes, and multiple class inheritance. Moreover, the support

for communication with external objects (see Section 8.4) allows Maude objects to interact

by message passing with internet sockets and, through them, with all kinds of other external

objects, such as ﬁles, databases, graphical user interfaces, sensors, robots, and so on. All this

is achieved without compromising Maude’s declarative nature: interaction with normal Maude

objects and with external objects can both be programmed with rewrite rules. Using internet

sockets as external objects, it is also easy to develop distributed implementations in Maude,

where a “soup” of objects and messages is not realized just as a multiset data structure in a

single sequential machine, but as a “distributed soup,” with objects and messages in diﬀerent

machines or in transit.

Reﬂection

This is a very important feature of Maude. Intuitively, it means that Maude programs can

be metarepresented as data, which can then be manipulated and transformed by appropriate

functions. It also means that there is a systematic causal connection between Maude mod-

ules themselves and their metarepresentations, in the sense that we can either ﬁrst perform

a computation in a module and then metarepresent its result, or, equivalently, we can ﬁrst

metarepresent the module and its initial state and then perform the entire computation at the

metalevel. Finally, the metarepresentation process can itself be iterated giving rise to a very

useful reﬂective tower. Thanks to Maude’s logical semantics (more on this in Section 1.2), all

this is not just some kind of “gloriﬁed hacking,” but a precise form of logical reﬂection with a

well-deﬁned semantics (see Chapter 11 and [25, 26]). There are many important applications

of reﬂection. Let us mention just three:

• Internal strategies. Since the rewrite rules of a system module can be highly nondeter-

ministic, there may be many possible ways in which they can be applied, leading to quite

diﬀerent outcomes. In a distributed object system this may be just part of life: provided

some fairness assumptions are respected, any concurrent execution may be acceptable.

But what should be done in a sequential execution? Maude does indeed support two

diﬀerent fair execution strategies in a built-in way through its rewrite and frewrite

commands (see Section 5.4). But what if we want to use a diﬀerent strategy for a given

application? The answer is that Maude modules can be executed at the metalevel with

user-deﬁnable internal strategies

(see Section 11.6). Such internal strategies can be de-

ﬁned by rewrite rules in a metalevel module that guides the possibly nondeterministic

application of the rules in the given “object level” module. This process can be iterated

in the reﬂective tower. That is, we can deﬁne meta-strategies, meta-meta-strategies, and

so on.

• Module algebra. The entire module algebra in which parameterized modules can be com-

posed and instantiated becomes expressible within the logic, and extensible by new mod-

ule operations that transform existing modules metarepresented as data. This is of more

That is, internal to Maude’s logic, in the sense of being deﬁnable by logical axioms.

8 CHAPTER 1. INTRODUCTION

than theoretical interest: Maude’s module algebra is realized exactly in this way by Full

Maude, a Maude program deﬁning all the module operations and easily extensible with

new ones (see Part II of this manual).

• Formal tools. The veriﬁcation tools in Maude’s formal environment must take Maude

modules as arguments and perform diﬀerent formal analyses and transformations on such

modules. This is again done by reﬂection in tools such as Maude’s inductive theorem

prover, the Church-Rosser checker, the Maude termination tool, the Real-Time Maude

tool, and so on.

1.1.3 Performance

Achieving expressiveness in all the ways described above without sacriﬁcing performance is

a nontrivial matter. Successive Maude implementations have been advancing this goal while

expanding the set of language features. More work remains ahead, but it seems fair to say that

Maude, although still an interpreter, is a high-performance system that can be used for many

non-toy applications with competitive performance and with many advantages over conventional

code. Without in any way trying to extrapolate a speciﬁc experience into a general conclusion,

a concrete example from the Maude user’s trenches may illustrate the point. A formal tool

component to check whether a trace of events satisﬁes a given linear temporal logic (LTL)

formula was written in Maude at NASA Ames by Grigore Ro¸su in about one page of Maude

code. The component had a trivial correctness proof—the Maude module was based on the

equational deﬁnition of the LTL semantics for the diﬀerent connectives. This replaced a similar

component having about 5,000 lines of Java code that had taken over a month to develop by an

experienced colleague. The Java tool used a translation of LTL formulas into B¨uchi automata

(the usual method to eﬃciently model check an LTL formula) and run about three times more

slowly than the Maude code. It would have been very diﬃcult to prove the correctness of the

Java tool and, having a better and clearly correct alternative in the Maude implementation,

this was never done.

Generally and roughly speaking, the current Maude implementation can execute syntac-

tic rewriting with typical speeds from half a million to several million rewrites per second,

depending on the particular application and the given machine. Similarly, associative and

associative-commutative equational rewriting with term patterns used in practice

can be per-

formed at the typical rate of one hundred thousand to several hundred thousand rewrites per

second.

These ﬁgures must be qualiﬁed by the observation that, until recently, the cost of an associa-

tive or associative-commutative rewriting step depended polynomially on the size of the subject

term, even with the most eﬃcient algorithms. In practice this meant that this kind of rewriting

was not practical for large applications, in which the lists or multisets to be rewritten could have

millions of elements. This situation has been drastically altered by a recent result of Steven

Eker [51] providing new algorithms for associative and associative-commutative rewriting that,

for patterns typically encountered in practice, can perform one step of associative rewriting

in constant time, and one associative-commutative rewriting step in time proportional to the

logarithm of the subject term’s size. Maude supports equational rewriting with these new

algorithms.

In its fullest generality, it is well known that associative-commutative rewriting is an NP-complete problem.

In programming practice, however, the patterns used as lefthand sides allow much more eﬃcient matching,

so that the theoretical limits only apply to “pathological” patterns not encountered in typical programming

practice.

剩余490页未读，继续阅读

村里可爱程序猿

粉丝: 0
资源: 1

Maude工具详解与Linux环境使用指南

Eclipse中Maude插件使用指南：集成IDE环境的强大工具

Maude 2.7官方手册：逻辑框架与性能优化

使用Maude工具基于重写逻辑建模和分析哺乳动物信号通路

eclipse下maude插件用户手册

Maude-manual

Maude-Syntax:Maude 的语法高亮

实时Maude 2.1：形式化分析工具的进展与应用

Maude与IOP：实现形式工具间互操作的平台

HICmd:HI-Maude 多功能分析工具的新界面与功能

实时Maude：面向对象分析与高性能工具的突破

最新资源