Maude Action Tool: Using Reflection to Map Action Semantics to Rewriting Logic

  • Christiano de O. Braga
  • E. Hermann Haeusler
  • José Meseguer
  • Peter D. Mosses
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1816)


Action semantics (AS) is a framework for specifying the semantics of programming languages, in a very modular and readable way. Recently, the operational semantics of action notation (action semantics’s specification language) has been rewritten using Modular SOS (MSOS), a new modular approach for specifying operational semantics. The new modular specification of action notation facilitates the creation of extensions to action semantics, to deal with new concepts, such as components. The Maude Action Tool uses the reflective capabilities of rewriting logic, implemented on the Maude system, to create an executable environment for action semantics and its potential extensions. This is achieved by a mapping between the MSOS and rewriting logic formalisms which, when applied to the MSOS semantics of each facet of action notation, yields a corresponding rewrite theory. Such rewrite theories are executed on action programs, that is, on the action notation translation of a given program P in a language L, according to L’s action semantics.


Equational Theory Operational Semantic Label Category Label Transition System Semantic Structure 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    D. Brown, H. Moura, and D. A. Watt. Actress: an action semantics directed compiler generator. In CC’92, Proc. 4th Int. Conf. on Compiler Construction, Paderborn, volume 641 of LNCS, pages 95–109. Springer-Verlag, 1992.Google Scholar
  2. 2.
    M. Clavel. Reflection in General Logics and in Rewriting Logic. PhD thesis, Univesity of Navarre, 1998.Google Scholar
  3. 3.
    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,, January 1999.
  4. 4.
    M. Clavel, F. Durán, S. Eker, and J. Meseguer. Building equational proving tools by reflection in rewriting logic. In Proceedings of the CafeOBJ Symposium’ 98, Sumazu, Japan. CafeOBJ Project, April 1998.Google Scholar
  5. 5.
    L. C. de Sousa Menezes and H. P. de Moura. The Abaco system an algebraic based action compiler. In A. Haeberer, editor, AMAST’98, Proc. 7th Intl. Conf. on Algebraic Methodology and Software Technology, Amazonia, Brazil, volume 1548 of LNCS, pages 527–529. Springer, 1999.Google Scholar
  6. 6.
    G. Denker, J. Meseguer, and C. Talcott. Formal specification and analysis of active networks and communication protocols: The Maude experience. In DISCEX 2000, Proc. Darpa Information Survivability Conference and Exposition, Hilton Head, South Carolina, volume 1, pages 251–265. IEEE Computer Society Press, January 2000.CrossRefGoogle Scholar
  7. 7.
    F. Durán. A Reflective Module Algebra with Applications to the Maude Language. PhD thesis, Universidad de Málaga, Escuela Técnica Superior de Ingeniería Informática, 1999.Google Scholar
  8. 8.
    J. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, and J.-P. Jouannaud. Introducing OBJ. Technical Report SRI-CSL-92-03, SRI International, Computer Science Laboratory, 1992. To appear in J.A. Goguen and G.R. Malcolm, editors, Applications of Algebraic Specification Using OBJ, Kluwer, 2000.Google Scholar
  9. 9.
    R. Ibrahim and C. Szyperski. Formalization of component object model (COM)-the COMEL language. In ECOOP’98 PhD Workshop, July 1998.Google Scholar
  10. 10.
    N. Martí-Oliet and J. Meseguer. Rewriting logic as a logical and semantic framework. Technical Report SRI-CSL-93-05, SRI International, August 1993.Google Scholar
  11. 11.
    P. D. Mosses. Action Semantics. Cambridge University Press, 1992.Google Scholar
  12. 12.
    P. D. Mosses. Theory and practice of action semantics. In MFCS’96, Proc. 21st Int. Symp. on Mathematical Foundations of Computer Science, Cracow, Poland, volume 1113 of LNCS, pages 37–61. Springer-Verlag, 1996.Google Scholar
  13. 13.
    P. D. Mosses. Foundations of Modular SOS (extended abstract). In MFCS’99, Proc. 24th Intl. Symp. on Mathematical Foundations of Computer Science, Szklarska-Poreba, Poland, volume 1672 of LNCS, pages 70–80. Springer-Verlag, 1999. The full version appears as Tech. Report RS-99-54, BRICS, Dept. of Computer Science, Univ. of Aarhus.Google Scholar
  14. 14.
    P. D. Mosses. A modular SOS for Action Notation. Research Series BRICS-RS-99-56, BRICS, Dept. of Computer Science, Univ. of Aarhus, 1999.Google Scholar
  15. 15.
    H. Moura and D. A. Watt. Action transformations in the Actress compiler generator. In CC’94, Proc. 5th Intl. Conf. on Compiler Construction, Edinburgh, volume 786 of LNCS, pages 16–30. Springer-Verlag, 1994.Google Scholar
  16. 16.
    M. A. Musicante and P. D. Mosses. Communicative action notation with shared storage. Tech. Mono PB-452, Dept. of Computer Science, Univ. of Aarhus, 1993.Google Scholar
  17. 17.
    Object Management Group. The Common Object Request Broker Architecture and Specification-Revision 2.0, July 1995.
  18. 18.
    P. Ørbæk. OASIS: An optimizing action-based compiler generator. In CC’94, Proc. 5th Intl. Conf. on Compiler Construction, Edinburgh, volume 786 of LNCS, pages 1–15. Springer-Verlag, 1994.Google Scholar
  19. 19.
    J. Penix and P. Alexander. Toward automated component adaptation. In Ninth International Conference on Software Engineering and Knowledge Engineering (SEKE), June 1997.
  20. 20.
    G. D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.Google Scholar
  21. 21.
    A. van Deursen and P. D. Mosses. ASD: The action semantic description tools. In AMAST’96, Proc. 5th Intl. Conf. on Algebraic Methodology and Software Technology, volume 1101 of LNCS, pages 579–582. Springer-Verlag, 1996.CrossRefGoogle Scholar
  22. 22.
    K. Wansbrough and J. Hamer. A modular monadic action semantics. In Conference on Domain Specific Languages, pages 157–170. The USENIX Association, 1997.

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Christiano de O. Braga
    • 1
    • 2
  • E. Hermann Haeusler
    • 2
  • José Meseguer
    • 1
  • Peter D. Mosses
    • 3
  1. 1.Computer Science LaboratorySRI InternationalUSA
  2. 2.Departamento de InformáticaPontifícia Universidade Católica do Rio de JaneiroRio de Janeiro
  3. 3.BRICS & Department of Computer ScienceUniversity of AarhusAarhus

Personalised recommendations