Introducing Objects through Refinement

We present a strategy for using the existing theory of class refinement in Object-Z to introduce an arbitrary number of object instances into a specification. Since class refinement applies only to a single class, the key part of the strategy is the use of references to objects of the class being refined. Once object instances have been introduced through local class refinements in this way, they can be turned into foreign class instantiations through the application of straight-forward equivalence preserving transformations. We introduce a set of logical classifiers to allow for the precise determination of which parts of the specification logic must be moved into the foreign class.