School of Computing

Coupling schemas: data refinement and view(point) composition

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

In D.J. Duke and A.S. Evans, editors, 2nd BCS-FACS Northern Formal Methods Workshop, Workshops in Computing, pages 182-196. Springer-Verlag, July 1997.


We define the notion of a coupling schema in Z, and describe the role it plays in data refinement, view composition, and viewpoint unification. In each case coupling schemas relate several state schemas. In data refinement they occur as retrieve relations (abstraction schemas). In specification by views, coupling schemas provide a link between the various views. For viewpoint specification, coupling schemas are closely related to correspondence relations between state schemas in the viewpoints. Simple properties of coupling schemas (e.g. totality, functionality, and consistency) are shown to have important consequences in the techniques listed, and to be very useful for exhibiting the relations between these techniques. It turns out that views and viewpoints can both be seen as variations on, or even as generalisations of, data refinement.


Paper on BCS website.

Bibtex Record

author = {E.A. Boiten and J. Derrick and H. Bowman and M. Steen},
title = {Coupling schemas: data refinement and view(point) 	 composition},
month = {July},
year = {1997},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {},
    ISBN = {3-540-76215-9},
    booktitle = {2nd BCS-FACS Northern Formal Methods Workshop},
    editor = {D.J. Duke and A.S. Evans},
    publisher = {Springer-Verlag},
    refereed = {yes},
    series = {Workshops in Computing},

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

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

Last Updated: 21/03/2014