zbMATH — the first resource for mathematics

Maude action tool: Using reflection to map action semantics to rewriting logic. (English) Zbl 0983.68519
Rus, Teodor (ed.), Algebraic methodology and software technology. 8th international conference, AMAST 2000, Iowa City, IA, USA, May 20-27, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1816, 407-421 (2000).
Summary: 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 progmms, that is, on the action notation translation of a given program \(P\) in a language \(L\), according to \(L\)’s action semantics.
For the entire collection see [Zbl 0939.00039].

68Q55 Semantics in the theory of computing
68Q60 Specification and verification (program logics, model checking, etc.)
LOTOS; Maude