nach oben

2007 | Buch

All About Maude - A High-Performance Logical Framework

How to Specify, Program and Verify Systems in Rewriting Logic

verfasst von: Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This book gives a comprehensive account of Maude, a language and system based on rewriting logic. Many examples are used throughout the book to illustrate the main ideas and features of Maude, and its many possible uses. Maude modules are rewrite theories. Computation with such modules is - cient deduction by rewriting. Because of its logical basis and its initial model semantics,aMaudemodulede?nesaprecisemathematicalmodel.Thismeans that Maude and its formal tool environment can be used in three, mutually reinforcing ways: • as a declarative programming language; • as an executable formal speci?cation language; and • as a formal veri?cation system. Maude’s rewriting logic is simple, yet very expressive. This gives Maude good representational capabilities as a semantic framework to formally represent a wide range of systems, including models of concurrency, distributed al- rithms, network protocols, semantics of programming languages, and models of cell biology. Rewriting logic is also an expressive universal logic,making Maude a ?exible logical framework in which many di?erent logics and - ference systems can be represented and mechanized. This makes Maude a useful metatool to build many other tools, including those in its own formal tool environment. Thanks to the logic’s simplicity and the use of advanced semi-compilation techniques, Maude has a high-performance implementation, making it competitive with other declarative programming languages.

Inhaltsverzeichnis

Frontmatter

Introduction

Abstract

This introduction tries to give the big picture on the goals, design philosophy, logical foundations, applications, and overall structure of Maude. It is written in an impressionistic, conversational style, and should be read in that spirit. The fact that occasionally some particular technical concept mentioned in passing (for example, “the Church-Rosser property”) may be unfamiliar should not be seen as an obstacle. It should be taken in a relaxed, sporting spirit: those things will become clearer in the body of the book; here it is just a matter of gaining a first overall impression.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

Part I: Core Maude

Frontmatter

Using Maude

Abstract

The Maude system is available, free of charge, under the terms of the GNU General Public License as published by the Free Software Foundation, at the Maude home page (a snapshot is shown in Figure 2.1) http://maude.cs.uiuc.edu .

There you can also find documentation about Maude, including a Maude primer, some papers on Maude and rewriting logic, and several Maude applications, including a set of proving tools for Maude specifications and Maude case studies.

Maude binaries are provided for selected architectures and operating systems, including Linux and MacOS X. Detailed information on this can be found in the Maude web site, where installation instructions are also available.

The companion cd-rom contains the latest version of Maude available at the time of writing, together with the complete source code of all the examples in this book.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

Syntax and Basic Parsing

Abstract

This chapter introduces the basic syntactic ingredients of all Maude specifications: identifiers, module names, sort names, and operator declarations. Other syntactic parts of Maude specifications, like equations and rules, will appear in the following chapters.

Some syntax is presented in an informal way by means of general schemes; a formal BNF grammar of the language can be found in Chapter 24.

The chapter finishes explaining some features that can be used to reduce parsing ambiguities in the user-definable syntax, including mixfix operator declarations, supported by Maude.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

Functional Modules

Abstract

Functional modules define data types and operations on them by means of equational theories. The data types consist of elements that can be named by ground terms. Two ground terms denote the same element if and only if they belong to the same equivalence class as determined by the equations. That is, the mathematical semantics of a functional module is its initial algebra. Maude’s functional modules are assumed to have the nice property that equations, considered as simplification rules by using them only in the left to right direction, are Church-Rosser and terminating (see Section 4.7). This means that repeated application of the equations as simplification rules eventually reaches a term to which no further equations apply, and the result, called the canonical form, is the same regardless of the order of application of the equations. Thus each equivalence class has a natural representative, its canonical form, that can be computed by equational simplification. As explained in Section 1.2, this ensures that the initial algebra and the canonical term algebra of the functional module are isomorphic, and therefore that the module’s mathematical and operational semantics coincide.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

A Hierarchy of Data Types: From Trees to Sets

Abstract

In Section 4.4.1 we have introduced equational attributes as a means of declaring some equational properties of binary operators that allow Maude to use these properties efficiently in a built-in way in parsing and in matching modulo such equational axioms. We recall that Maude supports the following equational attributes:

assoc (associativity),
comm (commutativity),
id:\(\langle Term\rangle\) (identity, with the corresponding term for the identity element), with variations for left identity and right identity, and
idem (idempotency).

An important restriction to bear in mind is that the assoc and idem attributes cannot be used together in any combination.

In this chapter we will show that equational attributes correspond to structural axioms of well-known data types built with a binary constructor operator. In this way we obtain a hierarchy of data types:

