Accession Number:

ADA277618

Title:

Structuring Z Specifications with Views

Descriptive Note:

Technical rept.

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

1994-03-01

Pagination or Media Count:

29.0

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 though 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 programs 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. The features of Z that make it especially well suited to composing views are discussed, along with some hints for adapting other languages to the purpose.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE