Structuring Z Specifications with Views

Author: Daniel Jackson

Technical Report CMU-CS-94-126R.

Abstract

A view is a partial specification of a program, consisting of a state space and a set of operations. A full specification is obtained by composing several views, linking them through their states (by asserting invariants across views) and through their operations (by defining external operations as combinations of operations from different views).

By encouraging multiple representations of the program's state, view structuring lends clarity and terseness to the specification of operations. And by separating different aspects of functionality, it brings modularity at the grossest level of organization, so that specifications can accommodate change more gracefully.

View structuring in Z is demonstrated with a few small examples. Both the features of Z that lend themselves to view structuring, and those that are a hindrance, are discussed examples. Both the features of Z that lend themselves to view structuring, and those that are a hindrance, are discussed.