non-empty binary trees, with elements only in their leaves, built with a free binary constructor, that is, a constructor with no equational axioms;
non-empty lists, built with an associative constructor;
lists, built with an associative constructor and an identity;
multisets (or bags), built with an associative and commutative constructor and an identity; and
sets, built with an associative, commutative, and idempotent constructor and an identity.

All these data types are generic, so that they can be constructed on top of any given data type of basic elements; for example, we can have lists of natural numbers, lists of Booleans, lists of sets of integers, etc. This genericity corresponds to making use of parameterized modules in Maude, which will be introduced later in Section 8.3. Therefore, in this chapter we only consider constructions over natural numbers. In Section 9.12 we will describe the predefined parameterized versions of lists and sets provided in the Maude prelude, and in Chapter 10 we will describe many other parameterized data types, like stacks, queues, sorted lists, multisets, and different versions of trees.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

System Modules

Abstract

A Maude system module specifies a rewrite theory. A rewrite theory has sorts, kinds, and operators (perhaps with frozen arguments), and can have three types of statements: equations, memberships, and rules, all of which can be conditional. Therefore, any rewrite theory has an underlying equational theory, containing the equations and memberships, plus the rules. What is the intuitive meaning of such rules? Computationally, they specify local concurrent transitions that can take place in a system if the pattern in the rule’s lefthand side matches a fragment of the system state and the rule’s condition is satisfied. In that case, the transition specified by the rule can take place, and the matched fragment of the state is transformed into the corresponding instance of the righthand side. Logically, that is, when we use rewriting logic as a logical framework to represent other logics as explained in Section 1.4, a rule specifies a logical inference rule, and rewriting steps therefore represent inference steps.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

Playing with Maude

Abstract

Mathematical games and puzzles of all sorts constitute an important subclass of mathematical problems, with a long tradition and an extensive literature [20, 135, 11, 287]. Most of them have in common the fact that they are easy to state and understand, which does not mean that a precise solution is always trivial to find.

In this chapter we make use of Maude system modules to present and illustrate some general techniques that allow solving a diverse enough selection of these problems. We are not concerned with finding neat and concise mathematical solutions, but rather we would like to find out how easy it is to express those problems in the rewriting logic formalism underlying Maude, and how far we can go in their resolution by the use of just brute force and as little ingenuity as possible. In this regard, a clear conclusion is that many of these problems can be represented/specified in Maude in a much simpler way than it would be possible in more conventional languages.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott, Miguel Palomino, Alberto Verdejo

Module Operations

Abstract

Specifications and code should be structured in modules of relatively small size to facilitate understandability of large systems, increase reusability of components, and localize the effects of system changes. In Maude, these goals are achieved by means of a module algebra that supports parameterized programming techniques in the OBJ3 style [146] as well as the definition of module hierarchies, i.e., acyclic graphs of module importations; that is, each functional or system module can import other Maude modules as submodules. Since the submodule relation is transitive, we can in this way develop module hierarchies. Mathematically, we can think of such hierarchies as partial orders of theory inclusions, that is, the theory of the importing module contains the theories of its submodules as subtheories.

As in Clear [33], OBJ [146], and other specification languages in that tradition, the abstract syntax for writing specifications in Maude can be seen as given by module expressions, where the notion of module expression is understood as an expression that defines a new module out of previously de- fined modules by combining and/or modifying them according to a specific set of operations. In fact, structuring is essential in all specification languages, not only to facilitate the construction of specifications from already existing ones—with more or less flexible reusability mechanisms—but also for managing the complexity of understanding and analyzing large specifications. Maude supports module operations for summation, renaming, and instantiation of parameterized modules.

Section 8.1 introduces module importations and the different modes in which such importations can take place. Section 8.2 discusses the summation and renaming module expressions. Section 8.3 introduces parameterized programming, including the use of theories and views, the parameterization of functional and system modules, and the instantiation of parameterized modules. We refer to [98, 110, 111] for a deeper discussion on the semantics of the Maude module operations.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

Predefined Data Modules

Abstract

Maude has a standard library of predefined modules that, by default, are entered into the system at the beginning of each session, so that any of these predefined modules can be imported by any other module defined by the user. Also, by default, the predefined functional module BOOL is automatically imported (in including mode) as a submodule of any user-defined module, unless such importation is explicitly disabled. These modules can be found in the file prelude.maude that is part of the Maude distribution.

We describe below those predefined modules that provide commonly used data types, including Booleans, numbers, strings, and quoted identifiers. The relationships among these modules are shown in the importation graph in Figure 9.1, where all the importations are in protecting mode.

