PIC

Maude Manual
(Version 3.0)

Manuel Clavel
Francisco Durán
Steven Eker
Santiago Escobar
Patrick Lincoln
Narciso Martí-Oliet
José Meseguer
Rubén Rubio
Carolyn Talcott



December 2019, revised January 2020

  

Maude 3 is copyright 1997-2019 SRI International, Menlo Park, CA 94025, USA. The Maude system is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. The Maude system is distributed in the hope that it will be useful, but without any warranty; without even the implied warranty of merchantability or fitness for a particular purpose. See the GNU General Public License for more details.

Contents
List of Figures
1 Introduction
 1.1 Simplicity, expressiveness, and 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
4 Functional Modules
 4.1 Unconditional equations
 4.2 Unconditional memberships
 4.3 Conditional equations and memberships
 4.4 Operator attributes
 4.5 Statement attributes
 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
6 Module Operations
 6.1 Module importation
 6.2 Module summation and renaming
 6.3 Parameterized programming
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.13 Containers: lists and sets
 7.14 Maps and 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.2 File I/O
 9.3 Sockets
 9.4 Buffered sockets
10 Strategy Language
 10.1 The strategy language
 10.2 Strategy modules
 10.3 Parameterization in strategy modules
 10.4 Strategy search and the dsrewrite command
 10.5 Case study: logic programming
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.3 Theories currently supported
 13.4 The unify command
 13.5 Some applications of unification
 13.6 Endogenous vs. exogenous order-sorted unification algorithms
 13.7 Some notes on the implementation of unification
14 Variants and Variant Unification
 14.1 Introduction
 14.2 Theories currently supported
 14.3 The get variants command
 14.4 Variant generation with irreducibility constraints
 14.5 Incremental variant generation
 14.6 Variant generation in incomplete unification examples
 14.7 Variant-based equational order-sorted unification
 14.8 The variant unify command
 14.9 Variant-based unification with irreducibility constraints
 14.10 Incremental variant unification
 14.11 Variant unification in incomplete unification examples
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.7 The fvu-narrow command
 15.8 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.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.7 Internal 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.2 Debugging strategy executions
 20.3 Traps and known problems
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.4 Moving up and down between reflection levels
 21.5 Ax-coherence completion
 21.6 Differences between Full Maude and Core Maude
22 Object-Oriented Modules
 22.1 Object-oriented systems
 22.2 Example: a rent-a-car store
 22.3 Object-oriented parameterized programming
 22.4 Module operations on object-oriented modules
 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
Index
Index of Maude Modules
Index of Maude Theories
Index of Maude Views