Toward formal development of programs from algebraic specifications: Parameterisation revisited (Q1323357)

Parameterization is an important mechanism for structuring programs and specifications into modular units. The interplay between parameterization (of programs and of specifications) and specification (of parameterized and of non-parameterized programs) is analyzed, exposing important semantic and methodological differences between specifications of parameterized programs and parameterized specifications. The extension of parameterization mechanisms to the higher-order case is considered, both for parameterized programs and parameterized specifications, and the methodological consequences of such an extension are explored. A specification formalism with parameterization of an arbitrary order is presented. Its denotational-style semantics is accompanied by an inference system for proving that an object satisfies a specification. The formalism includes the basic specification-building operations of the ASL specification language and is institution independent.