Computing and Informatics, Vol. 00, 0000, 0–32, V 2003Jun16
Z LOGIC AND ITS CONSEQUENCES
Martin C. Henson
Department of Computer Science, University of Essex, U.K
Steve Reeves
Department of Computer Science, University of Waikato, N.Z.
Jonathan P. Bowen
Centre for Applied Formal Methods, London South Bank University, U.K.
Abstract.
This paper provides an introduction to the speciﬁcation language Z froma logical perspective. The possibility of presenting Z in this way is a consequence of a number of joint publications on Z logic that Henson and Reeves have cowrittensince 1997. We provide an informal as well as formal introduction to Z logic andshow how it may be used, and extended, to investigate issues such as equationallogic, the logic of preconditions, the issue of monotonicity and both operation anddata reﬁnement.For Peter Wexler –
in memoriam
1 INTRODUCTION
This paper describes an approach to Z
logic
– it is relatively unconcerned withZ
semantics
, except insofar as the existence of a nontrivial model is useful forestablishing the consistency of the logic. The paper neither attempts to replicate,nor to extend, the excellent work on Z standardisation which has led to ISO standard
Z Logic and its Consequences
113568.
1
It is, rather, complementary, seeking to explore and express the logicalpreliminaries of Z
2
and aiming to describe those uncontroversial properties of themajor elements of the language, in particular, the language of
schemas
and its
calculus
.The approach to Z logic taken here is mainly based on three papers [17, 18, 19];these remain the comprehensive technical resource for two separate though relatedapproaches (we make some reference to the distinction in section 3.5). Our objectivein this paper is to provide a more accessible overview of that work and to highlightsome more advanced related work beyond speciﬁcation, in particular in the theoryof reﬁnement, that becomes possible by virtue of the Z logic that we describe.The paper is structured in three parts. The ﬁrst is the least formal and mostaccessible: it explores initial considerations concerning the formalisation of vernacular
3
Z with particular reference to the novel features (those that take Z beyond, atleast in expressivity, higherorder logic) concerning
schema types
and
bindings
. Thesecond part of the paper is a more formally presented account of Z logic (the logic
Z
C
) and how that may be extended by means of a series of conservative extensionsto more comprehensive logical systems with wider coverage. We are by no meansencyclopædic and the earlier papers referred to above contain more detail and amore formal account. The ﬁnal part of the paper contains the most advanced material: it looks beyond Z as a speciﬁcation language and
Z
C
as a logic for reasoningabout speciﬁcation. It demonstrates the further utility of such a logic by showinghow various theories of equality, operation and data reﬁnement can be integratedwith, and issues such as monotonicity explored within, the base logic in a smoothand systematic manner: something made possible with a logic in place. This surveyrelies on the reader’s previous general knowledge of the topics it brieﬂy surveys.The paper ends with some concluding remarks, our acknowledgements and relevantreferences to the literature.
2 INITIAL CONSIDERATIONS
We take it as selfevident that any formal speciﬁcation should permit precise consequences to be drawn: the emphasis in the term
formal method
should fall on thesecond word and not the ﬁrst. A language, even one with a semantics, is impoverished if there is no logic: it would provide no means for drawing those consequencesin a methodical, reproducible and agreed fashion. In this ﬁrst part of the paper we
1
The Z Standard does not provide a logic. The strategic decision to exclude a logicwas reported in [22]. An inconsistency [16] was discovered in the (unﬁnished) draft logicsubmitted as part of the ISO Committee Draft 1.2 of the Z Standard in 1995.
2
Although beginning from its logical ﬁrst principles, this paper does not begin Z itself from ﬁrst principles. The reader is assumed to be familiar with Z notation and conceptsas described in one of the better textbooks, for example, [33].
3
By
vernacular
Z we refer to Z as it has been used in practice and as it is reported ininformal and semiformal accounts in the literature.
2
M. C. Henson, S. Reeves, J. P. Bowen
reintroduce the key features of speciﬁcation in Z from a logical perspective. Ourobjective is to motivate and introduce the basic principles of the logic
Z
C
and toexplain why this core logic is a satisfactory basis for establishing logical apparatusfor a range of Z concepts.
2.1 Z schemas and bindings
At the heart of Z is the
schema
. Schemas are usually used in two ways: for describingthe
state space
of a system and for describing
operations
which the system mayperform.
Example 1.
Informal state space: a jug of capacity 250ml of water having a currentvolume and a current temperature. As a schema:
Jug volume
:
N
temp
:
N
volume
≤
250
temp
≤
100Written in linear form this would be:
Jug
= [
volume
:
N
;
temp
:
N

volume
≤
250
∧
temp
≤
100]This schema has the name
Jug
and introduces two
observations
,
volume
and
temp
,which have some natural number value (
i.e.
drawn from the set
N
) in each systemstate.
4
The states which comprise a schema are called
bindings
, each binding belonging to a schema is a legitimate state of the system. In this example the bindingsassociate values (of the correct type) to the observations named
volume
and
temp
.We use the word “observation” and
never
call them “variables”. If one pursuesthe “schemas as sets of bindings” interpretation (which has been quite standard)then these are constants, not variables. Most informal accounts run into immediatediﬃculty in this area
5
.We will write bindings like this:
6

