Abstract
This chapter describes how data types can be defined in Maude as equational specifications. Section 2.1 introduces specification and execution in Maude with some simple “Hello World!” examples specifying the natural numbers and the Boolean values. Section 2.2 defines many-sorted equational specifications and explains how Maude computes with equations.
This is a preview of subscription content, log in via an institution.
Notes
- 1.
The command load nat-add does the same thing, but does not print the list of modules.
- 2.
Although protecting and including have different mathematical meaning (see [21] for details), the Maude system treats them in the same way.
- 3.
A “decrease” typically means that the number of function symbol occurrences in a constructor ground term must decrease.
- 4.
That is, using only a finite number of sorts, functions, and equations.
- 5.
A computable algebra is one whose domains are recursive sets (i.e., we can decide whether an element is a member of the set) and whose functions are recursive (i.e., computable) functions.
- 6.
The modules NAT1 and BOOLEAN1 are defined in Exercise 9.
- 7.
A connected component of \((S, \le )\) is an equivalence class in the transitive and symmetric closure of \((S, \le )\).
- 8.
The extra parentheses in the following equations are not needed, due to the precedence on the operators. They are just added for readability.
- 9.
These are binary trees where, for each subtree, the root element of the (sub)tree is greater than or equal to all elements in its left subtree and is less than or equal to all elements in its right subtree.
- 10.
Parts of the specifications are omitted and replaced by ‘...’.
- 11.
Multiple declarations of the same non-constructor function are usually not needed, since equations will reduce a term to a constructor term of the right sort. However, in built-in modules, operators such as + have multiple declarations, since it is a built-in function not defined by equations.
- 12.
The arrow ~> means that the function is a partial function.
- 13.
Maude has an idempotency attribute, but currently it cannot be used with the assoc attribute.
- 14.
Is it i=0 or i=1? j=i or j=i+1? i++ or ++i? Until \({\small \texttt {j>k}}\) or \({\small \texttt {j>=k}}\)? A -1 or +1 missing somewhere?
- 15.
There are \(2^n\) different subsets of an n-element set, and n! different permutations of n elements.
- 16.
The complexity of an algorithm can be precisely defined in a machine-independent way as the number of steps performed by a Turing machine implementing the algorithm.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2017 Springer-Verlag London
About this chapter
Cite this chapter
Ölveczky, P.C. (2017). Equational Specification in Maude. In: Designing Reliable Distributed Systems. Undergraduate Topics in Computer Science. Springer, London. https://doi.org/10.1007/978-1-4471-6687-0_2
Download citation
DOI: https://doi.org/10.1007/978-1-4471-6687-0_2
Published:
Publisher Name: Springer, London
Print ISBN: 978-1-4471-6686-3
Online ISBN: 978-1-4471-6687-0
eBook Packages: Computer ScienceComputer Science (R0)