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
  6.3.7 Parameterized views
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 Conversions between strings and lists of quoted identifiers
 7.12 Basic theories and standard views
  7.12.1 TRIV
  7.12.2 DEFAULT
  7.12.3 STRICT-WEAK-ORDER and STRICT-TOTAL-ORDER
  7.12.4 TOTAL-PREORDER and TOTAL-ORDER
 7.13 Containers: lists and sets
  7.13.1 Lists
  7.13.2 Sets
  7.13.3 Relating lists and sets
  7.13.4 Generalized lists
  7.13.5 Generalized sets
  7.13.6 Sortable lists
  7.13.7 Making lists out of sets
 7.14 Maps and arrays
  7.14.1 Maps
  7.14.2 Arrays
 7.15 A linear Diophantine equation solver
 7.16 Predefined Parameterized Views
8 Object-Based Programming
 8.1 Configurations
 8.2 Object-message fair rewriting
 8.3 Example: data agents
9 External Objects and IO
 9.1 Standard streams
  9.1.1 The Hello Word! example
  9.1.2 A ROT13 cypher example
  9.1.3 A calculator example
 9.2 File I/O
  9.2.1 A file copy example
 9.3 Sockets
  9.3.1 An HTTP/1.0 client example
  9.3.2 Buffered sockets
 9.4 Processes
  9.4.1 A desk calculator process
  9.4.2 Python and Maude processes
 9.5 Control-C on external events
10 Strategy Language
 10.1 The strategy language
  10.1.1 Basic control combinators
  10.1.2 Rewriting of subterms
  10.1.3 The one operator
  10.1.4 Strategy calls
 10.2 Strategy modules
  10.2.1 Module importation
 10.3 Parameterization in strategy modules
 10.4 Strategy search and the dsrewrite command
11 Model Checking Invariants Through Search
 11.1 Invariants
 11.2 Model checking of invariants
 11.3 Bounded model checking of invariants
 11.4 Verifying infinite-state systems through abstractions
12 LTL Model Checking
 12.1 LTL formulas and the LTL module
 12.2 Associating Kripke structures to rewrite theories
 12.3 LTL model checking
 12.4 The LTL satisfiability and tautology checker
 12.5 Other model-checking examples
13 Unification
 13.1 Introduction
 13.2 Order-sorted unification
  13.2.1 A hybrid approach to equational order-sorted unification
 13.3 Theories currently supported
 13.4 The unify command
  13.4.1 Non-supported unification examples
  13.4.2 Associative-commutative (AC) unification examples
  13.4.3 Unification examples with the iter attribute
  13.4.4 Associative-commutative with identity (ACU) unification examples
  13.4.5 Unification examples with an identity symbol
  13.4.6 Associative (A) unification examples
  13.4.7 Associative with identity (AU) unification examples
 13.5 Some applications of unification
  13.5.1 Narrowing-based unification
  13.5.2 Symbolic reachability analysis in rewrite theories
  13.5.3 Other automated deduction applications
 13.6 Endogenous vs. exogenous order-sorted unification algorithms
 13.7 Some notes on the implementation of unification
  13.7.1 Combining unification algorithms
  13.7.2 Combining incomplete unification algorithms
  13.7.3 Diophantine basis element selection
14 Variants and Variant Unification
 14.1 Introduction
 14.2 Term variants
 14.3 Theories currently supported
 14.4 The get variants command
 14.5 Variant generation with irreducibility constraints
 14.6 Incremental variant generation
 14.7 Variant generation in incomplete unification examples
 14.8 Variant-based equational order-sorted unification
 14.9 The variant unify command
 14.10 Variant-based unification with irreducibility constraints
 14.11 Incremental variant unification
 14.12 Variant unification in incomplete unification examples
 14.13 The variant match command
15 Narrowing
 15.1 Introduction
 15.2 Applications
 15.3 Completeness of narrowing
 15.4 Narrowing with simplification
 15.5 Theories supported for narrowing reachability
 15.6 The vu-narrow command
  15.6.1 Variant Unification Options
  15.6.2 Folding the narrowing space
 15.7 Narrowing with extra variables in righthand sides of rules
16 SMT Solving
 16.1 Boolean formulas
 16.2 Formulas using integer linear arithmetic
 16.3 Formulas using rational linear arithmetic
 16.4 Formulas using rational and integer linear arithmetic
 16.5 Satisfiability of formulas
 16.6 A brief introduction to variant satisfiability
