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.