Home page
We have been exploring the features of rewriting logic and the language
Maude
as an executable semantic framework for the representation and implementation
of different kinds of operational semantics.
In this page we enumerate our works and include the Maude code of the implementations.
| Abstract | We explore the features of rewriting logic and, in particular, of the rewriting logic language Maude as a logical and semantic framework for representing both the semantics of CCS and a modal logic for describing local capabilities of CCS processes. Although a rewriting logic representation of the CCS semantics was given previously, it cannot be directly executed in the current default interpreter of Maude. Moreover, it cannot be used to answer questions such as which are the successors of a process after performing an action, which is used to define the semantics of Hennessy-Milner modal logic. Basically, the problems are the existence of new variables in the righthand side of the rewrite rules and the nondeterministic application of the semantic rules, inherent to CCS. We show how these problems can be solved by exploiting the reflective properties of rewriting logic, which allow controlling the rewriting process. We also show how the semantics can be extended to traces of actions and to the CCS weak transition relation. This executable specification plus the reflective control of the rewriting process can be used to analyze CCS processes. |
| Postscript file | ccs-jdgm.ps |
| Maude code | ccs-jdgm.fm, tests.fm |
| Isabelle code | CCS-Isabelle.thy |
| Abstract | This paper describes in detail how to bridge the gap between theory and practice in a new implementation of the CCS operational semantics in Maude, 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 implement both the usual transition semantics and the weak transition semantics where internal actions are not observed, and on top of them we also implement the Hennessy-Milner modal logic for describing processes. We compare this implementation with a previous one where transitions become judgements and inference rules become rewrites and also comment on extensions to the LOTOS language. |
| Postscript file | ccs-rc.ps |
| Maude 2.0 code | ccs-rc.maude |
| Abstract | We describe a formal tool based on a symbolic semantics for Full LOTOS, where specifications without restrictions in their data types can be executed. The reflective feature of rewriting logic and the metalanguage capabilities of Maude make it possible to implement the whole tool in the same semantic framework, and have allowed us to implement the LOTOS operational semantics, to integrate it with ACT ONE specifications, and to build an entire environment with parsing, pretty printing, and input/output processing of LOTOS specifications. Our aim has been to implement a formal tool that can be used by everyone without knowledge of the concrete implementation, but where the semantics representation is at so high level that can be understood and modified by everyone that knows about operational semantics. |
| Postscript file | lotos-rc.ps |
| Maude 2.0 code | lotos-rc.maude (with comments) |
| Abstract | Following the approach for implementing structural operational semantics where transitions become rewrites and inference rules become conditional rewrite rules, we have implemented the different semantics presented by M. Hennessy in his book "The semantics of programming languages: an elementary introduction using structural operational semantics". |
| Postscript file | (In preparation.) |
| Maude 2.0 code | fpl-evaluation.maude, fpl-computation.maude, fpl-abstract-machine.maude, whileL-evaluation.maude, whileL-computation.maude, guardL.maude |
We would appreciate any comment (alberto @ sip . ucm . es).
Thanks.