We also describe typical parameterized collections of data types such as lists and sets, and associations such as maps and arrays. The chapter ends introducing the built-in linear Diophantine equation solver, defined in the file linear.maude that is also part of the Maude distribution.

Other predefined modules, also in the prelude.maude file, are discussed later; more specifically, the META-LEVEL module is discussed in Chapter 14, the LOOP-MODE module in Section 17.1, and the CONFIGURATION module in Sections 11.1 and 11.4.

Furthermore, this chapter also describes a predefined module MACHINE-INT for machine integers, which is obtained from the module INT of (arbitrary size) integers, but is distributed in a separate file machine-int.maude.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

Specifying Parameterized Data Structures in Maude

Abstract

This chapter describes the equational specification in Maude of a series of typical data structures, complementing in this way the list and set data structures provided as predefined modules in Maude and described in Section 9.12.

We start with the well-known stacks, queues, lists, and multisets to continue with binary and search trees; not only are the simple versions considered, but also advanced ones such as AVL and 2-3-4 trees. The operator attributes available in Maude allow the specification of data based on constructors that satisfy some equational properties, like concatenation of lists which is associative and has the empty list as identity, as opposed to the free constructors available in other functional programming languages. Moreover, the expressive version of equational logic on which Maude is based, namely membership equational logic, allows the faithful specification of types whose data are defined not only by means of constructors, but also by the satisfaction of additional properties, like sorted lists, search trees, balanced trees, etc. We will see along this chapter how this is accomplished by means of membership assertions that equationally characterize the properties satisfied by the corresponding data.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott, Miguel Palomino, Alberto Verdejo

Object-Based Programming

Abstract

Distributed systems can be naturally modeled in Maude as multisets of entities, loosely coupled by some suitable communication mechanism. An important example is object-based distributed systems in which the entities are objects, each with a unique identity, and the communication mechanism is message passing.

Core Maude supports the modeling of object-based systems by providing a predefined module CONFIGURATION that declares sorts representing the essential concepts of object, message, and configuration, along with a notation for object syntax that serves as a common language for specifying objectbased systems. In addition, there is an object-message fair rewriting strategy that is well suited for executing object system configurations. To specify an object-based system, the user can import CONFIGURATION and then define the particular objects, messages, and rules for interaction that are of interest. In addition to simple asynchronous message passing, Maude also supports complex patterns of synchronous interaction that can be used to model higherlevel communication abstractions. The user is also free to define his/her own notation for configurations and objects, and can still take advantage of the object-message rewriting strategy, simply by making the appropriate declarations. All this is explained in detail below.

Furthermore, Maude also supports external objects, so that objects inside a Maude configuration can interact with different kinds of objects outside it. At present, the external objects directly supported are internet sockets; but through them it is possible to interact with other external objects. In addition, sockets make possible distributed programming with rewrite rules. External objects are discussed in Section 11.4. A substantial case study using sockets to build a mobile language is presented in Chapter 16.

As discussed in Chapter 19, Full Maude provides additional support for object-oriented programming with classes, subclassing, and convenient abbreviations for rule syntax.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

Model Checking Invariants Through Search

Abstract

A rewrite theory, specified in Maude as a system module, provides an executable mathematical model of a concurrent system. We can use the Maude specification to simulate the concurrent system so specified. But we can do more. Under appropriate conditions we can check that our mathematical model satisfies some important properties, or obtain a useful counterexample showing that the property in question is violated. This kind of model-checking analysis can be quite general. Chapter 13 will explain how, under appropriate finite reachability assumptions, we can model check any linear time temporal logic (LTL) property of a system specified in Maude as a system module. This chapter focuses on a simpler, yet very useful, model-checking capability, namely, the model checking of invariants, which can be accomplished just by using the search command.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

LTL Model Checking

Abstract

As pointed out in Section 1.4, given a Maude system module, we can distinguish two levels of specification:

a system specification level, provided by the rewrite theory specified by that system module which defines the behavior of the system, and
a property specification level, given by some property (or properties) φ that we want to state and prove about our module.

This chapter discusses how a specific property specification logic, linear temporal logic (LTL), and a decision procedure for it, model checking, can be used to prove properties when the set of states reachable from an initial state in a system module is finite. It also explains how this is supported in Maude by its MODEL-CHECKER module, and other related modules, including the SAT-SOLVER module that can be used to check both satisfiability of an LTL formula and LTL tautologies. These modules are found in the file model-checker.maude.

