A formal OO method inspired by Fusion and Object-Z

Abstract

We present a new formal OO method, called $\mathcal{F}\mathcal{O}\mathcal{X}$, 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, $\mathcal{F}\mathcal{O}\mathcal{X}$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 $\mathcal{F}\mathcal{O}\mathcal{X}$.