VDM and Z: A comparative case study

Abstract

The specification notations of VDM and Z are closely related. They both use model-based specification techniques and share a large part of their mathematical notation. However, the approaches taken to writing specifications differ in other, more subtle, ways. We present a comparative case study of VDM and Z for specifying database systems. John Fitzgerald and Cliff Jones in their paper entitled "Modularising the formal description of a database system" in the proceedings of VDM '90: VDM and Z (LNCS Vol. 428, Springer-Verlag) provide the basis for the comparison. We present equivalent Z specifications to the VDM specifications contained in their paper. The approach taken in writing the Z specifications is to reuse as much as possible of the Z mathematical toolkit and to build the system specification from specifications of components of the system. In their paper, Fitzgerald and Jones emphasise their modularisation facilities. While the facilities for modularisation in Z are not as powerful, they are adequate for the specification of the database systems presented. © 1992 BCS.