1 Introduction
 1.1 Simplicity, expressiveness, and performance
  1.1.1 Simplicity
  1.1.2 Expressiveness
  1.1.3 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
  3.9.1 Default precedence values
  3.9.2 Default gathering patterns
  3.9.3 The extended signature of a module
  3.9.4 Parsing examples
4 Functional Modules
 4.1 Unconditional equations
 4.2 Unconditional memberships
 4.3 Conditional equations and memberships
 4.4 Operator attributes
  4.4.1 Equational attributes
  4.4.2 The iter attribute
  4.4.3 Constructors
  4.4.4 Polymorphic operators
  4.4.5 Format
  4.4.6 Ditto
  4.4.7 Operator evaluation strategies
  4.4.8 Memo
  4.4.9 Frozen arguments
  4.4.10 Special
 4.5 Statement attributes
  4.5.1 Labels
  4.5.2 Metadata
  4.5.3 Nonexec
  4.5.4 Otherwise
  4.5.5 Print
 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
  5.4.1 The rewrite command
  5.4.2 The frewrite command
  5.4.3 The search command
6 Module Operations
 6.1 Module importation
  6.1.1 Protecting
  6.1.2 Extending
  6.1.3 Including
  6.1.4 Default conventions in module importations
  6.1.5 Some module hierarchy examples
 6.2 Module summation and renaming
  6.2.1 The summation module expression
  6.2.2 Module renaming
 6.3 Parameterized programming
  6.3.1 Theories
  6.3.2 Views
  6.3.3 Parameterized modules
  6.3.4 Module instantiation
  6.3.5 Lists
  6.3.6 Sorted lists
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.11.1 TRIV
  7.11.2 DEFAULT
  7.11.3 STRICT-WEAK-ORDER and STRICT-TOTAL-ORDER
  7.11.4 TOTAL-PREORDER and TOTAL-ORDER
 7.12 Containers: lists and sets
  7.12.1 Lists
  7.12.2 Sets
  7.12.3 Relating lists and sets
  7.12.4 Generalized lists
  7.12.5 Generalized sets
  7.12.6 Sortable lists
  7.12.7 Making lists out of sets
 7.13 Maps and arrays
  7.13.1 Maps
  7.13.2 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
  8.4.1 Sockets
  8.4.2 Buffered sockets
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.2.1 Metarepresenting sorts and kinds
  11.2.2 Metarepresenting terms
 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.5.1 Moving between reflection levels: upModule, upTerm, downTerm, and others
  11.5.2 Simplifying: metaReduce and metaNormalize
  11.5.3 Rewriting: metaRewrite and metaFrewrite
  11.5.4 Applying rules: metaApply and metaXapply
  11.5.5 Matching: metaMatch and metaXmatch
  11.5.6 Searching: metaSearch and metaSearchPath
  11.5.7 Parsing and pretty-printing: metaParse and metaPrettyPrint
  11.5.8 Sort operations
  11.5.9 Other metalevel operations: wellFormed
 11.6 Internal strategies
12 Unification
 12.1 Introduction
 12.2 Order-sorted unification modulo a set of axioms
 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.6.1 Narrowing-based unification
  12.6.2 Symbolic reachability analysis in rewrite theories
  12.6.3 Other automated deduction applications
 12.7 Endogenous vs. exogenous order-sorted unification algorithms
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.1.1 Tracing
  14.1.2 Term coloring
  14.1.3 The debugger
  14.1.4 The profiler
  14.1.5 Performance note
 14.2 Traps and known problems
  14.2.1 Associativity and idempotency
  14.2.2 Segmentation fault (core dumped)
  14.2.3 Bare variable lefthand sides
  14.2.4 Operator overloading and associativity
  14.2.5 Preregularity and equational attributes
  14.2.6 Collapse theories
  14.2.7 One-sided identities and associativity
  14.2.8 Memberships for associative operators
  14.2.9 Memberships for iterated operators
  14.2.10 Ambiguity in print attribute items
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.3.1 The tuple and power module expressions
  15.3.2 Parameterized views
 15.4 Moving up and down between reflection levels
  15.4.1 Up
  15.4.2 Down
 15.5 Differences between Full Maude and Core Maude
16 Narrowing
 16.1 Introduction
 16.2 Completeness of narrowing
 16.3 Theories supported
 16.4 The narrowing search command
 16.5 Unification with identities: The id-unify command
 16.6 Reachability at the metalevel: metaNarrowSearch
 16.7 Unification with identities at the metalevel: metaACUUnify
17 Object-Oriented Modules
 17.1 Object-oriented systems
  17.1.1 Objects and messages
  17.1.2 Classes
  17.1.3 Inheritance
  17.1.4 Object-oriented rules
 17.2 Example: a rent-a-car store
 17.3 Object-oriented parameterized programming
  17.3.1 Theories
  17.3.2 Views
  17.3.3 Parameterized object-oriented modules
 17.4 Module operations on object-oriented modules
  17.4.1 Module summation and renaming
  17.4.2 Module instantiation
 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 command
 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