Implementing Modular SOS ***TALK CANCELLED***

Christiano Braga

(Universidad Complutense de Madrid )

Modular SOS (MSOS) is a formalism that allows Structural Operational Semantics specifications to be written in a modular way. In the context of the specification of programming language semantics, a modular specification intuitively means that the transition rules for a given programming language construct can be given "once and for all". An extension to a semantics specification that adds new constructs and requires new semantic entities does not imply a reformulation of the existing rules. For instance, a specification of constructs that reflects functional aspects of a programming language, such as declarations and applications, can be extended in with imperative constructs, such as assignment, without any change to the transition rules that give semantics to the functional constructs.

In this talk we report on the development of the Maude MSOS Tool (MMT), an execution environment for MSOS specifications using the Maude system, a high performance implementation of Meseguer's Rewriting Logic. MMT is implemented in Maude as a (semantics preserving) meta-function that transforms Modular SOS specifications into Maude modules thus allowing the execution and analysis of MSOS specifications using Maude's built-in tools (rewriting modulo theories, state search, and LTL model-checking) and user-defined tools, such as the strategy language interpreter.

As a non-trivial case study, we will report on an implementation of Mosses's Constructive approach to programming language semantics in MSOS, or Constructive MSOS, using MMT. The Constructive approach defines basic language constructs that capture common programming language features. Within this approach, the semantics of a programming language is defined by semantic functions that relate constructs in a given programming language to the basic constructs. MMT provides tool support for constructive programming language design using Modular MSOS as underlying semantic framework.

The MMT home page is at http://maude-msos-tool.sourceforge.net/

Thursday 2nd November 2006, 14:00
Board Room
Department of Computer Science