Algebraic theory of parameterized specifications with requirements

Abstract

Parameterized specifications of abstract data type are studied within the theory of algebraic specifications. In the algebraic theory as introduced by the ADJ-group a parameterized specification, like set (data), consists of a parameter declaration data and a target specification set (data). This basic algebraic approach is combined with a very general notion of requirements which have to be satisfied for the parameters of the specification. Especially we can use fixed basic types like bool or nat in the parameter part, a feature which is already included in the algebraic specification language CLEAR. This allows to specify bounded types like bounded natural numbers nat (bound) with variable bound or bounded arrays. Moreover the requirement feature allows to use arbitrary predicate formulas which are also used in logical requirement specifications for software systems. In spite of this generality the theory developed for the basic algebraic approach can be fully extended to the case with requirements. The basic result is an extension lemma which allows to show correctness of parameter passing and associativity of nested parameterized specifications like set (stack (nat)). Correctness of such composite specifications is automatically induced by correctness of the parts. This theory with requirements is still based on initial algebra semantics but with slight modifications it can also be used for final algebraic semantics.