Introduction:

In this paper we present a method for using generic components in formal specifications. This approach results in a flexible generic system description that separates the concerns of structure and data types. The generic specification can be extended and modified in a natural manner, to track requirements as they inevitably evolve during the development process. In addition, the specification can readily be specialised to use more concrete data types without the need for a formal refinement, using explicit generic instantiation. Such generic instantiation also allows operation preconditions to be strengthened ; this is not allowed by classic refinement, but it permits a separation of concerns by allowing preconditions relevant to specialised data types to be added only when they become relevant.

Here we use the Z specification language and a simple entity-relationship form as demonstration notations. No new notation or theory is presented; rather it is the use of Z's generic schemas to structure and specialise a specification that is somewhat different from the classical Z specification style described in much of the literature. We believe that this approach is also applicable to other formal methods.

@inproceedings(SS-FM99,
  author = "Fiona Polack and Susan Stepney",
  title = "Systems Development using {Z} Generics",
  pages = "1048--1067",
  crossref = "FM99"
)

@proceedings(FM99,
  title = "FM'99: World Congress on Formal Methods, Toulouse, France,
           September 1999, proceedings volume II",
  booktitle = "FM'99: World Congress on Formal Methods, Toulouse, France,
           September 1999, proceedings volume II",
  editor = "Jeannette M. Wing and Jim Woodcock and Jim Davies",
  series = "LNCS",
  volume = 1709,
  publisher = "Springer",
  year = 1999
)