On Refinement in Rewriting Logic.
Dorel Lucanu, Nicolae Surpatanu · 1996
Rewriting logic [Mes92] is a logic of action, whose models are concurrent systems and whose deduction is concurrent computation. Refinement is the process of moving from one specification to another, more concrete, specification which displays the same behaviour. In this paper we investigate what this process is when we deal with rewrite specifications. 1 Introduction Rewriting logic (RWL) [Mes92, Mes93, MFW92] differs from the standard logics, as first- or higher-order logics, by the fact that it is a logic of change whose models are concurrent systems, and whose deduction is concurrent computation in such systems. A concurrent system - as model of the rewriting logic - is formalized as a category with algebraic structure whose objects are states of the system and whose morphisms are transitions in the system. In [Mes92] it is shown that diverse models of concurrency can be expressed and unified within rewriting logic. Following [MG96, GM97], refinement is the process of moving from ...