School of Computing

Guards, Preconditions, and Refinement in Z

Ralph Miarka, Eerke Boiten, and John Derrick

In Jonathan P. Bowen, Steve Dunne, Andy Galloway, and Steve King, editors, ZB2000: Formal Specification and Development in Z and B / First International Conference of B and Z Users, volume 1878 of Lecture Notes in Computer Science, pages 182-196. Springer-Verlag Berlin, August 2000.

Abstract

In the common Z specification style operations are, in general, partial relations. The domains of these partial operations are traditionally called preconditions, and there are two interpretations of the result of applying an operation outside its domain. In the traditional interpretation anything may result whereas in the alternative, guarded, interpretation the operation is blocked outside its precondition.

In fact these two interpretations can be combined, and this allows representation of both refusals and underspecification in the same model. In this paper we explore this issue, and we extend existing work in this area by allowing arbitrary predicates in the guard.

To do so we adopt a non-standard three valued interpretation of an operation by introducing a third truth value. This value corresponds to a situation where we don't care what effect the operation has, i.e.~the guard holds but we may be outside the precondition.

Using such a three valued interpretation leads to a simple and intuitive semantics for operation refinement, where refinement means reduction of undefinedness or reduction of non-determinism. We illustrate the ideas in the paper by means of a small example.



Bibtex Record

@inproceedings{1130,
author = {Ralph Miarka and Eerke Boiten and John Derrick},
title = {{Guards, Preconditions, and Refinement in Z}},
month = {August},
year = {2000},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2000/1130},
    ISBN = {3-540-6794-8},
    ISSN = {0302-9743},
    booktitle = {ZB2000: Formal Specification and Development in Z and B / First International Conference of B and Z Users},
    editor = {Jonathan P. Bowen and Steve Dunne and Andy Galloway and Steve King},
    publication_type = {inproceedings},
    publisher = {Springer-Verlag Berlin},
    refereed = {yes},
    series = {Lecture Notes in Computer Science},
    submission_id = {29246_973525433},
    volume = {1878},
}

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

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

Last Updated: 21/03/2014