School of Computing

Loose specification and refinement in Z

Eerke Boiten

In D. Bert, J.P. Bowen, M.C. Henson, and K. Robinson, editors, ZB 2002: Formal Specification and Development in Z and B, volume 2272 of Lecture Notes in Computer Science, pages 182-196, Grenoble, France, January 2002. Springer.

Abstract

Z is a specification notation with a model-based semantics, but in contrast to most such languages, its normal refinement relation is not defined in terms of model containment. This paper investigates this phenomenon, leading to a variety of observations concerning the relation between Z semantics and refinement.

Bibtex Record

@conference{1335,
author = {Eerke Boiten},
title = {Loose Specification and Refinement in {Z}},
month = {January},
year = {2002},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2002/1335},
    publication_type = {conference},
    submission_id = {3176_1012303677},
    ISBN = {3-540-43166-7},
    booktitle = {ZB 2002: Formal Specification and Development in Z and B},
    editor = {D. Bert and J.P. Bowen and M.C. Henson and K. Robinson},
    volume = {2272},
    series = {Lecture Notes in Computer Science},
    address = {Grenoble, France},
    publisher = {Springer},
    ISSN = {0302-9743},
    refereed = {yes},
}

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

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

Last Updated: 21/03/2014