FORMAL SPECIFICATION OF A PERSISTENT OBJECT MANAGEMENT-SYSTEM

The goal of the research on which the paper is based was to specify fo rmally a persistent object management system and to implement a part o f the specification in the form of a prototype. The prototype is calle d the persistent object storage manager (POSM). The prototype was impl emented in C++ using the IBM OS/2 operating system. POSM is formally s pecified in the paper. The data model used in POSM is rigorously defin ed using the Z notation. The operations of POSM and its state space ar e also specified in Z notation. Example schemas for the operations of the node management component of the prototype are presented. Z notati on is justified in the paper and the benefits of using Z in the resear ch are discussed.