Abstract
Maude is a wide-spectrum reflective logical language based on rewriting logic [7] that can be used to specify, prototype, and formally analyze concurrent soft- ware systems, specification languages, logics, and theorem provers. Because of its efficient implementation, it can also be used as a programming language and as a meta-tool to generate other tools. This paper gives a brief introduction to the language and illustrates with examples some of the features of the current version, available free of charge together with examples, documentation, and papers from SRI: see http://maude.csl.sri.com. The key characteristics of Maude can be summarized as follows:
-
—
Based on rewriting logic. This makes it particularly well suited to express concurrent and state-changing aspects of systems declaratively.
-
—
Wide-spectrum. Rewriting logic is a logical and semantic framework for both specification and efficient execution.
-
—
Multiparadigm. Since rewriting logic conservatively extends equational logic, an equational style of functional programming is naturally supported in a sublanguage. A declarative style of concurrent object-oriented programming is also supported with a simple logical semantics.
-
—
Reflective. Rewriting logic is reflective [4, 1]. The design of Maude capitalizes on this fact to support a novel style of metaprogramming with very powerful module-combining and module-transforming operations that surpass those of traditional parameterized programming.
-
—
Internal Strategies. The strategies controlling the rewriting process can be defined by rewrite rules and can be reasoned about inside the logic [4, 5, 1].
Supported through Rome Laboratories contract F30602-97-C-0312, by DARPA and NASA through Contract NAS2-98073, by Office of Naval Research Contract N00014- 96-C-0114, and N00014-99-C-0198.
Chapter PDF
References
Manuel Clavel. Reflection in general logics and in rewriting logic, with applications to the Maude language. Ph.D. Thesis, University of Navarre, 1998.
Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and José Quesada. Maude: specification and programming in rewriting logic. SRI International, January 1999, http://www.maude.csl.sri.com.
Manuel Clavel, Francisco Durán, Steven Eker, and José Meseguer. Building equational proving tools by reflection in rewriting logic. In Proc. of the CafeOBJ Symposium’ 98, Numazu, Japan. CafeOBJ Project, April 1998. http://www.maude.csl.sri.com.
Manuel Clavel and José Meseguer. Reflection and strategies in rewriting logic. In J. Meseguer, editor, Proc. First Intl. Workshop on Rewriting Logic and its Applications, volume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm.
Manuel Clavel and José Meseguer. Internal strategies in a reflective logic. In B. Gramlich and H. Kirchner, editors, Proceedings of the CADE-14 Workshop on Strategies in Automated Deduction (Townsville, Australia, July 1997), pages 1–12, 1997.
Francisco Durán. A reflective module algebra with applications to the Maude language. Ph.D. Thesis, University of Malaga, 1999.
José Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96(1):730–155, 1992.
J. Siekmann and P. Szabo. A noetherian and confluent rewrite system for idempotent semigroups. Semigroup Forum, 25:83–110, 1982.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Clavel, M. et al. (2000). Using Maude. In: Maibaum, T. (eds) Fundamental Approaches to Software Engineering. FASE 2000. Lecture Notes in Computer Science, vol 1783. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46428-X_27
Download citation
DOI: https://doi.org/10.1007/3-540-46428-X_27
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67261-6
Online ISBN: 978-3-540-46428-0
eBook Packages: Springer Book Archive