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 Manual structure
1.6 The Maude book
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 Object-Oriented Modules
6.1 Objects, messages and configurations
6.1.1 Classes
6.1.2 Messages
6.1.3 Class inheritance
6.1.4 Object-oriented statements
6.1.5 Search on object-oriented modules
6.2 Example: a rent-a-car store
6.3 Object-message fair rewriting
6.4 Object-based programming
6.4.1 Object-based programming using the CONFIGURATION module
6.4.2 Object-based programming without the CONFIGURATION module
6.5 From object-oriented modules to system modules
7 Module Operations
7.1 Module importation
7.1.1 Protecting
7.1.2 Extending
7.1.3 Generated-by
7.1.4 Including
7.1.5 Default conventions in module importations
7.1.6 Some module hierarchy examples
7.2 The summation module expression
7.3 Module renaming
7.4 Parameterized programming
7.4.1 Theories
7.4.2 Views
7.4.3 Parameterized modules
7.4.4 Module instantiation
7.4.5 Lists
7.4.6 Sorted lists
7.4.7 Parameterized views
7.5 Example: data agents
7.6 Example: extended rent-a-car store
8 Predefined Data Modules
8.1 Boolean values
8.2 Initial equality predicate
8.3 Natural numbers
8.4 Random numbers and counters
8.5 Integer numbers
8.6 Machine integers
8.7 Rational numbers
8.8 Floating-point numbers
8.9 Strings
8.10 String and number conversions
8.11 Quoted identifiers
8.12 Conversions between strings and lists of quoted ids.
8.13 Basic theories and standard views
8.13.1 TRIV
8.13.2 DEFAULT
8.13.3 STRICT-WEAK-ORDER and STRICT-TOTAL-ORDER
8.13.4 TOTAL-PREORDER and TOTAL-ORDER
8.14 Containers: lists and sets
8.14.1 Lists
8.14.2 Sets
8.14.3 Relating lists and sets
8.14.4 Generalized lists
8.14.5 Generalized sets
8.14.6 Sortable lists
8.14.7 Making lists out of sets
8.15 Maps and arrays
8.15.1 Maps
8.15.2 Arrays
8.16 A linear Diophantine equation solver
8.17 Predefined parameterized views
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 Directory API
9.4 Sockets
9.4.1 An HTTP/1.0 client example
9.4.2 Two-Way Communication
9.4.3 Buffered sockets
9.5 Processes
9.5.1 A desk calculator process
9.5.2 Python and Maude processes
9.6 Time API
9.6.1 Timers
9.6.2 Current UTC and local time
9.6.3 Measuring an interval of time
9.6.4 An example with timers
9.7 Pseudo-random number generator objects
9.8 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 Model checking a round-robin scheduling algorithm
12.6 LTL+ formulas and the LTL+ model checker
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
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 Filtered vs. unfiltered symbolic reachability analysis
15.6.3 Folding the narrowing space
15.6.4 Reducing the symbolic reachability analysis using vfold
15.6.5 Narrowing path commands
15.6.6 Narrowing from multiple initial terms
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
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
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
19 Meta-interpreters
19.1 Maude meta-interpreters
19.1.1 Some additional information on meta-interpreters
19.2 A Russian dolls example
19.3 An execution environment for Mini-Maude
20 LaTeX Support
20.1 Some basic first examples
20.2 The latex attribute
21 Debugging and Troubleshooting
21.1 Debugging approaches
21.1.1 Tracing
21.1.2 Term coloring
21.1.3 The debugger
21.1.4 Status report
21.1.5 The profiler
21.1.6 Performance note
21.2 Debugging strategy executions
21.3 Traps and known problems
21.3.1 Associativity and idempotency
21.3.2 Internal errors and stack overflow
21.3.3 Bare variable lefthand sides
21.3.4 Operator overloading and associativity
21.3.5 Preregularity and equational attributes
21.3.6 Collapse theories
21.3.7 One-sided identities and associativity
21.3.8 Memberships for associative operators
21.3.9 Memberships for iterated operators
21.3.10 Ambiguity in print attribute items
A Complete List of Maude Commands
A.1 Command line flags
A.2 Rewriting commands
A.3 Matching commands
A.4 Searching commands
A.5 Strategic rewriting commands
A.6 Unification, variants, and narrowing commands
A.7 SMT commands
A.8 Tracing commands
A.9 Print attribute commands
A.10 Print option commands
A.11 Show option commands
A.12 Show commands
A.13 Profiler commands
A.14 Debugger commands
A.15 Miscellaneous commands
A.16 System level commands
B Maude Grammar
B.1 The grammar
B.2 Synonyms
B.3 Lexical and other Issues
Bibliography