Abstract
Modular SOS (MSOS) is a framework created to improve the modularity of structural operational semantics specifications, a formalism frequently used in the fields of programming languages semantics and process algebras. With the objective of defining formal tools to support the execution and verification of MSOS specifications, we have defined a mapping, named \( \mathcal{M}{\mathbf{ }}to{\mathbf{ }}\mathcal{R} \) , from MSOS to rewriting logic (RWL), a logic which has been proposed as a logical and semantic framework. We have proven the correctness of \( \mathcal{M}{\mathbf{ }}to{\mathbf{ }}\mathcal{R} \) and implemented it as a prototype, the MSOS-SL Interpreter, in the Maude system, a high-performance implementation of RWL. In this paper we characterize the \( \mathcal{M}{\mathbf{ }}to{\mathbf{ }}\mathcal{R} \) mapping and the MSOS-SL Interpreter.
The reader is assumed to have some basic knowledge of structural operational semantics and object-oriented concepts.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
M. Clavel. Reflection in rewriting logic: metalogical foundations and metaprogramming applications. CSLI Publications, 2000.
M. Clavel, F. Durán, S. Eker, N. Martí-Oliet, P. Lincoln, J. Meseguer, and J. Quesada. Maude: Specification and Programming in Rewriting Logic. SRI International, http://maude.csl.sri.com, January 1999.
M. Clavel and J. Meseguer. Reflection in conditional rewriting logic. Theoretical Computer Science, 285(2):245–288, August 2002.
C. de O. Braga. Rewriting Logic as a Semantic Framework for Modular Structural Operational Semantics. PhD thesis, Pontifícia Universidade Católica do Rio de Janeiro, September 2001. http://www.ic.uff.br/~cbraga.
C. de O. Braga, E. H. Haeusler, J. Meseguer, and P. D. Mosses. Maude action tool: Using reflection to map action semantics to rewriting logic. In AMAST’00, Proc. 8th Intl. Conf. on Algebraic Methodology and Software Technology, Iowa City, IA, USA, volume 1816 of Lecture Notes in Computer Science, pages 407–421. Springer, May 2000.
F. Durán. A Reflective Module Algebra with Applications to the Maude Language. PhD thesis, Universidad de Mlaga, Escuela Tcnica Superior de Ingeniera Informtica, 1999.
N. Martí-Oliet and J. Meseguer. Handbook of Philosophical Logic, volume 61, chapter Rewriting Logic as a Logical and Semantic Framework. Kluwer Academic Publishers, second edition, 2001. http://maude.csl.sri.com/papers.
J. Meseguer. A logical theory of concurrent objects. In N. Meyrowitz, editor, Proceedings ECOOP-OOPSLA’90 Conference on Object-Oriented Programming, Ottawa, Canada, October 1990, pages 101–115. ACM Press, 1990.
J. Meseguer. Conditional rewriting as a unified model of concurrency. Theoretical Computer Science, 96(1):73–155, April 1992.
R. Milner. Communication and Concurrency. Prentice-Hall International Series in Computer Science. Prentice-Hall International, 1989.
P. D. Mosses. Action Semantics. Cambridge University Press, 1992.
P. D. Mosses. A Modular SOS for ML concurrency primitives. Technical Report Research Series RS-99-57, BRICS, Dept. of Computer Science, Univ. of Aarhus, 1999.
P. D. Mosses. Pragmatics of Modular SOS. In H. Kirchner and C. Ringeissen, editors, Algebraic Methodology and Software Technology, 9th International Conference, AMAST 2002, Saint-Gilles-les-Bains, Reunion Island, France, September 9–13, 2002, Proceedings, volume 2422 of Lecture Notes in Computer Science, pages 21–40. Springer, 2002.
G. D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Braga, C.O., Hæusler, E.H., Meseguer, J., Mosses, P.D. (2003). Mapping Modular SOS to Rewriting Logic. In: Leuschel, M. (eds) Logic Based Program Synthesis and Transformation. LOPSTR 2002. Lecture Notes in Computer Science, vol 2664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45013-0_21
Download citation
DOI: https://doi.org/10.1007/3-540-45013-0_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40438-5
Online ISBN: 978-3-540-45013-9
eBook Packages: Springer Book Archive