Contents

• List of Figures
  • Introduction
    • Simplicity, expressiveness, and performance
      • Simplicity
      • Expressiveness
      • Performance
    • The logical foundations of Maude
    • Programming, specification, and verification
    • A high-performance logical framework
    • Core Maude vs. Full Maude
    • Manual structure
    • The Maude book
  
  
• Core Maude
  • Using Maude
    • Getting Maude
    • Running Maude
    • Getting support and more information
    • Reporting bugs in Maude
  • Syntax and Basic Parsing
    • Identifiers
    • Modules
    • Sorts and subsorts
    • Operator declarations
    • Kinds
    • Operator overloading
    • Variables
    • Terms and preregularity
    • Parsing
      • Default precedence values
      • Default gathering patterns
      • The extended signature of a module
      • Parsing examples
  • Functional Modules
    • Unconditional equations
    • Unconditional memberships
    • Conditional equations and memberships
    • Operator attributes
      • Equational attributes
      • The iter attribute
      • Constructors
      • Polymorphic operators
      • Format
      • Ditto
      • Operator evaluation strategies
      • Memo
      • Frozen arguments
      • Special
    • Statement attributes
      • Labels
      • Metadata
      • Nonexec
      • Otherwise
    • Admissible functional modules
    • Matching and equational simplification
    • More on matching and simplification modulo
    • The reduce, match, trace, and show commands
  • System Modules
    • Unconditional rules
    • Conditional rules
    • Admissible system modules
    • The rewrite, frewrite, and search commands
      • The rewrite command
      • The frewrite command
      • The search command
  • Module Operations
    • Module importation
      • Protecting
      • Extending
      • Including
      • Default conventions in module importations
      • Some module hierarchy examples
    • Module summation and renaming
      • The summation module expression
      • Module renaming
    • Parameterized programming
      • Theories
      • Views
      • Parameterized modules
      • Module instantiation
      • Lists
      • Sorted lists
  • Predefined Data Modules
    • Boolean values
    • Natural numbers
    • Random numbers and counters
    • Integer numbers
    • Machine integers
    • Rational numbers
    • Floating-point numbers
    • Strings
    • String and number conversions
    • Quoted identifiers
    • Basic theories and standard views
      • TRIV
      • DEFAULT
      • STRICT-WEAK-ORDER and STRICT-TOTAL-ORDER
      • TOTAL-PREORDER and TOTAL-ORDER
    • Containers: lists and sets
      • Lists
      • Sets
      • Relating lists and sets
      • Generalized lists
      • Generalized sets
      • Sortable lists
      • Making lists out of sets
    • Maps and arrays
      • Maps
      • Arrays
    • A linear Diophantine equation solver
  • Object-Based Programming
    • Configurations
    • Object-message fair rewriting
    • Example: data agents
    • External objects
      • Sockets
      • Buffered sockets
  • Model Checking Invariants Through Search
    • Invariants
    • Model checking of invariants
    • Bounded model checking of invariants
    • Verifying infinite-state systems through abstractions
  • LTL Model Checking
    • LTL formulas and the LTL module
    • Associating Kripke structures to rewrite theories
    • LTL model checking
    • The LTL satisfiability and tautology checker
    • Other model-checking examples
  • Reflection, Metalevel Computation, and Strategies
    • Reflection and metalevel computation
    • The META-TERM module
      • Metarepresenting sorts and kinds
      • Metarepresenting terms
    • The META-MODULE module: Metarepresenting modules
    • The META-LEVEL module: Metalevel operations
      • Moving between reflection levels: upModule, upTerm, downTerm, and others
      • Simplifying: metaReduce and metaNormalize
      • Rewriting: metaRewrite and metaFrewrite
      • Applying rules: metaApply and metaXapply
      • Matching: metaMatch and metaXmatch
      • Searching: metaSearch and metaSearchPath
      • Parsing and pretty-printing: metaParse and metaPrettyPrint
      • Sort operations
      • Other metalevel operations: wellFormed
    • Internal strategies
  • User Interfaces and Metalanguage Applications
    • The LOOP-MODE module
    • User interfaces
    • Using the loop
    • Metalanguage applications: tokens, bubbles, and metaparsing
  • Debugging and Troubleshooting
    • Debugging approaches
      • Tracing
      • Term coloring
      • The debugger
      • The profiler
      • Performance note
    • Traps and known problems
      • Associativity and idempotency
      • Segmentation fault (core dumped)
      • Bare variable lefthand sides
      • Operator overloading and associativity
      • Preregularity and equational attributes
      • Collapse theories
      • One-sided identities and associativity
      • Memberships for associative operators
      • Memberships for iterated operators
  
  
• Full Maude
  • Full Maude: Extending Core Maude
    • Running Full Maude
    • Using Core Maude modules in Full Maude
    • Additional module operations in Full Maude
      • The tuple and power module expressions
      • Parameterized views
    • Moving up and down between reflection levels
      • Up
      • Down
    • Differences between Full Maude and Core Maude
  • Object-Oriented Modules
    • Object-oriented systems
      • Objects and messages
      • Classes
      • Inheritance
      • Object-oriented rules
    • Example: a rent-a-car store
    • Object-oriented parameterized programming
      • Theories
      • Views
      • Parameterized object-oriented modules
    • Module operations on object-oriented modules
      • Module summation and renaming
      • Module instantiation
    • Example: extended rent-a-car store
    • A strategy for sequential rule execution
    • Model checking a round-robin scheduling algorithm
    • From object-oriented modules to system modules
  
  
• Reference
  • Complete List of Maude Commands
    • Command line flags
    • Rewriting commands
    • Matching commands
    • Searching commands
    • Tracing commands
    • Print option commands
    • Show option commands
    • Show commands
    • Profiler commands
    • Debugger commands
    • Miscellaneous commands
    • System level commands
  • Core Maude Grammar
    • The grammar
    • Synonyms
    • Lexical Issues
  
  
• Bibliography