Manual structure

The present manual documents Maude 2, and explains Maude's basic concepts in a leisurely and mostly informal style. The material is basically presented following a ``grammatical'' order; for example, all features related with operators are discussed together. Concepts are introduced by concrete examples, that may be fragments of modules. The complete module examples are available in http://maude.cs.uiuc.edu.

The manual is divided in three parts: Part I is devoted to Core Maude, Part II is devoted to Full Maude, and Part III is a reference manual. Here is a brief summary of what can be found in the remaining chapters:

Part I.

Core Maude.

Chapter 2

explains how to get Maude, how to install the system on the different platforms supported, and how to run it. It also includes pointers on how to get additional information and support.

Chapter 3

describes the basic syntactic constructs of the language, including what is an identifier, a sort, and an operator. The different kinds of declarations that can be included in the different types of modules are explained here, in addition to fundamental concepts such as kinds or terms, and a discussion on parsing.

Chapter 4

introduces functional modules, and the different statements that can be found in this kind of modules, namely equations and membership axioms. Operator and statement attributes are also introduced. The final part of this chapter is devoted to the use of functional modules for equational simplification, for which matching modulo axioms is a fundamental feature.

Chapter 5

introduces system modules, and is mainly devoted to rules, term rewriting, and the search command.

Chapter 6

explains the support for modularity provided by Core Maude. It describes first the different modes of module importation, namely protecting, extending, and including. Then it introduces the module summation and renaming operations. Finally, this chapter explains the powerful form of parameterized programming available in Core Maude, based on theories and views.

Chapter 7

provides detailed descriptions of the different predefined data types available, including Booleans, natural numbers, integers, rationals, floating-point numbers, strings, and quoted identifiers. It also describes the generic containers provided by Maude, namely lists, sets, maps, and arrays. The chapter finishes with a description of a built-in linear Diophantine equation solver.

Chapter 8

explains the basic support for object-based programming, with special emphasis on the standard notation for object systems. It also describes how communication with external objects is supported in Core Maude through sockets.

Chapter 9

explains how to use the search command to model check invariant properties of concurrent systems specified as system modules in Maude.

Chapter 10

introduces linear temporal logic (LTL) and describes the facilities for LTL model checking provided by the Maude system. This procedure can be used to prove properties when the set of states reachable from an initial state in a system module is finite. When this is not the case, it may be possible to use an equational abstraction technique for reducing the size of the state space.

Chapter 11

presents the reflective capabilities of the Maude system. The concept of reflection is introduced, and the effective way of supporting metalevel computation is discussed. The predefined module META-LEVEL and its submodules are presented, with special emphasis on the descent functions provided. The chapter ends with an introduction to the notion of internal strategies.

Chapter 12

explains the way of using the facilities provided by the modules META-LEVEL and LOOP-MODE for the construction of user interfaces and metalanguage applications.

Chapter 13

discusses debugging and troubleshooting, considering the different debugging facilities provided: tracing, term coloring, the debugger, and the profiler. A number of traps and known problems are also commented.

Part II.

Full Maude.

Chapter 14

explains the nature of Full Maude, and how to use it. This chapter includes information on how to load Core Maude modules into Full Maude, on the additional module operations (supported by tuple generation and parameterized views), and on the facilities available in Full Maude for moving up and down between reflection levels.

Chapter 15

introduces object-oriented modules, which provide a syntax more convenient than that of system modules for object-oriented applications, with direct support for the declaration of classes, inheritance, and useful default conventions in the definition of rules. Such object-oriented modules can also be parameterized. This chapter includes several extended examples that illustrate the power of combining the additional features available in Full Maude.

Part III.

Reference.

Chapter 16

gives a complete list of the commands available in Maude.

Chapter 17

includes the grammar of Core Maude.