17 Reflection, Metalevel Computation, and Internal Strategies
 17.1 Reflection and metalevel computation
 17.2 The META-TERM module
  17.2.1 Metarepresenting sorts and kinds
  17.2.2 Metarepresenting terms
 17.3 The META-STRATEGY module: Metarepresenting the strategy language
 17.4 The META-MODULE module: Metarepresenting modules
 17.5 The META-VIEW module: Metarepresenting views
 17.6 The META-LEVEL module: Metalevel operations
  17.6.1 Moving between reflection levels: upModule, upTerm, and others
  17.6.2 Simplifying: metaReduce and metaNormalize
  17.6.3 Rewriting: metaRewrite and metaFrewrite
  17.6.4 Applying rules: metaApply and metaXapply
  17.6.5 Matching: metaMatch and metaXmatch
  17.6.6 Searching: metaSearch and metaSearchPath
  17.6.7 Rewriting using strategies: metaSrewrite
  17.6.8 Unification
  17.6.9 Variants: metaGetVariant
  17.6.10 Variant Matching and Unification
  17.6.11 Narrowing
  17.6.12 Checking satisfiability modulo theories: metaCheck
  17.6.13 Parsing and pretty-printing: metaParse and metaPrettyPrint
  17.6.14 Sort operations
  17.6.15 Other metalevel operations: wellFormed
 17.7 Internal strategies
  17.7.1 Internal and object-level strategies
18 User Interfaces and Metalanguage Applications
 18.1 User interfaces
 18.2 The interaction with the system
 18.3 Tokens, bubbles, and metaparsing
 18.4 The LOOP-MODE module (deprecated)
19 Meta-interpreters
 19.1 Maude meta-interpreters
 19.2 A Russian dolls example
 19.3 An execution environment for Mini-Maude
20 Debugging and Troubleshooting
 20.1 Debugging approaches
  20.1.1 Tracing
  20.1.2 Term coloring
  20.1.3 The debugger
  20.1.4 Status report
  20.1.5 The profiler
  20.1.6 Performance note
 20.2 Debugging strategy executions
 20.3 Traps and known problems
  20.3.1 Associativity and idempotency
  20.3.2 Segmentation fault (core dumped)
  20.3.3 Bare variable lefthand sides
  20.3.4 Operator overloading and associativity
  20.3.5 Preregularity and equational attributes
  20.3.6 Collapse theories
  20.3.7 One-sided identities and associativity
  20.3.8 Memberships for associative operators
  20.3.9 Memberships for iterated operators
  20.3.10 Ambiguity in print attribute items
II  Full Maude
21 Full Maude: Extending Core Maude
 21.1 Running Full Maude
 21.2 Using Core Maude modules in Full Maude
 21.3 Additional module operations in Full Maude
  21.3.1 The tuple and power module expressions
 21.4 Moving up and down between reflection levels
  21.4.1 Up
  21.4.2 Down
 21.5 Differences between Full Maude and Core Maude
22 Object-Oriented Modules
 22.1 Object-oriented systems
  22.1.1 Objects and messages
  22.1.2 Classes
  22.1.3 Inheritance
  22.1.4 Object-oriented rules
 22.2 Example: a rent-a-car store
 22.3 Object-oriented parameterized programming
  22.3.1 Theories
  22.3.2 Views
  22.3.3 Parameterized object-oriented modules
 22.4 Module operations on object-oriented modules
  22.4.1 Module summation and renaming
  22.4.2 Module instantiation
 22.5 Example: extended rent-a-car store
 22.6 A strategy for sequential rule execution
 22.7 Model checking a round-robin scheduling algorithm
 22.8 From object-oriented modules to system modules
III  Reference
23 Complete List of Maude Commands
 23.1 Command line flags
 23.2 Rewriting commands
 23.3 Matching commands
 23.4 Searching commands
 23.5 Strategic rewriting commands
 23.6 Unification, variants, and narrowing commands
 23.7 SMT commands
 23.8 Tracing commands
 23.9 Print attribute commands
 23.10 Print option commands
 23.11 Show option commands
 23.12 Show commands
 23.13 Profiler commands
 23.14 Debugger commands
 23.15 Miscellaneous commands
 23.16 System level commands
24 Core Maude Grammar
 24.1 The grammar
 24.2 Synonyms
 24.3 Lexical Issues
Bibliography