Specification of parameterized programs - persistency revisited

摘要

We revisit the concept of persistent functor pointing out its well known limitations for the purpose of describing the semantics of specifications of parameterized data types (PDTs). We introduce a more general notion of a semantic functor F which requires only that the parameter algebra A is a subalgebra of its image F(A). We illustrate the flexibility and advantages of the proposed construction by examples. The main part of the paper concerns the syntactic restrictions on the specifications which allow one to define the semantics of PDTs in this way. One obtains the possibilities to: 1) preserve the carriers of the parameter algebras (corresponding to the classical persistency), or 2) extending carriers of the parameter algebras. The later situation means that one can, typically, use free functor semantics. In this case, one also has two further options: either 2a) to restrict the validity of the axioms from the parameter specification to apply only to the old elements (from the carriers of the parameter algebras), or 2b) to extend them to apply also to the new elements added to the carrier. We discuss the mechanism of actual parameter passing, actualization of the semantic functors and refer to an earlier work for the counterparts of the vertical and horisontal composition theorems, as well as the notion of refinement of PDTs which amounts to the refinement of the structure of the specified data type.