volume
⇛
n
,
temp
⇛
m

4
Note that the schema describes a
state space
, that is, a set of legitimate system states.This is worth stressing because some informal accounts give a mixed message, sometimessuggesting that a schema describes a
particular
state.
5
See for example [33]. In chapter 11, page 149, they are “variables”; by page 154 theyare “components” (constants).
6
ISO Z uses == rather than
⇛
, a notation which dates back to [28] and [29].
Z Logic and its Consequences
3where, in this case,
n
∈
N
etc.
Naturally, it
should
follow that, for example:

volume
⇛
100
,
temp
⇛
20
 ∈
Jug
and also:

volume
⇛
100
,
temp
⇛
200
 ∈
Jug
It is possible to extract the values associated with observations from bindings. Thisis called
binding selection
. For example, we should be able to show:

volume
⇛
100
,
temp
⇛
20

.
volume
= 100In order to capture these ideas we begin by introducing the idea of a
schema type
:
[
···
z
T
i
i
···
]
This is an unordered sequence of typed (indicated by superscripts) observations (the
z
i
). Then
schemas
are either
schema sets
:
[
···
z
i
:
C
P
T
i
i
···
]
or they are
atomic schemas
:
[
S

P
]
where the
C
i
are sets,
S
is a schema and
P
is a predicate.Of particular note are the
carrier sets
of the various types. These are formedby closing:
N
=
df
{
z
N

true
}
under the cartesian product, power type and schema type operations.
7
No ambiguity results from the overloading of the symbol
N
here: types appearonly as superscripts – all other uses denote the carrier set.We have remarked that schemas are
sets of bindings
. So the logic of schemascan be obtained from the logic of sets and bindings. In
Z
C
, for sets, we have:
P
[
z
/
t
]
t
∈ {
z

P
}
(
{}
+
)
t
∈ {
z

P
}
P
[
z
/
t
] (
{}
−
)Note that
Z
C
is strongly typed, so these (typed) set comprehensions present notechnical diﬃculties. See section 3 for further details.For bindings,
Z
C
has:
 ···
z
i
⇛
t
i
··· 
.
z
i
=
t
i
(
⇛
=
)
 ···
z
i
⇛
t
.
z
i
··· 
=
t
[
···
z
Tii
···
]
(
⇛
=
)The ﬁrst of these establishes what information may be extracted from bindings; thesecond conﬁrms that these values are
all
that the binding contains.
7
In fact
N
is only one possible base type. See section 3 for further details.
4
M. C. Henson, S. Reeves, J. P. Bowen
The logical rules for schemas ﬂow from the following
Z
C
deﬁnitions:
[
···
z
i
:
C
i
···
]
=
df
{
x

··· ∧
x
.
z
i
∈
C
i
∧ ···}
and:
[
S

P
]
=
df
{
z
∈
S

z
.
P
}
The
binding selection
operator, introduced in the object logic for selection from bindings (that is,
Z
C
terms such as
z
.
x
) is generalised into a metalanguage substitutionover terms (that is, metaterms such as
z
.t) and over propositions (metaterms suchas
z
.P)
8
. This is essentially a straightforward structural recursive generalisation of binding selection, and appears in more detail in section 3 below.The rules for
schema sets
are then derivable in
Z
C
:
···
t
i
∈
C
i
··· ···
z
i
⇛
t
i
···  ∈
[
···
z
i
:
C
i
···
] ([]
+
)
t
∈
[
···
z
i
:
C
i
···
]
t
.
z
i
∈
C
i
([]
−
)and, for
atomic schemas
:
t
∈
S t
.
P t
∈
[
S

P
] (
S
+
)
t
∈
[
S

P
]
t
∈
S
(
S
−
)
t
∈
[
S

P
]
t
.
P
(
S
−
)Then for example, writing
b
for

volume
⇛
100
,
temp
⇛
20

, we have:....100
∈
N
∧
20
∈
N
b
∈
[
volume
:
N
,
temp
:
N
] ([]
+
)....100
≤
250
∧
20
≤
100
b
∈
Jug
(
S
+
)as expected, with the trivial steps omitted.The elimination rules allow us to determine properties of speciﬁcations. Forexample, taking the product of the temperature and the volume as a rudimentarymeasure of the thermal energy of the water, we can show that this is never biggerthan 25000:
b
∈
Jug
1
,
(
S
−
)
b
.
volume
≤
250
∧
b
.
temp
≤
100
b
.
volume
∗
b
.
temp
≤
25000
∀
b
∈
Jug
•
b
.
volume
∗
b
.
temp
≤
25000 1
2.2 Schema algebra and ﬁltered bindings
Having now considered simple schemas, we will move on immediately to consider anoperation from the schema calculus:
schema conjunction
.
8
This is modelled to some extent on the more complex
object language
substitution
frogspawn
operator to be found in the faulty logic presented in [26]. A thorough analysisof frogspawn terms is presented in [19].