Foundations for Structuring Behavioural Specifications

We develop foundations for structuring behavioural specifications based on the logic tradition of hidden algebra. This includes an analysis of a number of important technical compositional properties for behavioural signatures, such as pushouts, inclusions and unions, as well as an investigation of algebraic rules for behavioural module composition. As a particularity of behavioural specifications, some of the constructions and results arise in a partial algebraic form. This partiality aspect is one of the distinguishing features of our approach to behavioural specification modules. In addition, our study does not commit to any actual choice of structuring constructs, thus being applicable to a wide variety of structuring situations. 1