Contents
List of Figures
1 Introduction
 1.1 Simplicity, expressiveness, and performance
 1.2 The logical foundations of Maude
 1.3 Programming, specification, and verification
 1.4 A high-performance logical framework
 1.5 Core Maude vs. Full Maude
 1.6 Manual structure
 1.7 The Maude book
I  Core Maude
2 Using Maude
 2.1 Getting Maude
 2.2 Running Maude
 2.3 Getting support and more information
 2.4 Reporting bugs in Maude
3 Syntax and Basic Parsing
 3.1 Identifiers
 3.2 Modules
 3.3 Sorts and subsorts
 3.4 Operator declarations
 3.5 Kinds
 3.6 Operator overloading
 3.7 Variables
 3.8 Terms and preregularity
 3.9 Parsing
4 Functional Modules
 4.1 Unconditional equations
 4.2 Unconditional memberships
 4.3 Conditional equations and memberships
 4.4 Operator attributes
 4.5 Statement attributes
 4.6 Admissible functional modules
 4.7 Matching and equational simplification
 4.8 More on matching and simplification modulo
 4.9 The reduce, match, trace, and show commands
5 System Modules
 5.1 Unconditional rules
 5.2 Conditional rules
 5.3 Admissible system modules
 5.4 The rewrite, frewrite, and search commands
6 Module Operations
 6.1 Module importation
 6.2 Module summation and renaming
 6.3 Parameterized programming
7 Predefined Data Modules
 7.1 Boolean values
 7.2 Natural numbers
 7.3 Random numbers and counters
 7.4 Integer numbers
 7.5 Machine integers
 7.6 Rational numbers
 7.7 Floating-point numbers
 7.8 Strings
 7.9 String and number conversions
 7.10 Quoted identifiers
 7.11 Basic theories and standard views
 7.12 Containers: lists and sets
 7.13 Maps and arrays
 7.14 A linear Diophantine equation solver
8 Object-Based Programming
 8.1 Configurations
 8.2 Object-message fair rewriting
 8.3 Example: data agents
 8.4 External objects
9 Model Checking Invariants Through Search
 9.1 Invariants
 9.2 Model checking of invariants
 9.3 Bounded model checking of invariants
 9.4 Verifying infinite-state systems through abstractions
10 LTL Model Checking
 10.1 LTL formulas and the LTL module
 10.2 Associating Kripke structures to rewrite theories
 10.3 LTL model checking
 10.4 The LTL satisfiability and tautology checker
 10.5 Other model-checking examples
11 Reflection, Metalevel Computation, and Strategies
 11.1 Reflection and metalevel computation
 11.2 The META-TERM module
 11.3 The META-MODULE module: Metarepresenting modules
 11.4 The META-VIEW module: Metarepresenting views
 11.5 The META-LEVEL module: Metalevel operations
 11.6 Internal strategies
12 Unification and Variant Generation
 12.1 Introduction
 12.2 Order-sorted unification
 12.3 Theories currently supported
 12.4 The unify command
 12.5 Unification at the metalevel: metaUnify and metaDisjointUnify
 12.6 Some applications of unification
 12.7 Endogenous vs. exogenous order-sorted unification algorithms
 12.8 Some notes on the implementation of unification
 12.9 Variants
 12.10 Variant-based equational order-sorted unification
13 User Interfaces and Metalanguage Applications
 13.1 The LOOP-MODE module
 13.2 User interfaces
 13.3 Using the loop
 13.4 Tokens, bubbles, and metaparsing
14 Debugging and Troubleshooting
 14.1 Debugging approaches
 14.2 Traps and known problems
II  Full Maude
15 Full Maude: Extending Core Maude
 15.1 Running Full Maude
 15.2 Using Core Maude modules in Full Maude
 15.3 Additional module operations in Full Maude
 15.4 Moving up and down between reflection levels
 15.5 Ax-coherence completion
 15.6 Differences between Full Maude and Core Maude
16 Narrowing
 16.1 Introduction
 16.2 Theories supported for narrowing reachability
 16.3 The narrowing search command
17 Object-Oriented Modules
 17.1 Object-oriented systems
 17.2 Example: a rent-a-car store
 17.3 Object-oriented parameterized programming
 17.4 Module operations on object-oriented modules
 17.5 Example: extended rent-a-car store
 17.6 A strategy for sequential rule execution
 17.7 Model checking a round-robin scheduling algorithm
 17.8 From object-oriented modules to system modules
III  Reference
18 Complete List of Maude Commands
 18.1 Command line flags
 18.2 Rewriting commands
 18.3 Matching commands
 18.4 Searching commands
 18.5 Unification and variants commands
 18.6 Tracing commands
 18.7 Print attribute commands
 18.8 Print option commands
 18.9 Show option commands
 18.10 Show commands
 18.11 Profiler commands
 18.12 Debugger commands
 18.13 Miscellaneous commands
 18.14 System level commands
19 Core Maude Grammar
 19.1 The grammar
 19.2 Synonyms
 19.3 Lexical Issues
Bibliography
Bibliography
Index
Index of Maude Modules
Index of Maude Theories
Index of Maude Views