Springer
CD-ROM OverviewTable of ContentsSearch

7  Generic Specifications

Michel Bidoit1 and Peter D. Mosses2

1 Laboratoire Spécification et Vérification, CNRS UMR 8643
École Normale Supérieure de Cachan
61, Avenue du Président Wilson, 94235 Cachan Cedex, France
bidoit@lsv.ens-cachan.fr

2 University of Aarhus, BRICS and Department of Computer Science
Aabogade 34, 8200 Aarhus N, Denmark
pdmosses@brics.dk

Abstract. Making a specification generic (when appropriate) improves its reusability.

As mentioned in the previous chapter, naming specifications is a good idea. In many cases, however, datatypes are naturally generic, having sorts, operations, and/or predicates that are deliberately left loosely specified, to be determined when the datatype is used. For instance, datatypes of lists and sets are generic regarding the sort of elements. Generic specifications allow the genericity of a datatype to be made explicit by declaring parameters when the specification is named: in the case of lists and sets, there is a single parameter that simply declares the sort Elem1 . A fitting argument specification has to be provided for each parameter of a generic specification whenever it is referenced; this is called instantiation of the generic specification.

The aim of this chapter is to discuss and illustrate how to define generic specifications and instantiate them. We have seen plenty of simple examples of generic specifications and instantiations in the previous chapters. In more complicated cases, however, explicit fitting symbol maps may be required to determine the exact relationship between parameters and arguments in instantiations, and so-called imports should be separated from the bodies of generic specifications.

1 Generic specifications are also useful to ensure loose coupling between several named specifications, replacing an explicit extension by a parameter including only the necessary symbols and their required properties. This is illustrated in the Steam-Boiler Control System case study, see Chap. 13.

LNCS 2900, pp. 77 - 92

Full article in PDF


lncs@springer.de
© Springer-Verlag Berlin Heidelberg 2004