On Generic Specifications

by Michel Bidoit

1 November 1996

It will be made available formatted for printing as compressed Postscript and DVI.

The WWW version provides only a rough approximation (mostly generated automatically by Hyperlatex) to the symbols used in the formatted versions. Please inform pdmosses@brics.dk about any places where a better approximation could be made!

N.B. All Study Notes are TENTATIVE first versions, unless explicitly marked otherwise.

Abstract

The following is an attempt to clarify how to integrate generic (parametrized) specifications in the X CoFI specification language. We take for granted that generic specifications are useful (as a means for structuring specification texts and for reusing them) and that they should not be confused with "architectural specifications".

(Sketch of) Examples are given in a hopefully suggestive but otherwise quite arbitrary concrete syntax. An attempt is made to provide a corresponding abstract syntax.

• All structured specification definitions are generic (parametrized) w.r.t. a (possibly empty) list of parameter specifications (uniformity).
• Parameter specifications can be named or not (referential transparency).
• Any specification can be turned into a parameter specification. There is no distinction between three classes of structured specifications (ordinary, generic, parameter) as in the previous proposal (homogeneity).
• Compound sorts are monotonic w.r.t. subsorting.
• More justifications are provided for the need of a "fixed" part in parameter specifications, and a new mechanism for achieving this is described.
• The abstract syntax has been revised accordingly, and well-formedness conditions are described precisely.