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. © 2008 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
McComb, T., & Smith, G. (2008). Introducing objects through refinement. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5014 LNCS, pp. 358–373). https://doi.org/10.1007/978-3-540-68237-0_25
Mendeley helps you to discover research relevant for your work.