Vertical Z

In this paper, lessons learned about decomposition in programming are used as the basis for the organisation of a Z specification. The example used is drawn from an information system which manages security for a large company. The part of the specification shown here illustrates the use of cards to permit access to secure rooms in the company building. We will refer to this part of the specification as the Door Control System.