Temporal logic allows specification of properties such as safety properties (ensuring that something bad never happens) and liveness properties (ensuring that something good eventually happens). These properties are related to the infinite behavior of a system. There are different temporal logics [54]; we focus on linear temporal logic [194, 54], because of its intuitive appeal, widespread use, and well-developed proof methods and decision procedures.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

Reflection, Metalevel Computation, and Strategies

Abstract

Informally, a reflective logic is a logic in which important aspects of its metatheory can be represented at the object level in a consistent way, so that the object-level representation correctly simulates the relevant metatheoretic aspects. In other words, a reflective logic is a logic which can be faithfully interpreted in itself. Maude’s language design and implementation make systematic use of the fact that rewriting logic is reflective [66, 56, 67, 68]. This makes the metatheory of rewriting logic accessible to the user in a clear and principled way. However, since a naive implementation of reflection can be computationally expensive, a good implementation must provide efficient ways of performing reflective computations. This chapter explains how this is achieved in Maude through its predefined META-LEVEL module, that can be found in the prelude.maude file.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

Metaprogramming Applications

Abstract

A metaprogram is a program that takes programs as inputs and performs some useful computation. It may, for example, transform one program into another. Or it may analyze such a program with respect to some properties, or perform other useful program-dependent computations. This is of course very useful and very powerful. In Maude, metaprogramming has a logical, reflective semantics. It is just a direct consequence of the fact that both membership equational logic and rewriting logic are reflective logics, and of the efficient exploitation of that fact in the META-LEVEL module. That is, we can easily write Maude metaprograms by importing META-LEVEL into a module that defines such metaprograms as functions that have Module as one of their arguments. Since this is one of the most powerful uses of Maude as a programming language, we present in this chapter three metaprogramming examples of moderate size, yet interesting and nontrivial, that can be helpful as an appetizer and guide to more ambitious metaprogramming tasks. Much more ambitious examples, also freely available for inspection, are the Full Maude system itself (see Chapter 18), which is a metaprogram entirely written in Maude, and the various tools in Maude’s formal environment, which are described in Section 21.1.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

Mobile Maude

Abstract

The popularity of the Internet has brought much attention to the world of distributed applications development. Now, more than ever, the network is being viewed as a platform for the development of cost-effective, mission-critical applications. Mobile code and mobile agents [186, 181] are emerging technologies that promise to make much easier the design, implementation, and maintenance of distributed systems. Mobile agents may reduce the network traffic, provide an effective means of overcoming network latency, and, perhaps more importantly, help us to construct more robust and fault-tolerant systems, thanks to their ability to operate asynchronously and autonomously.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott, Adrián Riesco, Alberto Verdejo

User Interfaces and Metalanguage Applications

Abstract

This chapter explains how to use the facilities provided by the predefined modules META-LEVEL and LOOP-MODE for constructing user interfaces and metalanguage applications, in which Maude is used not only to define a domain-specific language or tool, but also to build an environment for the given language or tool. In such applications, the LOOP-MODE module can be used to handle the input/ output and to maintain the persistent state of the language environment or tool. This chapter also describes an approach based on actors to endow Maude with interactive capabilities.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

Part II: Full Maude

Frontmatter

Full Maude: Extending Core Maude

Abstract

During the development of the Maude system we have put special emphasis on the creation of metaprogramming facilities to allow the generation of execution environments for a wide variety of languages and logics. The first most obvious area where Maude can be used as a metalanguage is in building language extensions for Maude itself. Our experience in this regard—first reported in [107], and further documented in [108, 98, 99, 109]—is very encouraging.

We have been able to define in Core Maude a language, that we call Full Maude, with all the features of Maude plus notation for object-oriented programming, parameterized views, module expressions specifying tuples of any size, etc. Although the Maude distribution has included the specification/ implementation of Full Maude since it was first distributed in 1999, Core Maude and Full Maude are now closer than ever before. Many of the features now available in Core Maude, like parameterized modules, views, and module expressions like summation, renaming and instantiation, were available in Full Maude long before they were available in Core Maude [107]. In fact, Full Maude has not only been a complement to Core Maude, but also a vehicle to experiment with new language features. Once these features have been mature enough to be implemented in the core language, we have made the effort to do so. Similarly, it is very likely that those features in Full Maude which are not yet available in Core Maude will become part of it sooner or later, and that new features will be added to Full Maude for purposes of language design and experimentation. This applies not only to Full Maude, but also to further language extensions based on Full Maude such as the strategy language proposed in [202], whose Core Maude implementation is currently underway.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

Object-Oriented Modules

Abstract

