Toward formal development of programs from algebraic specifications: Parameterisation revisited

General topics in the theory of software (68N01) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Review text

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.

Recommendations

Cites work

Cited in

(34)

Describes a project that uses

Uses Software

This page was built for publication: Toward formal development of programs from algebraic specifications: Parameterisation revisited

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1323357)