From Z to BON/Eiffel

The article shows how to make a transition from the Z formal notation to the Business Object Notation (BON). It is demonstrated that BON has the expressive power of Z, with the additional advantages of object-orientation and a supporting seamless development method. The transition is illustrated for some widely used Z constructs. The translation lays the groundwork for a semi-automated tool for extracting classes from Z specifications.