In Full Maude, concurrent object-oriented systems can be defined by means of object-oriented modules—introduced by the keyword omod...endom—using a syntax more convenient than that of system modules, because it assumes acquaintance with the basic entities, such as objects, messages and configurations, and supports linguistic distinctions appropriate for the object-oriented case.

As in Core Maude, we may have specifications of object-oriented systems in system modules; for example, we could enter into Full Maude the system modules describing object-based systems discussed in Chapter 11 by enclosing them in parentheses. However, although Maude’s system modules are suffi- cient for specifying object-oriented systems, there are important conceptual advantages provided by Full Maude’s syntax for object-orientedmodules. Such syntax allows the user to think and express his/her thoughts in object-oriented terms whenever such a viewpoint seems best suited for the problem at hand. Those conceptual advantages would be partially lost if only system modules at the Core Maude level were provided.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

Part III: Applications and Tools

Frontmatter

A Sampler of Application Areas

Abstract

This chapter gives an overview of some application areas of rewriting logic and Maude, with pointers to papers and web sites where more information can be found. Some of the material is adapted, with some modifications and extensions, from [199, 3, 217]. Since Maude is a general-purpose declarative programming language, there is in principle no limit to the applications that could be developed using it. Therefore, the areas discussed, although quite diverse, are only a sample of types of applications for which Maude seems particularly well suited. But there are many others. For example, the availability of built-in internet sockets in Maude 2.2 (see Section 11.4.1) opens up interesting possibilities for a new style of declarative internet programming which have already begun to be exploited (see Chapter 16).

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

Some Tools

Abstract

This chapter describes some existing Maude-based tools that are available for download. The first section describes tools concerned with analysis of either Maude specifications, or of extensions of such specifications. The second section describes tools that are not Maude-specific; they are instead concerned with specification and analysis in various application domains and support domain-specific notations. For each tool, its description addresses the following questions:

What does the tool do?
When would you want to use it?
How can the tool and documentation be obtained?

The material in this chapter is a reformulation and adaptation of the material kindly provided to us by the authors of each tool. We cordially thank them all for their help.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott, Christiano Braga, Azadeh Farzan, Joe Hendrix, Peter Ölveczky, Miguel Palomino, Ralf Sasse, Mark-Oliver Stehr, Alberto Verdejo

Part IV: Reference

Frontmatter

Debugging and Troubleshooting

Abstract

There are several approaches to debugging and optimizing Maude programs: tracing, term coloring, using the debugger, and using the profiler.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

Complete List of Maude Commands

Abstract

In this chapter we use curly bracket pairs, ‘{’ and ‘}’, to enclose optional syntax.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

Core Maude Grammar

Abstract

This chapter describes the syntax of Maude using the following extended BNF notation: the symbols ‘(’ and ‘)’ are used as metaparentheses; the symbol ‘|’ is used to separate alternatives; square bracket pairs, ‘[’ and ‘]’, enclose optional syntax; ‘*’ indicates zero or more repetitions of preceding unit; ‘+’ indicates one or more repetitions of preceding unit; and the string “x” denotes x literally. As an application of this notation, A(, A)* indicates a non-empty list of A’s separated by commas. Finally, %%% indicates comments in the syntactic description, as opposed to comments in the Maude code.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

Backmatter

Titel: All About Maude - A High-Performance Logical Framework
verfasst von: Manuel Clavel
Francisco Durán
Steven Eker
Patrick Lincoln
Narciso Martí-Oliet
José Meseguer
Carolyn Talcott
Verlag: Springer Berlin Heidelberg
Electronic ISBN: 978-3-540-71999-1
Print ISBN: 978-3-540-71940-3
DOI: https://doi.org/10.1007/978-3-540-71999-1

Springer Professional

Über dieses Buch

Inhaltsverzeichnis

Frontmatter

Introduction

Introduction

Part I: Core Maude

Frontmatter

Using Maude

Syntax and Basic Parsing

Functional Modules

A Hierarchy of Data Types: From Trees to Sets

System Modules

Playing with Maude

Module Operations

Predefined Data Modules

Specifying Parameterized Data Structures in Maude

Object-Based Programming

Model Checking Invariants Through Search

LTL Model Checking

Reflection, Metalevel Computation, and Strategies

Metaprogramming Applications

Mobile Maude

User Interfaces and Metalanguage Applications

Part II: Full Maude

Frontmatter

Full Maude: Extending Core Maude

Object-Oriented Modules

Part III: Applications and Tools

Frontmatter

A Sampler of Application Areas

Some Tools

Part IV: Reference

Frontmatter

Debugging and Troubleshooting

Complete List of Maude Commands

Core Maude Grammar

Backmatter

Premium Partner