Towards a Formal Framework for Evaluation of Operational Semantics Specifications
Fabio da SilvaAbstract: This paper describes the theoretical basis of a framework for writing and executing operational semantics descriptions of various aspects of programming languages. We consider such a framework as a fundamental step towards an environment for semantic based formal program manipulation in a broader sense. The framework described here share some common characteristics with other work in semantic based evaluation, e.g. the Centaur System, and the Animator Generator. Our approach differs from these works mainly in (1) the formal characterisation of an operational semantics, and (2) the meta-langauge of semantics specification, and its evaluation model. Regarding (1), we present a notion of operational semantics in the framework of first order signatures and first order structures. Our objective is to present operational semantics specification in a form that is more amenable to formal manipulation of the kind done by semi-automatic theorem provers. As far as (2) is concerned, we define a meta-language in which only a class of deterministic specifications can be expressed. For this meta-language we define an evaluation model that describes how deterministic specifications can be evaluated. In this work we present our characterisation of operational semantics, define the meta-language, and describe its evaluation model. We then describe how another sub-class of semantics specifications, called determinate semantics, can be transformed into deterministic ones. This transformation shows how the evaluation model can be applied to a wider class of specifications without changing its complexity.
This report is not available on-line.
Previous | Index | Next