A Formal OO Method Inspired by Fusion and Object-Z

We present a new formal OO method, called FOX, which is a synergetic combination of the semi-formal Fusion method and the formal specification language Object-Z. To manage complexity and to foster separation of concerns, FOX distinguishes between analysis and design. In each phase structure and behaviour specifications are developed step-by-step. The specifications may be graphical or textual. We give proof obligations to guarantee that the developed models are formally consistent and complete, and that the resulting system conforms to the original specification. By walking through a simple example – a graph editor – we illustrate the application of FOX. 1 The Need for a Formal OO Method Semi-formal OOA/D methods, such as Booch’s object-oriented design [1] or Rumbaugh’s OMT [20], are widely accepted in practice. Generally, they have a planned procedure; that is, step-by-step the software developer can approach a specific goal. This fact, combined with the support for creat...

• Type: Conference
• Year: 1997
• Where: ZUM
• Authors: Klaus Achatz, Wolfram Schulte
• Keywords: Formal Methods, Formal Oo Method, Semi-formal Ooa/d Methods, ZUM 1997