CAVIAR: A Case Study in Specification

Abstract

This paper describes the specification, written in the specification language known as Z, of a reasonably complex software system. Important features of the Z approach which are highlighted in this paper include the interleaving of mathematical text with informal prose, the creation of parameterised specifications, and use of the Z schema calculus to construct descriptions of large systems from simpler components.