![]() |
| ||
7 Generic SpecificationsMichel Bidoit1 and Peter D. Mosses2 1 Laboratoire Spécification et Vérification, CNRS UMR 8643 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 lncs@springer.de
|