Formal methods in object oriented analysis

This paper addresses the need for more precise ways of specifying behavioural requirements for software. A new approach is proposed for writing object oriented specifications. This approach uses object oriented analysis to produce a framework for writing a specification in an object oriented version of the formal specification language Z. It is argued that resulting specifications will be more precise, easier to understand and more easily reasoned about mathematically, providing a more reliable baseline for design, testing and verification than those provided by object oriented analysis, Z or English on their own. Finally this work is discussed within the context of telephone service specification.