Sciweavers

ENTCS
2006

Prototyping SOS Meta-theory in Maude

13 years 3 months ago
Prototyping SOS Meta-theory in Maude
We present a prototype implementation of SOS meta-theory in the Maude term rewriting language. The prototype defines the basic concepts of SOS meta-theory (e.g., transition formulae, deduction rules and transition system specifications) in Maude. Besides the basic definitions, we implement methods for checking the premises of some SOS meta-theorems (e.g., GSOS congruence meta-theorem) in this framework. Furthermore, we define a generic strategy for animating programs and models for semantic specifications in our meta-language. The general goal of this line of research is to develop a general-purpose tool that assists language designers by checking useful properties about the language under definition and by providing a rapid prototyping environment for scrutinizing the actual behavior of programs according to the defined semantics. Key words: Formal Semantics, Structural Operational Semantics, Term Rewriting, Language Prototyping, Maude.
Mohammad Reza Mousavi, Michel A. Reniers
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where ENTCS
Authors Mohammad Reza Mousavi, Michel A. Reniers
Comments (0)