RT Journal Article
T1 Executable Structural Operational Semantics in Maude
A1 Verdejo López, José Alberto
A1 Martí Oliet, Narciso
AB This paper describes in detail how to bridge the gap between theory and practice when implementingin Maude structural operational semantics described in rewriting logic, where transitionsbecome 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 inseveral case studies: a functional language Fpl (evaluation and computation semantics, includingan abstract machine), imperative languages WhileL (evaluation and computation semantics) andGuardL with nondeterminism (computation semantics), Kahn’s functional language Mini-ML (evaluationor 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 implementationof the Hennessy-Milner modal logic for describing local capabilities of processes, andfor 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 thismethod based on transitions as rewrites with another one based on transitions as judgements.
YR 2003
FD 2003-08
LK https://hdl.handle.net/20.500.14352/52233
UL https://hdl.handle.net/20.500.14352/52233
LA eng
DS Docta Complutense
RD 6 abr 2025