School of Computing

Constructive consistency checking for partial specification in Z

E.A. Boiten, J. Derrick, H. Bowman, and M.W.A. Steen

Science of Computer Programming, 35(1):182-196, September 1999.

Abstract

This paper is a significantly extended and slightly improved version of "Consistency and refinement for partial specification in Z" which was presented at FME'96. It has been accepted for publication in Science of Computer Programming.

Contents:

  • Introduction, goals and context: partial or viewpoint specification, where and why; the need for consistency checking, unification as a constructive method.
  • Technical preliminaries: Z, states and operations, pre- and postconditions, refinement, equivalence relations, unary consistency in Z.
  • Viewpoint unification: the parameters: states and operations as viewpoint specifications; the need for correspondences between state spaces; correspondences and unified state spaces; relabelling as an alternative for correspondences; default correspondences and relabellings.
  • Viewpoint unification: the algorithm: state unification by correspondences; adaptation of operations to unified state; operation unification; the algorithm in full.
  • Proofs and consistency conditions: operation adaptation is data refinement (state consistency); operation unification is operation refinement (operation consistency); unification is least common refinement; concluding remarks on the algorithm.
  • Variations and extensions to the algorithm: state initialisation; more than 2 viewpoints; local state components; partial specification of inputs and outputs; consistency checking in a software development model.
  • Related issues and approaches: viewpoint amalgamation and co-refinement; specification by views; demonic join and feature interaction; conjunction as composition; others.
  • Future work: promotion; behavioural interpretations.

Note: WWW version of paper is as accepted, for final version see SCP sometime in 1999.

Download publication 141 kbytes

Bibtex Record

@article{607,
author = {E.A. Boiten and J. Derrick and H. Bowman and M.W.A. Steen},
title = {Constructive consistency checking for partial specification in {Z}},
month = {September},
year = {1999},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1999/607},
    journal = {Science of Computer Programming},
    number = {1},
    volume = {35},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014