Executable Structural Operational Semantics in Maude

Alberto Verdejo and Narciso Martí-Oliet

Technical report 134-03, Dpto. Sistemas Informáticos y Programación,
Universidad Complutense de Madrid, September 2003.

Abstract: This paper describes in detail how to bridge the gap between theory and practice when implementing in Maude structural operational semantics described in rewriting logic, where transitions become rewrites and inference rules become conditional rewrite rules with rewrites in the conditions, as made possible by the new features in Maude 2.0. We validate this technique using it in several case studies: a functional language Fpl (evaluation and computation semantics, including an abstract machine), imperative languages WhileL (evaluation and computation semantics) and GuardL with nondeterminism (computation semantics), Kahn's functional language Mini-ML (evaluation or natural semantics), Milner's CCS (with strong and weak transitions), and Full LOTOS (including ACT ONE data type specifications). In addition, on top of CCS we develop an implementation of the Hennessy-Milner modal logic for describing local capabilities of processes, and for LOTOS we build an entire tool where Full LOTOS specifications can be entered and executed (without user knowledge of the underlying implementation of the semantics). We also compare this method based on transitions as rewrites with another one based on transitions as judgements.

[pdf]

@TechReport{VerdejoMarti-Oliet03,
  author =       {Alberto Verdejo and Narciso Mart{\'\i}-Oliet},
  title =        {Executable Structural Operational Semantics in {Maude}},
  institution =  {Dpto.\ Sistemas Inform\'aticos y Programaci\'on,
                  Universidad Complutense de Madrid},
  year =         2003,
  number =       {134-03},
  month =        sep
}