Formal Object Oriented Specification Using Object-Z
Published on 6. June 2000
Book
Paperback/Softback
240 pages
978-0-333-80123-9 (ISBN)
Description
This book presents techniques for the precise description of software or systems using the object-oriented formal specification language, Object-Z. 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. Although primarily intended for safety-critical or complex software development, formal specification also has wide application in hardware or general system description.
A practical and rigorous approach to object-oriented formal specification. Introduces Object-Z. Illustrates the key role of formal specification in formal verification by inclusion of example proofs of correctness.
A practical and rigorous approach to object-oriented formal specification. Introduces Object-Z. Illustrates the key role of formal specification in formal verification by inclusion of example proofs of correctness.
Reviews / Votes
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 ReliabilityMore details
Series
Edition
2000
Language
English
Place of publication
London
United Kingdom
Publishing group
Bloomsbury Publishing PLC
Target group
College/higher education
Professional and scholarly
Illustrations
240 p.
Dimensions
Height: 24.6 cm
Width: 18.9 cm
ISBN-13
978-0-333-80123-9 (9780333801239)
DOI
10.1057/9781137098344
Schweitzer Classification
Persons
ROGER DUKE and GORDON ROSE are lecturers in the Software Verification Research Centre, Department of Computer Science and Electrical Engineering at the University of Queensland.
Content
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.