Up Next
Go up to Top
Go forward to 1 Introduction

Contents

  • Contents
  • 1 Introduction
  • 1.1 The Logical Basis of Maude
  • 1.2 Core Maude
  • 1.3 Full Maude
  • 1.4 Applications
  • Acknowledgments
  • 2 Core Maude
  • 2.1 Functional Modules
  • 2.1.1 Identifiers, Order-Sorted Signatures, and Overloading
  • 2.1.2 A Set Hierarchy Example
  • 2.1.3 Operator Evaluation Strategies
  • 2.2 Rewriting Logic and System Modules
  • 2.3 Module Hierarchies
  • 2.4 Some Predefined Modules
  • 2.4.1 Truth and Booleans
  • 2.4.2 The Machine Integers
  • 2.4.3 Quoted Identifiers
  • 2.5 Reflection and the META-LEVEL
  • 2.5.1 Reflection and Metalevel Computation
  • 2.5.2 The Module META-LEVEL
  • 2.5.3 Representing Terms
  • 2.5.4 Representing Modules
  • 2.5.5 Descent Functions
  • 2.5.6 Parsing, Pretty Printing, and Sort Functions
  • 2.6 Internal Strategies
  • 2.6.1 The Game of Nim
  • 2.6.2 A Meta-Interpreter
  • 2.7 Parsing, Bubbles and Meta-Parsing
  • 2.7.1 MSCP Parser Design: An Overview
  • 2.7.2 Mixfix Parsing of Terms in a Module
  • 2.7.3 Parsing Terms in the Extended Signature of a Module
  • 2.7.4 Precedence and Gathering
  • 2.7.5 Default Precedence and Gathering
  • 2.7.6 Tokens, Bubbles and Metaparsing
  • 2.8 LOOP-MODE and Metalanguage Uses
  • 2.8.1 The Use of the Loop
  • 2.8.2 Metalanguage Uses of Maude
  • 2.9 System Issues and Debugging
  • 2.9.1 Command Line Options
  • 2.9.2 Debugging Core Maude Specifications
  • 2.9.3 User Facilities Not Yet Implemented
  • 2.9.4 Miscellaneous Differences from OBJ3
  • 2.9.5 Traps for the Unwary
  • 2.9.6 Known Problems
  • 3 Full Maude
  • 3.1 Functional and System Modules
  • 3.2 Object-Oriented Modules
  • 3.2.1 The Syntax of Object-Oriented Modules
  • 3.2.2 Transforming Object-Oriented Modules into System Modules
  • 3.3 Structured Specifications and Extensions of META-LEVEL
  • 3.4 Commands and the Module Database
  • 3.5 Parameterized Programming
  • 3.5.1 Theories
  • 3.5.2 Parameterized Modules
  • 3.5.3 Views
  • 3.5.4 Module Expressions
  • 3.6 Syntactic Restrictions and Caveats
  • 4 The Semantics of Maude
  • 4.1 Membership Equational Logic and Functional Modules
  • 4.2 Rewriting Logic
  • 4.2.1 Theories and Deduction
  • 4.2.2 Models
  • 4.3 Semantics of Object-Oriented and System Modules
  • References
  • A List of Core Maude Commands
  • A.1 Rewriting Commands
  • A.2 Matching Commands
  • A.3 Tracing Commands
  • A.4 Print Option Commands
  • A.5 Show Commands
  • A.6 Debugger Commands
  • A.7 Miscellaneous Commands
  • A.8 System Commands
  • A.9 Abbreviations and Synonyms
  • A.10 Deprecated features
  • B The Grammar of Core Maude
  • B.1 Lexical Issues
  • C The Signature of Full Maude
  • D Standard Library of Predefined Modules
  • E A Software Architecture Interoperation Example
  • Footnotes

  • Up Next