An object-oriented approach to formal specification
Graeme Smith · The University of Queensland · 1992
Formal methods for software development are becoming increasingly necessary as software becomes an important part of everyday life. To handle the complexities inherent in largescale software systems these methods need to be combined with a sound development methodology which supports modularity and reusability. Object orientation, based on the concept that systems are composed of collections of interacting objects whose behaviours are specified by classes, is such a methodology. This thesis presents the formal specification language Object-Z which is an extension of the formal specification language Z to facilitate specification in an object-oriented style. The major extension in Object-Z is the introduction of the class schema which captures the object-oriented notion of a class by encapsulating a single state schema with all the operation schemas which may affect its variables. The class schema is not simply a syntactic extension but also defines a type whose instances are objects. O...