Foundations of Behavioural Specification in Rewriting Logic
Răzvan Diaconescu · Electronic Notes in Theoretical Computer Science · 1996
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. 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 provide syntactic characterisations for the for the behavioural satisfaction relation, thus opening the door for shifting recent advanced proof techniques for behavioural satisfaction to rewriting logic. 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.