PIC

Maude Manual
(Version 3.5)

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



September 2024

  

Maude 3 is copyright 1997-2024 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 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
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 Object-Oriented Modules
6.1 Objects, messages and configurations
6.2 Example: a rent-a-car store
6.3 Object-message fair rewriting
6.4 Object-based programming
6.5 From object-oriented modules to system modules
7 Module Operations
7.1 Module importation
7.2 The summation module expression
7.3 Module renaming
7.4 Parameterized programming
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.14 Containers: lists and sets
8.15 Maps and arrays
8.16 A linear Diophantine equation solver
8.17 Predefined parameterized views
9 External Objects and IO
9.1 Standard streams
9.2 File I/O
9.3 Directory API
9.4 Sockets
9.5 Processes
9.6 Time API
9.7 Pseudo-random number generator objects
9.8 Control-C on external events
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
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
13 Unification
13.1 Introduction
13.2 Order-sorted unification
13.3 Theories currently supported
13.4 The unify command
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.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.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
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
21 LaTeX Support
21.1 Some basic first examples
21.2 The latex attribute
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
Index