Rewriting Logic as a Semantic Framework for Modular Structural Operational Semantics

Christiano de Oliveira Braga

Abstract

The abstraction level provided by programming languages constructs in the past decade has increased substantially. We moved from low level machine programming in card processing systems to executable mathematical specifications using functions, logic specifications with inference rules, or algebraic speci-fications with abstract datatypes, all running on laptops. The motto is becoming more and more "what" instead of "how".

A byproduct of this technology evolution is the transformation technology which moved from assembly to machine level code compilation towards high-level specification processing. This is accomplished by transformations from that high level language to another language following a refinement process, that is, a process that preserves semantic properties from the source language into the target language, in a potential network of transformations.

Among the high level frameworks that relate to the above mentioned process, are actions semantics (AS), modular structural operational semantics (MSOS), and rewriting logic (RWL). AS is a framework for specifying the semantics of programming languages in a very readable way without loosing its mathe-matical precision. MSOS is an extension to the structural operational semantics framework, that manages the pragmatic issue of modularity in a simple and elegant way. RWL is a generic framework to which many logics and specification languages have been mapped to.

This thesis applies state-of-the art transformation technology to the scope of semantic-driven generation of programming languages interpreters. The main contribution of this work is a proven correct mapping from MSOS to RWLand the MSOS-SL Interpreter, an implementation of an interpreter for MSOS specifications. As a case study for the MSOS-SL Interpreter, we have implemented the Maude Action Tool (MAT), an executable environment for AS using the MSOS specification of action notation.

We have coded our tools in Maude, an efficient implementation for rewriting logic, with a fairly inten-sive use of its meta-programming capabilities.

(BibTeX entry)    (gzip'ed Postscript)   


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