Behavioural Rewriting Logic: semantic foundations and proof theory (abstract)
We extend behavioural specification based on hidden sorts to
rewriting logic by constructing a hybrid between the two underlying
logics. This is achieved by defining a concept of behavioural
satisfaction for rewriting logic. In the case of concurrent
distributed systems, this provides behavioural abstraction for
rewriting logic not only by extending the hidden algebra concept
of behavioural equivalence from states to transitions,
but also by adding new behavioural transitions. Our
approach is semantic in that it is based on a general construction on
models, called behaviour image, which uses final models
in an essential way. However, we study some proof techniques for
rewriting logic behavioural satisfaction by extending both the
classical context induction technique and the more recent advanced
Goguen's coinduction to behavioural transitions. Finally, we also show
that the rewriting logic behavioural satisfaction obeys the so-called
``satisfaction condition'' of the theory of institutions, thus
providing support for OBJ style modularisation for this new paradigm.
full paper.
Back to CafeOBJ Home Page