Next:
Using Maude
Up:
Maude Manual (Version 2.3)
Previous:
Acknowledgements
Contents
Core Maude
Subsections
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
Prime numbers sieve
Vending machine
Bank accounts and object configurations
Hierarchy of predefined modules
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
Sorting lists with respect to a strict weak order
Sorting lists with respect to a total preorder
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
metaReduce
metaNormalize
Rewriting:
metaRewrite
and
metaFrewrite
metaRewrite
metaFrewrite
Applying rules:
metaApply
and
metaXapply
metaApply
metaXapply
Matching:
metaMatch
and
metaXmatch
Searching:
metaSearch
and
metaSearchPath
metaSearch
metaSearchPath
Parsing and pretty-printing:
metaParse
and
metaPrettyPrint
metaParse
metaPrettyPrint
Sort operations
sortLeq
sameKind
completeName
getKind
and
getKinds
lesserSorts
leastSort
glbSorts
maximalSorts
and
minimalSorts
maximalAritySet
Other metalevel operations:
wellFormed
Internal strategies
User Interfaces and Metalanguage Applications
The
LOOP-MODE
module
User interfaces
Using the loop
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
The Maude Team
