OBJECT EXTENSIONS TO Z: A SURVEY

Formal specification languages provide assistance to solving the problem of high maintenance costs caused by ineffective communication of a system’s requirements. Using a sound mathematical basis, a formal specification language provides a precise and definitive system description that can serve as a binding contract. Additionally, the integration of the object-oriented paradigm with a formal specification language provides increased potential for software reuse, conceptually cleaner specifications and a framework for defining interfaces. To this end, there has been significant work done to extend existing specification languages to allow object-oriented specifications. This paper provides a comparison of such object-oriented specification languages, specifically, those extending Z. The paper is organized into five major sections. After a brief introduction to the concepts of formal specification languages and Z, a simple library system is defined and used as an example throughout the paper. Each of the object-oriented specification languages is introduced and classified as either using Z in an object-oriented style or providing a true object-oriented extension of Z. For each language, the specification of the example library system is presented following a brief overview of the language’s features. An in-depth comparison is made of each of the languages which provide a true object-oriented extension of Z.