A project is being set up to write a formal specification, using the Z notation, of part of the Application Programming Interface of a large mainframe transaction processing system. The system, and its application programming interface, have been in use for many years. Two of the project staff, including the project leader, have some experience of using the notation for development, but not for this kind of after-the-event recovery of the specifications. The project has two contractors working on it, one who has worked before with the project owners on formal specification using Z, and one commercial consultant who has some experience of the Z notation. The project is expected to last about nine months, and produce about five hundred pages of specifications. The project staff have access to the manuals that describe the transaction processing system, and to the programmers currently developing the next release of the transaction processing system, many of whom have worked on the system for several years. There is little opportunity to experiment with the existing system. A Z type checker is available, but no theorem prover.
The project is justified on the grounds that the transaction processing system is about to be redeveloped for other platforms (Unix, PC, and others), and the application programming interface must be the same on the other platforms as it is on the mainframe.