Composition and Refinement of Specifications of Parameterized Data Types
Yngve Lamo, Michał Walicki · Electronic Notes in Theoretical Computer Science · 2002
In [5] we introduced a framework for specification of parameterized data types utilizing a generalization of the traditional semantics based on the pushout construction. In the present paper, we address the issue of program development using this framework with particular emphasis on the notion of refinement. Unlike for the loose specifications, refinement does not amount merely to a narrowing of the model class, but primarily to introduction of additional structure into the specified program. We give examples based on the analogues of the classical vertical and horizontal composition of such specifications.