Integrating object-oriented requirements specifications with formal notations

We propose an integration of an extension of Bailin´s object-oriented requirements specification (OOS) (1989) with a formal notation (Z), called OOSZ. The OOS is used to guide the derivation of Z specifications. In OOSZ a function process is converted into an operation schema. An entity process is manifested through a state schema, an instance creation operation schema and an abstract operation schema. Correctness conjectures are generated for verifying the consistency of intralevel and interlevel specifications. These are illustrated using the problem domain of Auto Banking Systems. The bringing together of diagrammatical and text elements of OOS specifications in Z notations offers three major benefits. First, the relationship, between ERD and EDFD is tightly coupled compared with Yourdon´s SA approach. Second, OOS specifications can be seen both as a structuring mechanism that helps in deriving Z specifications, and as a preliminary that assists in ascertaining the clients requirements. Third, Z specifications make it easier to identify omissions or errors