Invariants as Design Templates in Object-based Systems

S.J. Goldsack, K. Lano,

Department of Computing
Imperial College of Science, Technology and Medicine,
180 Queens Gate, London SW7 2BZ, England
Tel (+44) 171 594 8246
email sjg@doc.ic.ac.uk
email kcl@doc.ic.ac.uk

E. Dürr
Utrecht University
Dept. Computational Physics
P.O.Box 80.000
3508 TV Utrecht, The Netherlands.
fax : +31-38-4654511
email: durr@fys.ruu.nl

Abstract:

Recent work using VDM++ (see [4,5]) has shown how classes in an object-oriented language can be refined by a process of transformation of an initial class into a structure of (usually) simpler objects. The process has been nick-named ``annealing'' by analogy with the physical process which changes the crystaline structure of a material while retaining its chemical properties.

The annealing process is considered an important aspect of system development in relation to object oriented systems, especially where formal correctness is an objective. It was shown in [2] that it is a mechanism by which model splitting (see Jian Lu, 1995 [8]) may be implemented. In [4] and [7] it was applied to the development of design patterns (see for example Gamma [3]) to give them a formal basis. In this paper we pay special attention to the way in which the structure of the specified system can be derived from the logical structure of the invariant.

Keywords: Object Structures, formal methods, invariants, annealing, VDM⁺⁺, design patterns.

Workshop Goals: Advance the formal basis of design structures in component based programming. Increase awareness in the programming community of VDM⁺⁺, of structural transformations as a design approach and of the dependence of system structure on the logical structure of the invariant requirements.

The body of this paper is not available in HTML form. However, it is available in postscript and postscript for A4 paper