Modular Rewriting Semantics of Programming Languages

José Meseguer and Christiano O. Braga

We present a general method to achieve modularity of semantic denitions of programming languages specied as rewrite theories. This provides both a modular alternative to SOS definitions - with good executability and formal analysis capabilities - and a systematic way to execute and analyze SOS denitions by translation. The relationship to Mosses' modular operational semantics (MSOS) is explored in detail, yielding a semantics-preserving translation that supports execution and formal analysis of MSOS specications in Maude.

(BibTeX entry)    (gzip'ed Postscript)   

back   home   Formal Methods and Declarative Languages Laboratory   Computer Science Laboratory, SRI International