Structuring Z Specifications with Views

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 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. 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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 01, 1994
Accession Number
ADA277618

Entities

People

  • Daniel Jackson

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Air Force
  • Birds
  • Classification
  • Computer Programming
  • Computer Science
  • Contrast
  • Engineering
  • Grids
  • Language
  • Personality
  • Semantics
  • Sequences
  • Software Development
  • Specifications
  • Standards
  • United States Government

Fields of Study

  • Computer science

Readers

  • Adaptive Control and Estimation with Uncertainty in Dynamic Systems.
  • Systems Analysis and Design
  • Theoretical Analysis.

Technology Areas

  • Space
  • Space - Satellites