It includes numerous and varied case studies to illustrate the techniques and language of object-oriented formal specification and illustrates the key role of formal specification in formal verification and in implementation.

Preface.- Specification and Object Orientation.- Graphical Presentatio of Specifications.- Local vs Central Control.- Distributed and Mediated Message Passing.- Dependency and Information Sharing.- Reliable Behaviour.- Proving Invariant Properties.- Polymorphic Inheritance Hierachies.- Class Union.- Object Containment.- Computational Systems.- Functional Abstraction.- Semantic Issues of Object-Z.- Background Notation.- Glossary of Notation.- Object-Z Concrete Syntax.- Further Reading.

This book is very firmly oriented towards the practice of formal specification, and does not present the work on theoretical foundations which underpin the language. Instead, all the features of an Object-Z specification are introduced step by step through tutorial examples, together with motivations for their use. The book also shows how the Unified Modelling Language (UML) can be used in conjunction with Object-Z, introducing notations for state and operation composition within UML class descriptions. The emphasis throughout is on the use of formal notation for precise modelling, instead of verification of refinements. This is in tune with the usual way Z is used, and the way formal methods have primarily been used in industrial pratice.' - Kevin Lano, Software Testing, Verification and Reliability

This book is very firmly oriented towards the practice of formal specification, and does not present the work on theoretical foundations which underpin the language. Instead, all the features of an Object-Z specification are introduced step by step through tutorial examples, together with motivations for their use. The book also shows how the Unified Modelling Language (UML) can be used in conjunction with Object-Z, introducing notations for state and operation composition within UML class descriptions. The emphasis throughout is on the use of formal notation for precise modelling, instead of verification of refinements. This is in tune with the usual way Z is used, and the way formal methods have primarily been used in industrial pratice.' - Kevin Lano, Software Testing, Verification and Reliability