[pdf]
In S. Lucas, editor, Proceedings of the Fourth Spanish Conference on Programming
and Computer Languages (PROLE 2004), ENTCS 137,
pages 105-132. Elsevier, 2005.
Abstract: This tutorial describes the equational specification of a series of typical data
structures in Maude. We start with the well-known stacks, queues, and lists,
to continue with binary and search trees. Not only are the simple versions
considered but also advanced ones such as AVL and 2-3-4 trees.
The operator attributes available in Maude allow the specification of data
based on constructors that satisfy some equational properties, like concatenation
of lists which is associative and has the empty list as identity, as opposed to the
free constructors available in other functional programming languages.
Moreover, the expressive version of equational logic in which Maude is based,
namely membership equational logic, allows the faithful specification of types
whose data are defined not only by means of constructors, but also by the
satisfaction of additional properties, like sorted lists or search trees.
In the second part of the paper we describe the use of an inductive theorem
prover, the ITP, which itself is developed and integrated in Maude by means of
the powerful metalevel and metalanguage features offered by the latter,
to prove properties of the data structures. This is work in progress because
the ITP is still under development and, as soon as the data gets a bit complex,
the proof of their properties gets even more complex.
@inproceedings{MartiOlietPalominoVerdejo05,
Author = {Narciso Mart\'{\i}-Oliet and Miguel Palomino and Alberto Verdejo},
Booktitle = {Proceedings of the Fourth Spanish Conference on Programming and Computer Languages (PROLE 2004)},
Editor = {Salvador Lucas},
Number = {1},
Pages = {105-132},
Publisher = {Elsevier},
Series = {Electronic Notes in Theoretical Computer Science},
Title = {A Tutorial on Specifying Data Structures in {Maude}},
Volume = {137},
Year = {2005}}