Modular Context-Sensitive Algebraic Specifications

Authors

Bernhard Gramlich and Salvador Lucas

Abstract

Context-sensitivity in algebraic specifications is an interesting approach for bridging the gap between the purely logical and semantic nature of such systems and (certain problems in) their operational realization and implementation. Context-sensitive algebraic specifications can be seen as ordinary algebraic specifications, enriched by additional syntatical (context) information that turns out to be very useful in transforming these specifications into executable prototypes or implementations satisfying usually desired properties (like termination and uniqueness of results). Here we investigate modular aspects of such context-sensitive algebraic specifications and computations in the framework of context-sensitive equational reasoning and rewriting. In particular, we study the modularity behaviour of context-sensitive term rewriting systems w.r.t. confluence and related uniqueness properties. We show how to extend various modularity results known from (unrestricted) term rewriting systems to this more general setting, and how to cope with the additional complications caused by context-sensitivity.