Z Notation Book
Z Notation Book
Z Notation Book
Documentation using Z:
A Case Study Approach
Jonathan Bowen
Revised 2003
FORMAL
SPECIFICATION
AND
DOCUMENTATION
USING
Z
X
A
CASE
STUDY
APPROACH Jonathan Bowen
transputer
DCS
UNIX
documentation All material that serves primarily to describe a system and make it
more understandable, rather than to contribute in some way to the actual operation
of the system. . . .
Z A formal notation based on set algebra and predicate calculus for the specifica-
tion of computing systems. It was developed at the Programming Research Group,
Oxford University. Z specifications have a modular structure. . . .
Foreword ix
Preface xi
I Introduction 1
3 A Brief Introduction to Z 29
3.1 Introduction 29
3.2 Predicate Logic 29
3.3 Sets and Relations 31
3.4 Functions and Toolkit Operators 41
3.5 Numbers and Sequences 44
3.6 Schemas 54
3.7 Conclusion 63
II Network Services 65
4 Documentation using Z 67
4.1 Introduction 67
v
vi Contents
4.2 Motivation 68
4.3 Service Specification 69
4.4 Service Documentation 71
4.5 Reservation Service – User Manual 72
4.6 Reservation Service – Implementor Manual 79
4.7 Experience 83
4.8 Conclusions 87
V Graphics 167
Acknowledgements 219
viii Contents
Appendices 221
A Information on Z 223
A.1 Electronic Newsgroup 223
A.2 Electronic Mailing List 223
A.3 Postal Mailing List 224
A.4 Subscribing to the Newsgroup and Mailing List 224
A.5 Electronic Z Archive 224
A.6 Z Tools 225
A.7 Courses on Z 226
A.8 Publications 227
A.9 Object-oriented Z 229
A.10 Executable Z 229
A.11 Meetings 229
A.12 Z User Group 230
A.13 Draft Z Standard 230
A.14 Related Organizations 230
A.15 Comparisons of VDM and Z 231
A.16 Corrections 231
B Z Glossary 233
Bibliography 253
Index 285
Foreword
The formal methods community has, in writing about the use of discrete mathematics
for system specification, committed a number of serious errors. The main one is to
concentrate on problems which are too small, for example it has elevated the stack
to a level of importance not dreamt of by its inventors. While there is a good reason
for using small examples at the beginning of a book or a tutorial, the need becomes
progressively less important as one progresses towards teaching students and industrial
staff topics such as structuring and modelling. Too many books have given up the fight
after presenting small examples and have, I believe, contributed greatly to the lack of
take-up of this technology. Staff and students who have read introductory materials on
formal methods such as Z and VDM have had their hopes raised by small examples
which have given the impression that formal specification is merely the writing down
of some simple mathematical statements which define the behaviour of a system. What
small examples do is to hide one of the most difficult tasks of specification: the process
of selecting an adequate model.
Jonathan Bowen is a formal methods researcher who I have a great deal of respect
for. Almost all his work has concentrated on the application of this technology to
real-life problems – not just stacks and queues. His book teaches through the medium
of case studies which are realistic but not too large that they overwhelm the reader.
They range from the specification of the Transputer instruction set to that of a tool for
formatting free text. All the case studies contain excellent examples of the power of
Z: its ability to structure large specifications into chunks which can be read, validated
and developed in relative isolation.
The formal methods community still have a long way to go in convincing many
industrialists of the power of discrete mathematics; I would regard this book as a
major contribution to doing so.
Darrel Ince
The Open University
ix
Preface
Formal methods are becoming more accepted in both academia and industry as one
possible way in which to help improve the quality of both software and hardware
systems. It should be remembered however that they are not a panacea, but rather one
more weapon in the armoury against making design mistakes. To quote from Prof.
Tony Hoare:
Of course, there is no fool-proof methodology or magic formula that will ensure a
good, efficient, or even feasible design. For that, the designer needs experience,
insight, flair, judgement, invention. Formal methods can only stimulate, guide, and
discipline our human inspiration, clarify design alternatives, assist in exploring
their consequences, formalize and communicate design decisions, and help to en-
sure that they are correctly carried out.
C.A.R. Hoare, 1988
Thus we should not expect too much from formal methods, but rather use them to
advantage where appropriate.
Even within the formal methods community, there are many camps: for example,
those that believe that a formally correct system must be proved correct mechanically,
one small step at a time, and those who use the term formal to mean mathematical, us-
ing high-level pencil-and-paper style proofs to verify a design is ‘correct’ with respect
to its specification. Sometimes the latter method is known as ‘rigorous’ to differentiate
it from the former; and of course there are positions between these two extremes.
Even if a system is proved correct, there are still many assumptions which may be
invalid. The specification must be ‘obviously right.’ There is no way that this can be
formally verified to be what is wanted. It must be simple enough to be understandable
and should be acceptable to both the designer and the customer.
This book presents an even more pragmatic view of the use of formal methods
than that held by some academics: that is that formal specification alone can still be
beneficial (and is much more cost effective in general) than attempting proofs in many
cases. While the cost of proving a system correct may be justified in safety-critical
systems where lives are at risk, many systems are less critical, but could still benefit
from formalization earlier on in the design process than is normally the case in much
industrial practice.
Ultimately the computer system will be communicating with the outside world. In
a control system, we will probably be dealing with physical laws, continuous math-
xi
xii Formal Specification and Documentation using Z
ematics (e.g., differential equations), etc. This will have to be converted into digital
values and approximations will have to be made. In many cases, a Human-Computer
Interface will be involved. Great engineering skill will be needed to ensure that any
assumptions made are correct and will not invalidate any formally verified design. It is
very important to apportion responsibility between the engineers associated with each
design task. Mutually agreed interfaces must be drawn up. Ideally these should be
formalized to reduce the risk of ambiguity and misunderstanding on each side of the
interfaces.
This book presents the use of one notation in the accumulation of available mathe-
matical techniques to help ensure the correctness of computer-based systems, namely
the Z notation (pronounced ‘zed’), intended for the specification of such systems. The
formal notation Z is based on set theory and predicate calculus, and has been devel-
oped at the Oxford University Computing Laboratory since the late 1970’s.
The use of a formal notation early on in the design process helps to remove many
errors that would not otherwise be discovered until a later stage. The book includes
specification of a number of digital systems in a variety of areas to help demonstrate
the scope of the notation. Most of the specifications are of real systems that have been
built, either commercially or experimentally. It is hoped that the variety of examples
in this book will encourage more developers to attempt to specify their systems in a
more formal manner before they attempt the development or programming stage.
In Part I, the first two chapters give an introduction to formal specification, using Z
in particular, and also to the issues concerning the practical take-up and use of formal
methods in industry. Chapter 2 gives an overview of some industrial issues, for those
contemplating the use of formal methods as part of the software development process.
Some guidelines to help with successful use are given. Finally a brief tutorial is given
in Chapter 3, which introduces Z for those who have not seen the notation before, but
who wish to tackle the rest of the book. However, it should be noted that this is not
a substitute for a fuller treatment, which if required should be sought from one of the
numerous Z textbooks now available.
Z has been designed to be read by (suitably trained) humans, rather than by comput-
ers, and as such may be included in manuals documenting computer-based systems.
Part II gives some examples, using network services designed and built at Oxford Uni-
versity. Two types of manual have been developed, one of the user of a service, giving
an idealized external abstract view, and one for potential implementors, giving more
details of the suggested internal structure of the service.
In Part III, Chapter 6 details the specification of a text formatting tool designed for
using under the UNIX operating system. The structure of UNIX files is discussed in
this context. A specification of a mouse-based input system for UNIX workstations is
also presented in Chapter 7.
Although Z has mainly been applied to software systems, it is also applicable to
hardware. In Part IV, a number of aspects important in the specification of machine
instruction sets are discussed. Chapter 8 formally defines some concepts which are
useful in the specification of any microprocessor. Building of this, a part of a specific
instruction set, namely that of the Transputer, is then presented in Chapter 9.
Part V details some graphical concepts. Chapter 10 introduces general concepts
useful for specifying pixel maps and window systems. Chapter 11 defines the raster-
op function which is fundamental to many graphics operations.
Preface xiii
Window systems are now one of the most popular interfaces for computers. Part VI
builds on the ideas presented in Part V and gives details of three window systems,
including the highly successful X Window System. Chapter 15 remarks on experience
gained by formally specifying the three window systems and other case studies.
Appendix A gives some indications on how to obtain further up-to-date information
on Z. A glossary of the Z notation may be found in Appendix B. A literature guide
in Appendix C together with a substantial bibliography at the end of the book are
included to allow readers to follow up on another aspect of Z and formal methods
that are of special interest. Finally an index, particularly of names of definitions in
the specifications presented in the book, will aid the reader in navigating the text,
especially the formal parts.
It is hoped that the specifications presented here will help students and industrial
practitioners alike to produce better specifications of their designs, be they large or
small. Even if no proofs or refinement of a system are attempted, mere formalization
early on in the design process will help to clarify a designer’s thoughts (especially
when undertaken as part of a team) and remove many errors before they become im-
plemented, and therefore much more difficult and expensive to rectify.
For further on-line information related to this book, held as part of the distributed
World Wide Web (WWW) Virtual Library, the reader is referred to the following URL
(Uniform Resource Locator):
http://www.afm.sbu.ac.uk/zbook/
J.P.B.
June 1995
I
Introduction
In Chapter 1, the use of the Z notation for the formal specification of computer-based
systems is introduced. Chapter 2 considers industrial concerns in the application of
formal methods such as the use of Z. Finally a brief tutorial introduction to the formal
notation of Z is given in Chapter 3.
Chapter 1
Formal Specification
using Z
This chapter provides an introduction to formal methods, in general, and formal
specification in particular: what they are, and how and why they should be used,
with an emphasis on the Z notation. It provides some motivation for the use of for-
mal specification, a brief introduction to some example applications as presented
in more detail in the rest of the book, and some conclusions on the suitability or
otherwise for the use of Z for system specification. The chapter is informal in na-
ture and suitable for those who may not wish to read the later more detailed case
study chapters.
1.1 Introduction
Many design and documentation methods make use of informal techniques. For exam-
ple, natural language and diagrams are often used alone to describe computer systems
and software. A more formal approach can result in a simpler design and more thor-
ough documentation. This book presents a general specification language, Z (‘zed’),
based on set theory and developed at the Oxford University Computing Laboratory
(OUCL), as a possible solution to this problem. The notation is useful (once it has
been learned) to organize the thoughts and aid the communication of ideas within a
design team. It is also readable enough to be used as a documentation tool in a manual.
Of course, natural language should also be included to give an informal description of
the system and to relate the mathematical description to the real world.
A major advantage of a formal notation is that it is precise and unambiguous and
thus the formal notation always provides the definitive description in the case of any
misunderstanding. A number of examples are discussed, including network services,
software for UNIX, microprocessor instruction sets, computer graphics, and window
systems. Full formal descriptions of these in Z are included in the book in later chap-
ters.
This chapter is split into two main parts. The first half deals with the nature of for-
mal specification and why it should be used. Additionally, a brief introduction to Z and
how it is used is also presented in general terms, without covering the notation itself.
The second half of the chapter deals with the experience gained using Z for the design
and documentation of network services and during some case studies of existing sys-
tems. Finally some conclusions are drawn about the advantages and disadvantages of
using a formal approach.
3
4 Formal Specification and Documentation using Z
a feasible amount of time, possibly to the detriment of the design. Even though a Z
specification is not in general executable by computer, by passing it round members
of a design team it may be mentally executed and checked far more reliably than an
equivalent informal specification.
Note that Z is a formal specification notation rather than a formal method although
the term method is sometimes used rather loosely in this context.
The Distributed Computing Software (DCS) project at the Oxford University Com-
puting Laboratory designed a number of network services using the Z language. The
results have been documented in several monographs [55, 56, 172]. The designs have
formed the basis for manuals for each of the services. Two different types of man-
ual have been produced. User Manuals have been designed to describe each service
from the point of view of a client program using the service via Remote Procedure
Calls (RPCs) over a network. In addition, Implementor Manuals have been produced
for some services. These describe how the service may be implemented internally. Z
is still used for this description, although it is assumed that an imperative sequential
programming language will be used for the final implementation. As well as the User
and Implementor Manuals, a Common Service Framework manual has been produced.
This describes common parts of services to avoid repetition in individual manuals.
Significant effort was expended in the presentation of the manuals to make them as
readable as possible while still employing a formal notation.
A User Manual
A user will normally be interested in how a service reacts with the outside world rather
than with the detailed inner workings of the service. Thus the manual can provide an
abstract view of the service. This may be based directly on the original abstract design.
Indeed, the initial design of the network services which have been produced during the
project have consisted of a skeleton version of the User Manual. This has subsequently
been tidied up and improved for the final version of the manual, thus greatly reducing
the amount of time spent producing documentation.
Each User Manual is split into a number of sections. After a general introduction,
the abstract state of the service is presented. Next common parameters shared by
a number of service operations are covered (for example, all operations produce an
output report). A section details the result of operations when an error occurs and the
8 Formal Specification and Documentation using Z
reports which a returned. Each error condition is described as a Z schema which may
subsequently be included by individual operations as required.
Each operation is normally allocated a page for its description, although occasion-
ally this can spill over onto a second page for more complicated operations. The de-
scription is split into three sections. An Abstract section describes how the operation
may appear as a procedure heading in some programming language. This includes
all the explicit input and output parameters of the operation. A Definition section
provides a formal description of the operation (as a Z schema) when it is performed
successfully. Finally, a Reports section formally defines the specific errors which may
occur when the operation is invoked by combining the schema in the previous section
with error schemas. These three sections are accompanied by informal description as
required.
The problem of accounting has also been addressed. This is often of secondary
interest to a user, so it is included in a separate section. The charge for each operation
(which may vary depending on the amount of data transferred, for example) is formally
defined in a single ‘tariff’ schema. Finally all the operations and the tariff schema are
combined, together with features from the Common Service Framework (see later) as
desired to produce a complete specification of the service.
An Implementor Manual
Unlike a User Manual, an Implementor Manual does need to concentrate on the in-
ternal operation of a service. Thus a more concrete description of the service must
be presented. When an Implementor Manual is produced, a number of design deci-
sions must be taken. In the Implementor Manuals produced by the DCS project, it has
been assumed that the service will be implemented using a sequential imperative pro-
gramming language. (In fact, Modula-2 has been used for the actual implementations
which have been produced.) However the manuals have still used Z rather than some
pseudo-code to describe the operations. A small number of extra schema operators
have been defined to allow descriptions of iteration, etc.
The outline for the Implementor Manuals is similar to that for the User Manuals.
However a concrete state and concrete operations are presented, together with sub-
operations and sub-states for subsystems as required by a particular service.
Of course, an Implementor Manual should be proved correct with respect to the
corresponding User Manual. This has only been done for a simple service. Even
for a modestly large service, this becomes intractable relately quickly if the process
is undertaken by hand. Hopefully this may be alleviated by machine assistance in
the future. In any case, the Implementor Manuals have been designed to convey the
design to a programmer, rather than to aid a proof of correctness by defining its rela-
tionship with the User Manual (although this relationship is included formally in the
Implementor Manual).
Some parts of a network service service will inevitably be the same or similar to parts
of all or a number of other services. In addition the general outline for the description
of an individual service tends to follow a common pattern. Hence it is convenient to
Chapter 1 Formal Specification using Z 9
group such aspects of the services in a separate document for use in the description of
each specific service.
The Common Service Framework covers such features. First an example of a gen-
eralized service is presented, including all common features which may be used by
a particular service. Then a number of common subsystems are formally described.
These include extra operations to deal with concerns like time, accounting, statistics
and access control. Any combination of these subsystems may be included in a given
service. This will increase the number of operations which may be performed on that
service.
Next, it is shown how all the services in the distributed system may be formally com-
bined to produce a specification of the complete system. Network attributes, including
authentication, and client attributes (e.g., identification) are also covered. Finally a
summary of the common sets and data types used by the services is given.
Part II provides some actual examples of network service manuals. Chapter 4
presents some more detailed motivation and a very simple service by way of example.
Chapter 5 takes the form of a more substantial user manual.
UNIX software
The UNIX [37] file system was used as one of the earliest examples of the specification
of a real system, demonstrating the structuring feature know as the schema calculus
that is provided as part of Z to enable large specifications to be tackled [298]. Part III
of this book provides further examples of more detailed software that has been imple-
mented under UNIX. Chapter 6 presents a text formatting tool, useful for justifying
ASCII text in a file [44]. A matching UNIX manual page is provided for comparison by
the reader. Chapter 7 gives a specification for a library of C routines that implement
an event-based input system for UNIX workstations [80].
Instruction sets
Z is not necessarily restricted to the specification of software-based systems. Any sys-
tem which may be viewed as an abstract state on which a number of operations may
be performed can be conveniently specified in Z. For example, Z has proved partic-
ularly good for specifying instruction sets. The Motorola 6800 8-bit microprocessor
instruction set has been completely specified as an exercise [39, 38]. Additionally,
large parts of the Inmos (now SGS-Thomson) Transputer [224] and Motorola 68000
16/32-bit microprocessor instruction sets have also been specified in Z [45, 149, 350].
Z scales up to these larger instruction sets with few problems, mainly because of the
schema notation.
Part IV of the book gives an introduction to the formal specification of instruction
sets in Z. Chapter 8 presents some general concepts concerning operations on micro-
10 Formal Specification and Documentation using Z
processor words, consisting of fixed length sequences of bits. Next, Chapter 9 gives a
portion of a real microprocessor instruction set, namely that of the Transputer.
1.4 Conclusions
Z is one of a number of specification languages which are being developed around
the world. It is a general purpose specification language. For example, Z could be
specified using itself [376, 79]. It could also be used to specify a more special pur-
pose language such as CSP [215], which is designed to handle concurrency. Z itself is
cumbersome for specifying parallel systems. Its use will produce a much longer spec-
ification than if CSP is used. Hence it is more convenient to use a language like CSP
in such cases. Work has been undertaken to attempt to combine some of the features
of CSP with Z [28, 239, 438].
Z has direct competitors. The most mature of these is probably VDM, advocated
by Jones [233]. This is also based on set theory and predicates, and is similar to Z in
a number of respects. Its differences include explicitly stating which components are
read and written by an operation, and explicitly separating the preconditions, involv-
ing only the before state, and postconditions, also involving the after state. A more
Chapter 1 Formal Specification using Z 11
advanced toolset is available for VDM, although the situation is being rectified for
Z. The notation is arguably less readable that Z. It lacks an equivalent to the schema
notation of Z which is so useful for aiding the structuring and readability of specifi-
cations. Subsequently, a more comprehensive set of notations, with tool support, has
been produced in the form of RAISE [343].
Another approach to formal specification is that of algebraic specification (e.g.,
Larch [183] and OBJ [176]). These uses abstract data types in which the allowed
operators on types are specified rather than the types themselves. This approach is
theoretically very attractive but problems can occur in scaling up specifications for
industrially sized examples.
1.4.1 Z – advantages
1.4.2 Z – disadvantages
Z is not ideal for all problems. For example, as mentioned previously, dealing with
concurrency is clumsy. However, Z is good for systems which may be modelled as a
sequence of operations on an abstract state. This book aims to demonstrate a range of
applications where Z is useful.
In general formal techniques require a significant amount of training effort and prac-
tical experience to be applied successfully. They require the dedication and commit-
ment of all those involved, managers and engineers alike. In the past, management
and software engineers have not received appropriate training for their use, although
the situation is changing with regard to many university computer science courses,
especially in the UK [314]. However, once trained, especially if done on the job, engi-
neers can apply for more attractive posts elsewhere, which can be a very real deterrent
for industry to train their employees.
The toolset for Z is still not very advanced by industrial standards. Perhaps the best
type-checker available is the f UZZ system [380] which is intended for use with the
widely available LATEX document preparation system [251] and is compatible with the
main Z reference manual in current use [381]. Some theorem proving support is now
available (e.g., ProofPower [236] from ICL, based on HOL [178]) but is still not yet
widely used. In general Z is still used for specification rather than proof in industry
[22]. [326] provides some information on available tools.
who wish to learn more about Z (e.g., [336] is recommended). The bibliography,
together with the associated literature guide in Appendix C, provide a comprehensive
and categorized list of references on Z, including other examples of significant systems
specified in the Z notation which help to demonstrate that it can be advantageously
applied to industrially sized problems.
Formal techniques such as Z are now sufficiently well established and supported for
the software industry to gain significant benefits from their use. In practice this has
only happened to a very limited extent so far despite a number of well publicized suc-
cessful examples. In the future, the advantages are likely to be even greater and those
that do not keep up with developments are likely to be left behind. Other more mature
engineering disciplines make use of mathematics as a matter of course to describe,
verify and test their products. It is time for all practising software engineers to learn
to do likewise if computing is to come of age.
For further on-line information about the Z notation, held as part of the distributed
World Wide Web (WWW) Virtual Library, the reader is referred to the following URL
(Uniform Resource Locator):
http://www.zuser.org/z/
The next chapter addresses industrial concerns in particular when using formal
methods for development of computer-based system, with some general guidelines
on the application of formal methods in practice.
Chapter 2
Industrial Use of
Formal Methods
Formal methods are propounded by many academics but eschewed by many indus-
trial practitioners. Despite some successes, formal methods are still little used in
industry at large, and are seen as esoteric by many managers. In order for the tech-
niques to become widely used, the gap between theorists and practitioners must be
bridged effectively. In particular, safety-critical systems, where there is a potential
risk of injury or death if the system operates incorrectly, offer an application area
where formal methods may be engaged usefully to the benefit of all. This chap-
ter discusses some of the issues concerned with the general acceptance of formal
methods and gives some guidance for their practical use. The chapter is informal
and suitable for those without a mathematical knowledge of the formal methods
involved.
2.1 Introduction
The software used in computers has become progressively more complex as the size of
computers has increased and their price has decreased [335]. Unfortunately software
development techniques have not kept pace with the rate of software production and
improvements in hardware. Errors in software are renowned and software manufac-
turers have in general issued their products with outrageous disclaimers that would not
be acceptable in any other more established industrial engineering sector [170].
It has been suggested that formal methods are a possible solution to help reduce
errors in software. Sceptics claim that the methods are infeasible for any realistically
sized problem. Sensible proponents recommend that they should be applied selectively
where they can be used to advantage. More controversially, it has been claimed that
formal methods, despite their apparent added complexity in the design process, can
actually reduce the overall cost of software. The reasoning is that while the cost of
the specification and design of the software is increased, this is a small part of the
total cost, and time spent in testing and maintenance may be considerably reduced.
If formal methods are used, many more errors should be eliminated earlier in the
design process and subsequent changes should be easier because the software is better
documented and understood.
15
16 Formal Specification and Documentation using Z
Some confuse formal methods with ‘structured methods’. While research is under-
way to link the two and provide a formal basis to structured methods (e.g., see [241]),
the two communities have, at least until now, been sharply divided apart from a few
notable exceptions. Many so-called formal ‘methods’ have concentrated on notations
and/or tools and have not addressed how they should be slotted into existing industrial
best practice. On the other hand, structured methods provide techniques for devel-
oping software from requirements to code, normally using diagrams to document the
design. While the data structures are often well defined (and easily formalized), the
relationships between these structures are often left more hazy and are only defined
using informal text (natural language).
Industry has been understandably reluctant to use formal methods while they have
been largely untried in practice. There are many methods being touted around the
market place and formal methods are just one form of them. When trying out any of
these new techniques for the first time, the cost of failure could be prohibitive and the
initial cost of training is likely to be very high. For formal methods in particular, few
engineers, programmers and managers currently have the skills to apply the techniques
beneficially (although many have the ability).
Unfortunately, software adds so much complexity to a system that with today’s
formal techniques and mechanical tools, it is intractable to analyze all but the simplest
systems exhaustively. In addition, the normal concept of tolerance in engineering
cannot be applied to software. Merely changing one bit in the object code of a program
may have a catastrophic and unpredictable effect. However, software provides such
versatility that it is the only viable means of developing many products.
Formal methods have been a topic of research for many years in the theoretical
computer science community. However they are still a relatively novel concept for
most people in the computing industry. While industrial research laboratories are in-
vestigating formal methods, there are not many examples of the use of formal methods
in real commercial projects. Even in companies where formal methods are used, it is
normally only to a limited extent and is often resisted (at least initially) by engineers,
programmers and managers. [184] is an excellent article that helps to dispel some of
the unfounded notions and beliefs about formal methods (see Section 2.5).
Up until quite recently it has widely been considered infeasible to use formal tech-
niques to verify software in an industrial setting. Now that a number of case studies
and examples of real use are available, formal methods are becoming more acceptable
in some industrial circles [182, 212, 218]. Some of the most notable of these are men-
tioned in [73], particularly those where a quantitative indication of the benefits gained
have been published.
to apply formal methods to the development process (e.g., VDM [233]), using a set
of rules or a design calculus that allows stepwise refinement of the operations and
data structures in the specification to an efficiently executable program. At the most
rigorous level, the whole process of proof may be mechanized. Hand proofs or design
inevitably lead to human errors occurring for all but the simplest systems.
Mechanical theorem provers such as HOL [178] and the Boyer-Moore system have
been used to verify significant implementations, but need to be operated by people
with skills that very few engineers possess today. Such tools are difficult to use, even
for experts, and great improvements will need to be made in the usability of these tools
before they can be widely accepted in the computing industry. Tools are now becoming
commercially available (e.g., the B-Tool and Lambda) but there is still little interest
in industry at large. Eventually commercial pressures should improve these and other
similar tools which up until now have mainly been used in research environments.
In particular, the user interface and the control of proofs using strategies or ‘tactics’,
while improving, are areas that require considerable further research and development
effort.
although such examples are exceptional. A recent international investigation of the use
of formal methods in industry [106, 105] provides a view of the current situation by
comparing some significant projects which have made serious use of such techniques.
[18] is another survey worthy of mention, which suggests that Z is one of the leading
formal method in use within industry.
[73] provides a survey of selected projects and companies that have used formal
methods in the design of safety-critical systems and [102] gives an overall view of this
industrial sector in the UK. In critical systems, reliability and safety are paramount to
reduce the risk of loss of life or injury. Extra cost involved in the use of formal methods
is acceptable because of the potential savings later, and the use of mechanization for
formal proofs may be worthwhile for critical sections of the software. In other cases,
the total cost and time to market is of highest importance. For such projects, formal
methods should be used more selectively, perhaps only using informal proofs or just
specification alone. Formal documentation (i.e., formal specification with adequate
accompanying informal explanation) of key components may provide significant ben-
efits to the development of many industrial software-based systems without excessive
and sometimes demonstrably decreased overall cost (e.g., see [212, 218]).
less ambiguity and thus less likelyhood of errors [41]. Formal specification alone has
proved beneficial in practice in many cases [22]. Such use allows the possibility of
formal development subsequently as experience is gained.
The Human-Computer Interface (HCI) is an increasingly important component of
most software-based systems. Errors often occur due to misunderstandings caused by
poorly constructed interfaces [261]. Formalizing an HCI in a realistic and useful man-
ner is a difficult task, but progress is being made in categorizing features of interfaces
that may help to ensure their reliability in the future. There seems to be considerable
scope for further research in this area, which also spans many other disparate disci-
plines, particularly with application to safety-critical systems where human errors can
easily cause death and injury [192].
Security is an area related to safety-critical systems. Security applications have
in some cases been very heavy users of formal methods. However, it is normally
extremely difficult to obtain hard information on such projects because of the nature of
the work. Thus there is comparatively little widely published literature on the practical
application and experience of formal methods in this field, with a few exceptions (e.g.,
see [35]).
frequently to reflect the latest available techniques and best practice. For example,
00-55 includes a separate guidance section.
2.4.2 Legislation
Governmental legislation is likely to provide increasing motivation to apply appro-
priate techniques in the development of safety-critical systems. For example, a new
piece of European Commission (EC) legislation, the Machine Safety Directive, came
into effect on 1st January 1993 [121]. This encompasses software and if there is an
error in the machine’s logic that results in injury then a claim can be made under civil
law against the supplier. If negligence can be proved during the product’s design or
manufacture then criminal proceedings may be taken against the director or manager
in charge. There is a maximum penalty of three months in jail or a large fine [306].
Suppliers have to demonstrate that they are using best working practice. This could
include, for example, the use of formal methods. However the explicit mention of
software in [121] is very scant. Subsection 1.2.8 on Software in Annex B on p. 21 is
so short that it can be quoted in full here: ‘Interactive software between the operator
and the command or control system of a machine must be user-friendly.’ Software
correctness, reliability and risk are not covered as separate issues.
Care should be taken in not overstating the effectiveness of formal methods. In
particular, the term formal proof has been used quite loosely sometimes, and this has
even led to litigation in the law courts over the Viper microprocessor, although the
case was ended before a court ruling was pronounced [270]. If extravagant claims are
made, it is quite possible that a similar case could occur again. 00-55 differentiates be-
tween formal proof and rigorous argument (informal proof), preferring the former, but
sometimes accepting the latter with a correspondingly lower level of design assurance.
Definitions in such standards could affect court rulings in the future.
5th commandment: Thou shalt not abandon thy traditional development methods.
This relates to Myth 10. Formal methods should be used as an extra technique in
the armoury available for the elimination of errors. Certainly they will not catch all
the errors, so other techniques should also be used (e.g., see the 9th commandment
below).
6th commandment: Thou shalt document sufficiently.
Much of this book is dedicated to this subject, hopefully demonstrating that a for-
mal notation like Z can be used in a beneficial way for system documentation. Even
if the formal specification is omitted from the final documentation, its production
is likely to make the informal documentation clearer and less ambiguous.
7th commandment: Thou shalt not compromise thy quality standards.
Software quality standards such as ISO 9000 need to be met, whatever the develop-
ment techniques that are used. Formal methods can help in this respect if applied
sensibly, but the project manager should ensure that they do help rather than hinder
in practice.
8th commandment: Thou shalt not be dogmatic.
Absolute correctness in the real world can never be achieved. Mathematical models
can be verified with a good level of certainty, but these models might not correspond
with reality correctly. When applying formal methods, the level of use should al-
ways be determined beforehand and monitored while in progress. A project man-
ager should always be prepared to adjust the level of use if required.
9th commandment: Thou shalt test, test, and test again.
Formal methods will never replace testing; rather they will reduce the number of
errors found through testing. Formal development and testing tend to avoid and
discover different types of error, so the two are complementary to some extent.
10th commandment: Thou shalt reuse.
Formal specifications can be written in a reusable manner, with some thought. As
an example, Z includes a ‘toolkit’ of definitions, defined in Z itself, which have
proved to be useful for many different specifications. The core of the toolkit is
accepted as standard by most people who use Z for specification. In this book, the
Common Service Framework mentioned in Part II, the machine word definitions in
Chapter 8, and the graphics definitions in Part V, could all be reused – indeed, have
been reused – for other specifications.
The above ‘commandments’ will hopeful provide basic guidance in the use of formal
methods in practice. For further details, see [68]. For a number of examples of the
realistic application of formal methods, see [213].
• Better tools. Most formal methods tools so far have resulted from formal methods
research projects, and associated spin-off companies, rather than mainstream tools
developers. As a result, their usability, and sometimes robustness, can often leave a
lot to be desired. Unfortunately the formal methods tools market is still fairly small
and raising capital to invest in serious production quality tools may be difficult.
Raising commercial venture capital is likely to be difficult because the banks will
be more interested in the size of the market rather than the potential improvement
in software quality!
• Investment in technology transfer. The transfer of technology like formal methods
is a time consuming and costly business. The effects and benefits of formal methods
are less palpable than some of the other more popular techniques that come and go
with fashion. The investment in learning and using formal methods is large, but
the returns in the long term can be commensurate with this. Most people who have
made the investment have not regretted it afterwards, and would not go back to
their old ways.
• Unification and harmonization of engineering practices involved in building high
integrity systems. While the use of formal methods may seem to run perpendicular
and even counter to some other concerns on software engineering projects, such
friction should be minimized. It is important that all those involved, be it managers
or engineers, and whether the personnel involved fully understand the techniques
or not, at least understand the way the techniques slot into the overall framework.
It can be galling to some managers that the use of formal methods considerably
delays the start of production of code in the life-cycle. However it considerably
speeds up and improves its production when it is generated.
• More practical experience of industrial use of the methods. A number of signifi-
cant projects have now been undertaken using formal methods [213], but more are
needed to gain a better insight into the general applicability of such techniques.
Most successful formal methods project have had the help of an expert on call in
case of difficultly. It remains to be seen if formal methods can be successfully ap-
plied when less expert help is at hand. Fortunately computer science undergraduate
courses (in Europe at least) do now provide some suitable grounding for many soft-
ware engineers who are now entering the profession. However, the effects will take
some time to filter through in practice.
• Assessment and measurement of the effectiveness of formal methods. Metrics are
a problematic area. It would obviously be helpful and commercially advantageous
to know the effect of the use of formal methods on the productivity, error rates,
etc., in software (and hardware) development. However these can be hard and ex-
pensive to obtain, and even if hard numbers are available, these may not actually
measure the aspect that is of real interest. It is also difficult to extract such com-
mercially sensitive into the public domain, which hampers academic study of and
potential solutions to the problems. Metrics should be treated with caution, but
improvements in such techniques would be worthwhile.
The actual formal methods, etc., available at any given time, can and will of course
vary, and hopefully improve. For further up-to-date on-line information on formal
methods, notations, and tools, held as part of the distributed World Wide Web (WWW)
28 Formal Specification and Documentation using Z
Virtual Library, the reader is referred to the following URL (Uniform Resource Loca-
tor):
http://www.afm.sbu.ac.uk/
This chapter has considered the practical use of formal methods in general. The rest
of the book concentrates on the use of Z in particular, providing a brief introduction
in the next chapter, followed by a number of case studies, and appendices of related
information.
Chapter 3
A Brief Introduction to Z
This chapter provides a brief guide to the main features of Z. In the space available
here, it is only possible to present a flavour of the notation. Rather than give a
sketchy presentation of all of Z, some parts are presented in considerably greater
detail than others. Some lesser used features are omitted altogether. This eclectic
description is no substitute for a full tutorial introduction to Z. There are many
textbooks which already provide such introductions.
Some basic knowledge of predicate logic and set theory is highly desirable before
attempting this chapter, and most of the rest of the main part of the book. If required,
the reader is referred to the comprehensive list of Z textbooks collected together on
page 244 in Appendix C. Many of these include a grounding in the mathematics
involved before tackling the specific notation of Z. One that is widely used for Z
courses is [336]. Readers already familiar with Z may skip this chapter.
3.1 Introduction
In summary, Z [381] is a typed formal specification notation based on first order pred-
icate logic and Zermelo-Fraenkel (ZF) set theory [376]. It is a typed language which
allows a certain amount of static machine checking of specifications to avoid ‘obvious’
errors (e.g., using the f UZZ [380] or ZTC [444] type-checking tools). The notation was
originated and inspired by Jean-Raymond Abrial while visiting the Oxford University
Computing Laboratory, and was subsequently further developed by Hayes, Morgan,
Sørensen, Spivey, Sufrin and others [78]. Z is popular with governments, academics
and parts of industry [18], especially those developing critical systems where the re-
duction of errors and quality of software is extremely important [73]. It is undergo-
ing international standardization under ISO/IEC JTC1/SC22 [79]. A thriving Z User
Group organizes regular meetings (e.g., see the ZUM’95 proceedings [69]).
29
30 Formal Specification and Documentation using Z
like VDM [233] for example, predicates have one or other of these values. There is no
third ‘undefined’ value, which helps considerably in minimizing the complexity of the
interpretation of the language. If the result of a predicate cannot be established (for
example, because of an undefined expression within the predicate), then the predicate
may be interpreted as being either true or false, but the value is impossible to deter-
mine. This contrasts with some other logics which sometimes add a third ‘undefined’
value to handle such cases. This extra value can add considerable complexity, and the
Z approach is a compromise to try to keep things as simple as possible.
3.2.2 Quantification
Full predicate logic augments propositional logic with quantification over a list of
variables X, including type information in the case of Z:
• Universal quantification ∀ X • q is only true when the predicate q is true for all
possible values of X.
• Existential quantification ∃ X • q is true if there is any (at least one) set of values
for X possible which make q true. There may be more than one value; indeed all
possible values, as required for universal quantification, would still be valid.
• Unique existential quantification ∃1 X • q is a special but useful case of the more
general existential quantification which only allows X to take a single value, not an
arbitrary (non-zero) number of values.
X may be one or more variables, with type declarations in each of the above cases.
The scope of the variables listed in X is bounded by the clause q in the examples above.
Thus the same names may be reused outside the clause to stand for different variables
if desired.
3.2.3 Laws
There is a rich set of algebraic laws for transforming predicates when performing
proofs about specifications. A good selection of these is presented in [297]. Only a
Chapter 3 A Brief Introduction to Z 31
very cursory introduction to predicate logic has been given here. For more informa-
tion, see almost any of the Z textbooks listed on page 244.
3.3.1 Types
Z is a typed language; that is to say, every variable in Z has a particular type (i.e., set
from which it is drawn) associated with it which must match appropriately when it is
combined with other variables.
The question arises, why fuss about types? They introduce a lot of extra complex-
ity to a specification. However this proves to be well worthwhile for the following
reasons:
1. It helps to structure specifications.
We can specify the set of possible values from which a variable can be drawn, and
we can then further constrain the variable using a predicate if required. For example
in the (English) statement:
x is a path of least cost from A to B
we could give x a type:
x : Path
and constrain it further with a predicate:
least cost x
A, B : People
x : Likes
Predicate(x)
The first part of this is a signature (of variables including types) and the second part is
a predicate. The parts of the signature after the colons specify the types of the variables
before the colons, much like definitions in a programming language such as Pascal.
How can we build up types and what are the variables in predicates? For this, we
need to explore the world of set theory.
3.3.2 Sets
Mathematicians early in the 20th century discovered how to construct a world of sets,
powerful enough to describe anything we meet in practice.
A set is a collection of objects or elements of some type. Here are some examples
of the notation used in Z to describe sets:
∅ This denotes the empty set – i.e., the set with no elements in it. This can also
be denoted as {}.
{Jane, Alice, Emma} This is a set of people containing three elements. Note that
the types of Jane, Alice and Emma must be compatible!
{0, 1, 2} = {0, 0, 1, 0, 2, 1} = {1, 2, 0} All three of these represent a three ele-
ment set of numbers. An important property of sets is that there is no inherent
ordering in its elements (unlike in a list for example). Thus the numbers above may
be specified in any order, and repeated elements simply map on top of one another.
{0, 1, 2, 3, . . .} This is the set of natural numbers, or integers ranging from zero
upwards. Note that this set contains an infinite number of elements. The ‘. . . ’ in
this definition is informal (i.e., not part of the Z language). We cannot write out all
the elements of this set using this notation. Later we shall introduce a method for
overcoming this. Since the set of natural numbers is a very important set in many
Z specifications, it is normally denoted N for brevity.
{∅} =
6 ∅ It is important to understand that the set containing the empty set is
not the same as the empty set itself. It is a set containing one element (namely,
the empty set). Thus it is possible to have sets containing other sets (which may
themselves contain sets), and so on. We will look at this again later.
Note that every set must be drawn from some basic type (or given set) in Z. This even
applies to the empty set, ∅. I.e., there is a different empty set for each type. When
the empty set is used in Z, its type should be obvious from the context. If not, there
is probably something wrong with the specification. To avoid confusion, the notation
∅[T] may be used to indicate the empty set drawn from type T.
It is often important to be able to say that an element belongs to (‘is a member of ’)
a particular set. In set theory, we write ‘x is an element of S’ as:
x∈S
Chapter 3 A Brief Introduction to Z 33
This is a predicate (extra constraint) on x and S. Note that x and S must be type-
compatible for this to be meaningful. Here are some examples of this notation:
0 ∈ {0, 1, 2} This is patently true since 0 is one of the elements in the set con-
taining 0, 1 and 2.
∅ ∈ {∅} The empty set (of a particular type) is a member of the set containing
just the empty set of that type. In fact it is the only member.
0∈
/∅ This is another way of writing ‘¬ (0 ∈ ∅)’ – i.e., 0 is not a member of the
empty set (of numbers). This is true because no element can be a member of the
empty set; there are no elements in it by definition. In fact, for any x, we can say
x∈/ ∅. A special notation is used for ‘is not a member of ’ since this occurs quite
often in specifications.
William ∈
/ {Jonathan, Jane, Alice, Emma}
The set being checked by ∈ / need not be empty for a predicate using it to be true.
For example, the set of people given here does not include William, so the predicate
is true.
Operations on sets
So far, we have discovered how to denote (finite) sets as a number of elements and
how to specify membership and non-membership of sets. However, to manipulate sets
usefully, we need a richer collection of operators on sets. We shall now look at a
number of such operators.
The following operators two sets and return a new one:
P P ∪ Q Q
& &% %
P
P ∩ Q
Q
& &% %
P\Q ‘P minus Q’ – difference.
This gives the set with elements which are contained in P, but are not members of
Q.
' ' $ $
P P\Q Q\P Q
& &% %
The following are predicates on sets (or expressions representing sets):
P=Q ‘P equals Q’ – identity of sets.
The sets P and Q each contain exactly the same elements. As we have seen before,
{Alice} = {Alice, Alice, Alice}
{Alice, Emma} = {Emma, Alice}
You can see from the previous three Venn diagrams that
(P \ Q) ∪ (P ∩ Q) ∪ (Q \ P) = P ∪ Q
Often we wish the say the negation of P = Q – i.e., P and Q do not contain the same
elements. This may be written as ‘P 6= Q’ (which is equivalent to ‘¬ (P = Q)’).
P⊆Q ‘P contained in Q’ – subset.
All the elements of P are in Q. Note that it may be the case that P = Q. To specify a
strict subset, we use the notation ‘P ⊂ Q’. This is shorthand for ‘P ⊆ Q ∧ P 6= Q’.
' $
#
P Q
"!
& %
The following operator takes a set and returns another set:
−
P ‘complement P’ – complementation.
Set theory includes the idea of the complement of a set – i.e., all the elements not
in the set. Because Z is typed, this means all the elements of the same type not in
the set. This is not a part of Spivey’s ‘toolkit’ of operators [381], but can easily be
defined in terms of the ‘\’ operator. For a type T where P ⊆ T,
P− = T \ P
Chapter 3 A Brief Introduction to Z 35
' $
#
P− P T
"!
& %
− −
Note that T = ∅[T] and ∅[T] = T.
For completeness, we include our concept of set membership here:
x∈P ‘x belongs to P’ – membership.
x is one of the elements in P; and conversely, ‘x ∈
/ P’ means x is not one of the
elements in P (i.e., ‘¬ (x ∈ P)’).
Question: Simplify:
1. (P \ Q) \ P
2. (P \ Q) ∪ (P ∩ Q)
Set comprehension
So far we have defined sets in terms of individual members of that set. This is a rather
restrictive (although often useful) method of defining sets. For any set containing more
than a few elements, it is going to be a very cumbersome way of specifying sets. For
infinite sets, it fails completely since we would require an infinitely long document to
describe such sets.
What we need is a more general way of specifying sets. For this, we use a construc-
tion known as set comprehension. This ‘comprehensive form’ of set definition takes
the following form:
{x : Type | Predicate(x)}
or more generally {Signature | Predicate}, where the signature may include may than
one variable.
Here are some examples of the use of set comprehension:
{x : N | x is prime} (= {2, 3, 5, 7, 11, 13, . . .}).
This defines the set of all prime numbers (provided is prime is defined appropri-
ately). This is, of course, an infinite set.
{x : Path | least cost(x)}
This is the set of paths between A and B such that the cost is minimized. There
could be more than one such path if two or more paths have equally low cost; or
the set could be empty if there are no paths between A and B.
36 Formal Specification and Documentation using Z
Subsets
We have introduced the idea of a subset – i.e., a set contained within another set. Let
us look at a few examples of this in use:
A⊆B Each element of A is also an element of B.
∅⊆A This is always true. Every set contains at least the empty set (of compati-
ble type).
A⊆A Every set ‘contains’ itself.
{0, 1} ⊆ N
The numbers 0 and 1 make up a subset of the natural numbers.
{x : N | x is prime ∧ x 6= 2} ⊆ {x : N | x is odd}
The set of prime numbers (not including the number 2) is a subset of the odd num-
bers.
Set operations
Consider the subset operator ⊆. This has a number of mathematical properties. For
sets P, Q and R, drawn from the type T (i.e., P ⊆ T, Q ⊆ T and R ⊆ T):
⊆ is reflexive: P⊆P
⊆ is transitive: (P ⊆ Q ∧ Q ⊆ R) ⇒ P ⊆ R
⊆ is antisymmetric: (P ⊆ Q ∧ Q ⊆ P) ⇒ P = Q
∅[T] is the minimum of T: ∅[T] ⊆ P
Similarly, set intersection (∩) also has a number of properties:
• ∩ is the greatest lower bound of ⊆:
R ⊆ P ∧ R ⊆ Q ⇔ R ⊆ (P ∩ Q)
P ∩ Q is the largest subset of both P and Q.
• ∩ is idempotent P∩P=P
symmetric P∩Q=Q∩P
associative (P ∩ Q) ∩ R = P ∩ (Q ∩ R)
monotonic P ⊆ Q ⇒ (R ∩ P) ⊆ (R ∩ Q)
We can write P− for the complement of P (with respect to its type!). Complementing
a set is involutive:
(P− )− = P
Compare the following with contrapositive in predicate logic:
P ⊆ Q ⇔ Q− ⊆ P−
(¬ ). Note that
P ⊆ Q ⇔ P ∩ Q− = ∅
We normally write P ∪ Q for (P− ∩ Q− )− (one of De Morgan’s laws). We could list
further properties of ∪, etc. See [381] for a more comprehensive collection of laws.
Cartesian product
Sometimes it is useful to associate two or more sets together in order to build up more
complex types. If T and U are types then the Cartesian product
T ×U
denotes the type of ordered pairs
(t, u)
with t : T and u : U. If P and Q are subsets of types T and U respectively then
P × Q = {p : T; q : U | p ∈ P ∧ q ∈ Q}
38 Formal Specification and Documentation using Z
The notation may be generalized to an ordered n-tuple and any valid expression may
be used for the types:
E1 × E2 × . . . × En
Here are some examples of the notation of tuples (. . .) and Cartesian products in use:
(Z, Jonathan) ∈ Methods × People
A method has been associated with a person as an ordered pair or 2-tuple, perhaps
because they approve of it.
(Oxford, Cambridge) ∈ Places × Places
Two places are associated with each other (in some sense!). Here the types are the
same. This could be useful when specifying some relationship between places, for
example.
(Jonathan, Oxford, 1956) ∈ People × Places × N
This could be specifying the place and year of birth, as a 3-tuple.
Sometimes it is useful to extract the first or second element from an ordered pair.
We use the following notation for this:
first(t, u) = t
second(t, u) = u
For an ordered pair t, the following law applies:
(first t, second t) = t
Question: Is X × Y × Z equivalent to (X × Y) × Z or X × (Y × Z) ?
This notation permits us to write other, more complex, sets. For example, the set of
squares of primes may be defined as:
{x : N | x is prime • x ∗ x}
Here the expression x ∗ x acts as the defining term for the set.
In general the last term after the ‘•’ may be any valid expression:
{ Signature | Predicate • Expression }
The signature declares any variables required for the set comprehension definition, the
predicate constrains them as required, and the expression returns the elements in the
desired set. We may omit this last expression when it is simply a tuple formed from
the components of the signature. We can omit the predicate if it is simply true.
Power set
When defining a variable which is itself a set, its type will be a set of sets. Since many
variables in Z specifications are sets, we use a special notation for this. If S is a set,
P S denotes the set of all subsets of S, or the power set of S. Note that
X ∈ PS ⇔ X ⊆ S
Also ∅ ∈ P S, so P S 6= ∅. Here are some examples of power sets:
P∅ This set just contains the empty set of a given type (i.e., P ∅ = {∅}).
P{a} = {∅, {a}}
The power set of a singleton set is a set consisting of the empty set and the singleton
set.
PN This is the set of all possible sets of natural numbers. This is infinite of
course.
P Path Set of all sets of paths from A to B.
P(N × N) Sets of pairs of numbers. The Cartesian product may be used as
required in the definition of power sets.
S == P((Places × Places) × Path)
This is an abbreviation definition. X == Y means ‘replace X by Y’ where X is used
subsequently.
Here brackets have been used to group and nest Cartesian products. This can be
done to an arbitrary depth, but it is best to limit such usage to aid readability.
Given the definition above, we can say - ∈ S. The under scores are place-
Sometimes we are interested in non-empty subsets. For these, we use the notation
P1 (non-empty power set) or F1 (non-empty set of finite subsets):
P1 S == P S \ {∅}
F1 S == F S \ {∅}
3.3.3 Relations
Sometimes individual elements in one set are related to particular elements in another
set. For example,
R1 : Places ‘A’ and ‘B’ are adjacent.
R2 : Path x costs y to traverse.
(For example, ‘s - t’.) We can write R for relation R to indicate that it is an infix
p 7→ q
instead of (p, q) as a more graphical indication that p is related to q (although the
mathematical meaning is identical). Here are some examples of relations:
≤ = {x, y : N | (∃ z : N • x + z = y)}
uses = {Jonathan 7→ Z, Peter 7→ VDM, Peter 7→ RAISE}
If T, U are types,
T ↔ U == P(T × U)
denotes the set of all relations from T to U.
≤ ∈ N↔N
uses ∈ {Jonathan, Mike, Peter} ↔ Methods
Chapter 3 A Brief Introduction to Z 41
Every relation has a domain and range. The domain of a relation R : T ↔ U is the set
of all elements in T which are related to at least one element in U by R. The range is
all elements in U related to at least one in T. Formally:
dom R = {x : T | (∃ y : U • (x, y) ∈ R)}
ran R = {y : U | (∃ x : T • (x, y) ∈ R)}
Every relation also has an inverse. The inverse of a relation is another relation with all
its tuples (x, y) reversed (i.e., (y, x)). Again, formally we have:
R∼ = {x : T; y : U | (x, y) ∈ R • (y, x)}
= {x : T; y : U | (x, y) ∈ R • y 7→ x}
= {y : U; x : T | (x, y) ∈ R}
If R is of type T ↔ U, then its inverse R∼ is of type U ↔ T. Note that R∼ may also
be written as R−1 .
As an example, for the ‘uses’ relation we have:
dom uses = {Jonathan, Peter}
ran uses = {Z, VDM, RAISE}
uses∼ = {Z 7→ Jonathan, VDM 7→ Peter, RAISE 7→ Peter}
Pictorially, we may view the ‘uses’ relation as follows:
uses -
' People $' Methods $
- Z
Jonathan )
dom uses
Peter
yX
XXXXX
- VDM ran uses
XX z RAISE
Alice
XX
Emma B-Method
... ...
& %& %
Here is another example:
ran ≤ = dom ≤
= N
∼
( ≤ ) = ≥
The following laws concerning dom, ran and ∼ are relevant when reasoning about
relations:
ran(R∼ ) = dom R
dom(R∼ ) = ran R
(R∼ )∼ = R
Otherwise, reasoning about relations is as for sets.
3.4.1 Functions
In Z, functions are a special case of relations in which each element in the domain has
at most one value associated with it. For example, a partial function ‘→’ 7 is defined
using set comprehension in terms of a more general relation ‘↔’ as follows, using an
‘abbreviation definition’:
X→
7 Y ==
{ f : X ↔ Y | (∀ x : X; y1 , y2 : Y •
(x 7→ y1 ) ∈ f ∧ (x 7→ y2 ) ∈ f ⇒ y1 = y2 ) }
I.e., any element x in the domain can only map to a single value in the range of the
function, not to two (or more) different ones. X and Y are identifiers which repre-
sent arbitrary formal generic parameters. These are local to the right hand side of
the definition. → 7 is an infix symbol, and here ‘X → 7 Y’ is actually a short form for
‘( → 7 )[X, Y]’ where the underlines indicate positions of the parameters. The generic
parameters may be explicitly given in square brackets when → 7 and other similar con-
structs are used, but they are normally omitted since in most cases they can be inferred
from the context and clutter the specification unnecessarily.
There are a number of special types of function in Z, each given there own unique
type of arrow. For example, total functions, as indicated by ‘→’ have a domain con-
sisting of all the possible allowed values.
Here is a list of the other standard types of function available in Z:
• X 7 Y – Partial injections, in which there is a one-to-one mapping between ele-
ments in the domain and the range. Different values in the domain map to different
values in the range. Thus the inverse is also a function.
• X Y – Total injections, where the function is a partial injective in which the
domain completely populates the set X. I.e., if a function is defined as f : X Y,
then dom f = X.
• X→ →7 Y – Partial surjections, where the range completely populates the set Y. I.e.,
if a function is defined as f : X →
→
7 Y, then ran f = Y.
• X→ → Y – Total surjections, where both the domain and the range completely pop-
ulate X and Y respectively. Here, if a function is defined as f : X →
→ Y, then
dom f = X and ran f = Y.
• X → Y – Bijections, one-to-one total injective and surjective functions. Again,
with a function defined as f : X → → Y, dom f = X and ran f = Y, but in addition,
the inverse is also a total function (i.e., f ∼ ∈ Y → X).
• X→ 7 7 Y – Finite partial functions, where the domain of the function (and hence the
also range which can never be larger than the domain for a function) must be finite.
This is a subset of all partial functions on X and Y, and also of F(X × Y).
• X 7 7 Y – Finite partial injections, which as well as being finite are also one-to-one.
This is the same as the intersection of finite functions and partial injections on X
and Y.
All these different types of function are formally defined on pages 105 and 112 of
[381].
Chapter 3 A Brief Introduction to Z 43
• Q ⊕ R – Overriding. For each tuple in the right hand relation R, any tuples with
a matching first element in the left hand relation Q are omitted and the tuple is
included in the resulting relation. If no such tuple exists for a given tuple in Q,
then it is included in the resulting relation. More formally, Q ⊕ R is the same as
(dom R − C Q) ∪ R. Note that ⊕ is often applied to functions where part of the left
hand function needs to be modified by the right hand function (often typically a
single tuple), but in the general case in may be applied to a pair of relations.
3.5.1 Numbers
Let us consider sets of numbers which could be useful in defining sequences. The set
of integers
Z = {. . . , −2, −1, 0, 1, 2, . . .}
N = {n : Z | n ≥ 0} = {0, 1, 2, . . .}
Arithmetic
The following operators on integers are assumed and may be used in expressions as
required:
Chapter 3 A Brief Introduction to Z 45
addition + 2+2=4
subtraction − 4−2=2
multiplication ∗ 2∗2=4
division div 5 div 2 = 2
modulo arithmetic mod 5 mod 2 = 1
negation − −(−2) = 2
Brackets may be used for grouping (as they may in any Z expression). For example,
2 ∗ (4 + 5) = 18. The standard comparison relations are available:
less than < 2 < 3, ¬ 3 < 2
less than or equal ≤ 2≤2
greater than > a>b⇔b<a
greater than or equal ≥ a≥b⇔b≤a
The maximum and minimum values of a (non-empty) set of numbers can be deter-
mined.
maximum of a set max{1, 2, 3} = 3
minimum of a set min{1, 2, 3} = 1
Care should be taken to ensure that the set supplied to max or min is non-empty.
Otherwise the result will be undefined.
Extra operators may easily be added if required. For example, the function which
returns the absolute value of an integer may be defined using an axiomatic description:
abs : Z → Z
∀n : Z •
n ≤ 0 ⇒ abs n = −n ∧
n ≥ 0 ⇒ abs n = n
Note that ran abs = N.
Question: Can you suggest an alternative definition for abs?
An axiomatic description is available for use globally in the rest of a specification.
Such a description may be a loose specification in that there may be more than one
possible model for the specification. E.g., for the description
n:N
n ≤ 10
any integer value of n from 0 to 10 is allowable.
Sometimes strictly positive (non-zero) natural numbers are of interest. The notation
N1 = N \ {0} = {1, 2, 3, . . .}
is used for this.
Exercise: Write definitions for:
1. the square of an integer,
2. the factorial of a natural number.
46 Formal Specification and Documentation using Z
The successor function succ returns the next number when applied to a natural number:
succ = {0 7→ 1, 1 7→ 2, 2 7→ 3, . . .}
Thus ran succ = N1 . The successor function is often useful in specifications. Some-
times the inverse predecessor function is also useful. If this is so, we could define
pred == succ∼
The following laws apply:
succ = N C ( + 1)
= ( + 1) B N1
pred = N1 C ( − 1)
= ( − 1) B N
succ o9 succ = N C ( + 2)
= ( + 2) B (N1 \ {1})
succ o9 pred = id N
pred o9 succ = id N1
Iteration
Sometimes we wish to compose a relation R : X ↔ X (i.e., one in which the types of
the domain and range match) a certain number of times, n. As previously mentioned,
we normally write this as Rn . Informally we have
Rn = R o9 R o9 . . . o9 R k times
Using succ : N → N as a specific example, we can consider the following cases:
succ0 = id N Composing a relation zero times simply gives the identity relation.
It is as if the relation is not there, so elements are just mapped onto themselves
succ1 = succ Composing a relation once is the same as the relation itself.
2
succ = succ o9 succ This is the same as composing the relation with itself.
succn = N C ( + n) = ( + n) B {i : N | i ≥ n}
For any n : N, the above law applies.
succ−1 = succ∼ The inverse of a relation is a special case of iteration. As pre-
viously mentioned, the notations R∼ and R−1 may be used interchangeably if the
domain and range have the same type.
Exercise: Provide another way of writing:
1. Rm o9 Rn
2. (Rm )n
Chapter 3 A Brief Introduction to Z 47
Number range
A number range (a set of numbers) between two integers a, b : Z is denoted as
a . . b = {a, a + 1, a + 2, . . . , b − 2, b − 1, b}
or more formally
a . . b = {n : Z | a ≤ n ≤ b}
If a > b then a . . b = ∅. Also a . . a = {a}.
Cardinality
The cardinality of a (finite) set is the number of elements in that set, or the size of the
set. The cardinality of a set s ∈ F T (the set of all finite subsets of T – see page 39) is
denoted:
#s
Thus #∅ = 0, #{a} = 1, #{a, b} = 2 (if a 6= b) and so on. For a number range
a . . b,
#a . . b = 1 + b − a if a ≤ b
= 0 if a > b
= max{0, 1 + b − a}
For a set to be ‘finite’, it must be possible to map from a natural number in the range
1 . . n uniquely onto each element in that set. n is then the cardinality or size of the
set. This mapping can be done with a suitable finite partial injective function. For
example, the set a . . b (where a ≤ b) may be mapped using the function f : N 77 Z
such that f = succa−1 B a . . b. The range (ran f ) is a . . b, and the domain (dom f ) is
a − (a − 1) . . b − (a − 1) or 1 . . 1 + b − a. Thus the cardinality is 1 + b − a, as stated
above.
Pictorially we have:
1 2 3 ··· b − a 1 + b − a
– – – ··· – –
↓ ↓ ↓ ↓ ↓
a a + 1 a + 2 ··· b − 1 b
fact that it exists. We introduce such sets as a basic type (or given set):
[ Places ]
or for several sets,
[ A, B, C ]
If one particular place is of interest, we could define
London : Places
or for more than one place (for example):
Oxford, Cambridge : Places
Oxford 6= Cambridge
It is important to specify that Oxford 6= Cambridge here if we want to ensure that the
two are distinct. Otherwise they could be the same place with different names (heaven
forbid!).
If we wish to be more precise we can use a data type definition. For example,
Methods could be defined as
Methods ::= Z | VDM | RAISE | B-Method
Here, the type Methods may take one of four unique values. More complicated data
types are possible. For example, we could define
N ::= zero | succhhNii
This is equivalent to defining
[N]
zero : N
succ : N N
{zero} ∩ ran succ = ∅
{zero} ∪ ran succ = N
Functions such as succ here are known as constructors. Such complications are
often not needed for many specifications. You are referred to Section 3.10 starting on
page 82 of [381] for more information on such free type definitions.
Question: What is the type of {i, j : N | i < j} ?
3.5.3 Sequences
Lists, arrays, files, sequences, trace histories are all different names for a single im-
portant data type. The important characterization is that the elements are indexed and
normally contiguously numbered.
Consider how we might store, for any pair (A, B) ∈ Places × Places, the least cost
paths from A to B, (i.e., the relation (A, B) - path). A common way to do this is
Chapter 3 A Brief Introduction to Z 49
to store it as a sequence, say under key (A, B), ordered lexically to aid in fast access.
This is an example of data refinement. A sequence has a 1st element, a 2nd element,
3rd element, etc. . . Sequence elements are numbered from 1 rather than 0 in Z since
this is usually more natural. If T is a set, we define the set of (finite) sequences with
elements of type T as follows:
seq T == {s : N →
7 7 T | dom s = 1 . . #s}
This denotes the set of (partial) functions from N to T whose domain is a finite segment
1 . . k of N. ‘. .’ denotes a number range as defined previously:
a . . b = {n : N | a ≤ n ≤ b}
We call such sequences T-valued sequences, or T sequences. Note that sequences
must have a finite (although arbitrary) length. If s ∈ seq T, the length of s is simply
the cardinality, #s, of s considered as a function. The empty sequence, s = ∅ has
#s = 0 and is normally written as
hi – the empty sequence
Like the empty set ∅, the empty sequence is typed.
If non-empty sequences are required, we use the notation
seq1 T == seq T \ {hi}
If injective sequences (i.e., sequences which contain no repetitions of elements in their
range) are needed, we use
iseq T == seq T ∩ (N
7 T)
The sequence containing just one element, s = {1 7→ x}, has #s = 1 and is written
as
hxi – a singleton sequence
In general the sequence {1 7→ x1 , 2 7→ x2 , . . . , n 7→ xn } is written in a shorthand form
as
hx1 , x2 , . . . , xn i – a multi-element sequence
Here are some examples of sequences using this notation:
h 11, 29, 3, 7 i ∈ seq primes
Some of the prime numbers, in no particular order. Perhaps they are ready to be
sorted into numerical order.
h J, O, N, A, T, H, A, N i ∈ seq CHAR
A string of characters. Note that unlike for sets enumerated using the (similar)
{a, b, c, . . .} notation, the two occurrences of ‘N’ are each distinct. The two ‘N’
elements of the set are in fact the maplets 3 7→ N and 8 7→ N which form dif-
ferent elements in the set representing the sequence. The same applies to the two
occurrences
- - of ‘A’.
h , ,
6 i ∈ seq Path
A list of possible paths between A and B.
50 Formal Specification and Documentation using Z
The length (and thus cardinality) of the three sequences above is 4, 7 and 3 respec-
tively.
Note that unlike sets, sequences can have several repeated elements. E.g.:
hEmmai =
6 hEmma, Emma, Emmai
Also, the order is significant:
hAlice, Emmai =
6 hEmma, Alicei
Concatenation
We concatenate sequences s, t ∈ seq T (or append t to the end of s) by
sat 1 . . (#s + #t) → T with elements
– the function
s(j) if 1 ≤ j ≤ #s
j 7→
t(j − #s) if #s < j ≤ (#s + #t)
More formally, we could define concatenation as
s a t = s ∪ ( − #s) o9 t
For another equivalent definition, see page 116 of [381].
Consider the concatenation of two sequences of length 5 and 3:
sat
z }| {
Diagrammatically: | {z } | {z }
s t
#s = 5 #t = 3
Laws
hi a s = s a hi = s
r a (s a t) = (r a s) a t
(r a s = r a t) ⇒ s = t
Prefix
Note that for s, t ∈ seq T, s ⊆ t is equivalent to ∃ r : seq T • s a r = t. Thus ⊆ applied
to a pair of sequences effectively checks that the left hand sequence is a prefix of the
right hand sequence. For example:
hM, Ai ⊆ hM, A, Ni (Freud’s theorem!)
hi ⊆ s hi is always a prefix of any sequence.
s⊆s A sequence is always a prefix of itself.
Chapter 3 A Brief Introduction to Z 51
Laws
If one sequence is the prefix of another and vice versa, the two sequences are identical:
(s ⊆ t ∧ t ⊆ s) ⇒ s = t
If a sequence is the prefix of a sequence which is the prefix of yet another sequence,
then the first sequence is also a prefix of this other sequence:
(r ⊆ s ∧ s ⊆ t) ⇒ r ⊆ t
If two sequences are a prefix of another sequence, then one of the two sequences must
be a prefix of the other. Note that these laws also apply to sets:
(r ⊆ t ∧ s ⊆ t) ⇒ (r ⊆ s ∨ s ⊆ r)
In Z, the relation s prefix t, defined in the Z toolkit (page 119 of [381]) can also be
used to check for a sequence prefix.
It is often useful to be able to extract the first or last element from a sequence in
specifications. The rest of the sequence may also be of interest. Four functions are
available for these operations. If s ∈ seq T and s 6= hi (i.e., s ∈ seq1 T):
head s = s(1) •◦◦◦◦◦ first element of sequence
last s = s(#s) ◦◦◦◦◦• last element of sequence
tail s = succ o9 ({1} −
C s) ◦••••• sequence without first element
front s = {#s} − Cs •••••◦ sequence without last element
It is best to avoid applying these functions to an empty sequence; for example, headhi
is undefined.
As an example, if the sequence s is hC, O, D, Ei (which is {1 7→ C, 2 7→ O, 3 7→
D, 4 7→ E} then
head s = C
last s = E
tail s = {0 7→ 1, 1 7→ 2, 2 7→ 3, 3 7→ 4, . . .} o9 {2 7→ O, 3 7→ D, 4 7→ E}
= {1 →
7 O, 2 7→ D, 3 7→ E}
= hO, D, Ei
front s = {4} −
C {1 7→ C, 2 7→ O, 3 7→ D, 4 7→ E}
= {1 7→ C, 2 7→ O, 3 7→ D}
= hC, O, Di
Exercise: State some laws concerning these operations. Try not to refer to [381]!
We could construct more general versions of front and tail if required for a particular
application, allowing the length of sequence required to be specified, using generic
construction:
52 Formal Specification and Documentation using Z
[T]
for ,
after : (seq T) × N → (seq T)
∀ s : seq T; n : N •
s for n = (1 . . n) C s ∧
s after n = ({0} − C succn ) o9 s
For example, these could be useful in extracting portions of files considered as a se-
quence of bytes. Note that for s ∈ seq1 T,
front s = s for (#s − 1)
tail s = s after 1
Here are some laws:
s for 0 = hi
s for #s = s
s after 0 = s
s after #s = hi
Reversal
If s ∈ seq T, the reverse of s is given by rev s. For example, the sequence, hD, O, Gi is
converted to hG, O, Di using the rev function!
Laws
revhi = hi
revhxi = hxi
rev(rev s) = s
rev(s a t) = (rev t) a (rev s)
For example
Distributed operations
Sometimes the concatenation of a sequence of sequences is useful:
a/hi = hi
a/ha, b, . . . , ni = a a b a . . . a n
and also
a/(s a hai) = (a/ s) a hai
For the actual formal definition of a/, see page 121 of [381].
Question: What is rev(a/hhN, A, Hi, hT, Ai, hN, Oi, hJii)?
Other distributed operators can also be defined for sequences if required for a particu-
lar specification. For example, a session of updating a database results in a sequence
of partial functions. We could define a distributed overriding operator in terms of the
standard dyadic overriding operator to generalize the overriding of a relation. See for
example, a definition on page 172. Informally:
⊕/ha, b, . . . , ni = a ⊕ b ⊕ . . . ⊕ n
Exercise: The composition operator ‘o9’ may also be generalized to a distributed com-
position operator ‘o9/’. Again, informally:
o
9/ha, b, . . . , ni = a o9 b o9 . . . o9 n
Write a formal definition for this. Can you think of an application for this operator in
a specification?
Disjointness and partitioning may be generalized from sequences to any indexed set
(i.e., S : I →
7 P T instead of S : seq P T).
54 Formal Specification and Documentation using Z
3.5.4 Orders
The Z toolkit can be extended as required for a particular application. For example, a
partial order, which is reflexive, antisymmetric, and transitive, may be a useful concept
in some specifications:
partial order[X] ==
{ R : X ↔ X | ( ∀ x, y, z : X •
xRx∧
(x R y ∧ y R x) ⇒ x = y ∧
(x R y ∧ y R z) ⇒ x R z ) }
This can be extended to define a total order, in which all elements are related:
total order[X] ==
{ R : partial order[X] | ( ∀ x, y : X •
x R y ∨ y R x)}
For example, it may be useful to model time as a total order in a particular specifica-
tion.
3.5.5 Summary
We have briefly covered numbers and then used these to define the notion of se-
quences, an important data structure in many specifications and data refinement. We
have also looked at ways in which Z lets us manipulate sequences.
This concludes the introduction to the mathematical notation of Z. Some lesser used
parts of Z (such as bags) have not been covered here, but are included from page 124
onwards in [381]. As you gain confidence in writing Z specifications, you should
investigate these other features of Z.
Using mathematics for specification is all very well for small examples, but for
more realistically sized problems, things start to get out of hand. To deal with this,
Z includes the schema notation to aid the structuring and modularization of specifica-
tions. We have seen an example of a schema box in passing. In the next section we
shall see how to combine such schemas to produce larger specifications.
3.6 Schemas
A boxed notation called ‘schemas’ is used for structuring Z specifications. This has
been found to be necessary to handle the information in a specification of any size.
We saw a brief example on page 32. Here is another example of a schema:
Book
author : People
title : seq CHAR
readership : P People
rating : People →7 0 . . 10
readership = dom rating
Chapter 3 A Brief Introduction to Z 55
This defines a single author, a book title, and a number of people who make up the
readership of a book (a set of people, as indicated by the ‘power set’ operator P in the
type declaration), together with their rating of the book (out of 10). The bottom half
of a schema optionally introduces extra constraints between the variables in the form
of predicates. Here, the readership is the same as the domain of the rating function.
The top half of the Book schema box defines a number of named variables with
associated constraints from which the type information can be mechanically derived.
Here seq CHAR is a subset of N → 7 7 CHAR (see the definition of seq on page 115 of
[381]), which itself is a subset of Z ↔ CHAR. This is the same as P(Z × CHAR) (see
page 95 of [381]). The expression 0 . . 10 implies a type of integer Z with the extra
constraint that the rating must take a value between 0 and 10. In fact this schema may
be ‘normalized’ into the following form:
Book
author : People
title : P(Z × CHAR)
readership : P People
rating : P(People × Z)
title ∈ seq CHAR
rating ∈ People →7 0 . . 10
readership = dom rating
Note that the predicates on separate lines in the second half of the schema above
are conjoined together by default. Here, the declarations use the most general types
possible for the components. These are the actual types for these components, which
could be used for type-checking purposes if required. Mentally calculating such types
can be a useful aid in understanding a specification.
Schemas are primarily used to specify state spaces and operations for the mathe-
matical modelling of systems. For example, here is a schema called StateSpace:
StateSpace
x1 : S1
x2 : S2
..
.
xn : Sn
Inv(x1 , . . . , xn )
Even more space can be saved using a horizontal formal of schema definition, which
is typically used if the entire definition can conveniently fit on a single line. E.g.:
b [x1 : S1 ; . . . ; xn : Sn | Inv(x1 , . . . , xn )]
StateSpace =
56 Formal Specification and Documentation using Z
This schema specifies a state space in which x1 , . . . , xn are the state variables and
S1 , . . . , Sn are expressions from which their types may be systematically derived. Z
types are sets – x1 , . . . , xn should not occur free in S1 , . . . , Sn , or if they do, they refer
instead to other occurrences of these variables already in scope (e.g., globally defined
variables). Inv(x1 , . . . , xn ) is the state invariant, relating the variables in some way for
all possible allowed states of the system during its lifetime.
Note that unlike in an ordered tuple, the variables in a schema are essentially un-
ordered – reordering them would give the same schema – and the variable names do
not come into scope until the bottom half of the schema. Thus any interdependencies
must be defined here. (A common mistake by initial users of Z is to define interdepen-
dencies in the declaration part, but a type-checker will very quickly detect this.)
The ‘Birthday Book’ is a well known example from Chapter 1 of Spivey’s widely used
book on Z [381]. It is a system for recording birthdays. It uses the following basic
types (or given sets):
[NAME, DATE]
BirthdayBook
known : P NAME
birthday : NAME →
7 DATE
known = dom birthday
The state variables are known (a number of people’s names) and birthday (unique
dates associated with each known person’s name). The ‘invariant’ property of this
schema is:
I.e., every known person has a birth date associated with them.
Z makes use of identifier decorations to encode intended interpretations. A state
variable with no decoration represents the current (before) state and a state variable
ending with a prime (0 ) represents the next (after) state. A variable ending with a
question mark (?) represents an input and a variable ending with an exclamation mark
(!) represents an output. A typical schema specifying a state change is the following
operation schema:
Chapter 3 A Brief Introduction to Z 57
Operation
x1 : S1 ; . . . ; xn : Sn
x10 : S1 ; . . . ; xn0 : Sn
i1 ? : T1 ; . . . ; im ? : Tm
o1 ! : U1 ; . . . ; op ! : Up
Pre(i1 ?, . . . , im ?, x1 , . . . , xn )
Inv(x1 , . . . , xn )
Inv(x10 , . . . , xn0 )
Op(i1 ?, . . . , im ?, x1 , . . . , xn , x10 , . . . , xn0 , o1 !, . . . , op !)
The entire state with its invariant is repeated for both the before (undashed) and after
(dashed) states. Fortunately schemas may be ‘included’ in other schemas, so this may
be written much more concisely than above in a real specification, reducing six lines to
a single included schema in the specification above in Spivey’s original specification
(see page 4 of [381]).
58 Formal Specification and Documentation using Z
abbreviates:
Operation
x1 : S1 ; . . . ; xn : Sn
x10 : S1 ; . . . ; xn0 : Sn
i1 ? : T1 ; . . . ; im ? : Tm
Pre(i1 ?, . . . , im ?, x1 , . . . , xn )
Inv(x1 , . . . , xn )
Inv(x10 , . . . , xn0 )
Op(i1 ?, . . . , im ?, x1 , . . . , xn , x10 , . . . , xn0 , o1 !, . . . , op !)
This use of one schema (∆StateSpace here) within another schema is called schema
inclusion, and is a useful and widely use structuring technique in Z. It adds all the state
components and the associated constraining predicates to the including schema. If any
component names match those already declared elsewhere, then their types must be
compatible and they map in top of each other. This can be useful for sharing of com-
ponents in the specification. The use of schema inclusion allows detailed declarations
of state components to be hidden in subsequent parts of a specification once they have
been declared and explained beforehand.
Chapter 3 A Brief Introduction to Z 59
Strictly, Inv(x10 , . . . , xn0 ) is also included as a predicate, but this is redundant because
of the second and third predicate clauses above.
An example of such a status operation is FindBirthday, which looks up a birthday
for a given name:
FindBirthday
known : P NAME
birthday : NAME →7 DATE
known0 : P NAME
birthday0 : NAME →7 DATE
name? : NAME
date! : DATE
name? ∈ known
known = dom birthday
known0 = known
birthday0 = birthday
date! = birthday(name?)
The precondition is name? ∈ known and the the operation part of the predicate is
date! = birthday(name?).
60 Formal Specification and Documentation using Z
StateSpace
x1 : S1 ; . . . ; xn : Sn
Inv(x1 , . . . , xn )
Operation
ΞStateSpace
i1 ? : T1 ; . . . ; im ? : Tm
o1 ! : U1 ; . . . ; op ! : Up
Pre(i1 ?, . . . , im ?, x1 , . . . , xn )
Op(i1 ?, . . . , im ?, x1 , . . . , xn , x10 , . . . , xn0 , o1 !, . . . , op !)
Operation
x1 : S1 ; . . . ; xn : Sn
x10 : S1 ; . . . ; xn0 : Sn
i1 ? : T1 ; . . . ; im ? : Tm
o1 ! : U1 ; . . . ; op ! : Up
Pre(i1 ?, . . . , im ?, x1 , . . . , xn )
Inv(x1 , . . . , xn )
(x10 = x1 ∧ . . . ∧ xn0 = xn )
Op(i1 ?, . . . , im ?, x1 , . . . , xn , x10 , . . . , xn0 , o1 !, . . . , op !)
FindBirthday
ΞBirthdayBook
name? : NAME
date! : DATE
name? ∈ known
date! = birthday(name?)
and
Operation2
y1 : T1 ; . . . ; yq : Tq
z1 : U1 ; . . . ; zn : Un
z01 : U1 ; . . . ; z0n : Un
Op2(y1 , . . . , yq , z1 , . . . , zn , z01 , . . . , z0n )
Operation1 o9 Operation2
x1 : S1 ; . . . ; xp : Sp
y1 : T1 ; . . . ; yq : Tq
z1 : U1 ; . . . ; zn : Un
z01 : U1 ; . . . ; z0n : Un
∃ z001 : U1 ; · · · ; z00n : Un •
Op1(x1 , . . . , xp , z1 , . . . , zn , z001 , . . . , z00n ) ∧
Op2(y1 , . . . , yq , z001 , . . . , z00n , z01 , . . . , z0n )
All the z01 , . . . , z0n after states in Operation1 which match z1 , . . . , zn before states in
Operation2 are combined and existentially quantified as a new intermediate state
z001 . . . z00n . The x1 , . . . , xp components in Operation1 and the y1 , . . . , yq components
in Operation2 are those do not match in this way (including any input and output
components). If any of these components match in a type-compatible way, they are
merged as for other standard schema operators such as conjunction.
AddThenFindBirthday
known : P NAME
birthday : NAME →7 DATE
known0 : P NAME
birthday0 : NAME →7 DATE
name? : NAME
date? : DATE
date! : DATE
∃ known00 : P NAME; birthday00 : NAME → 7 DATE •
known = dom birthday ∧
known00 = dom birthday00 ∧
name? ∈ / known ∧
birthday00 = birthday ∪ {name? 7→ date?} ∧
known00 = dom birthday00 ∧
known0 = known00 ∧
birthday0 = birthday00 ∧
name? ∈ known00 ∧
date! = birthday00 (name?)
There is a similar schema piping operator in Z which matches the outputs of the first
schema to the inputs of the second schema instead of the state components.
3.6.3 Properties
I.e., a FindBirthday operation after an AddBirthday, with the same name input to both,
outputs the same date as that input to the AddBirthday operation. This is the sort of
property that, if proved, provides an extra level of confidence that a specification is
correct, since it confirms our intuitions about the properties of the specifications that
we expect to hold. If a given desired property cannot be proved, this may well indicate
a flaw in the specification, which can then be rectified at an early stage before any
implementation has been started. Using informal design techniques, such errors are
not normally discovered until a later stage, such as coding, testing, or even after the
system has been delivered, with all the extra costs that this involves.
Note that Z as defined by Spivey [381] includes no standard way to write theo-
rems. In this book, we adopt the convention of writing ` p where p is some predicate.
Alternatively, d ` p is sometimes used to include universally quantified declarations
d.
3.7 Conclusion
This chapter has provided an extremely brief introduction to Z. Readers who still have
reservations about their understanding of Z would be well advised to read an introduc-
64 Formal Specification and Documentation using Z
tory textbook on Z before tackling the formal case studies presented in the rest of this
book. See page 244 for a list of such books.
The Z notation includes set-theoretic definitions in the form of an extensive mathe-
matical ‘toolkit’ as comprehensively presented in [381]. Much of Z as it is normally
used is defined using itself in this toolkit, and it is forming the main basis for the
proposed Z standard [79]. In addition, in may be desirable to create further toolkit
libraries for certain applications. For example, the inclusion of real numbers has been
considered [411].
It is important to remember than Z is based on first order logic. A common mistake
of novice Z users is to attempt to form relations and functions on predicates. This is
not legal in Z. In fact there is no predefined Boolean type in Z since it is normally
unnecessary. It is possible to define a binary valued type in Z if required, but often
there is a better way of approaching the specification if a developer finds him/herself
tempted to do this, unless it is explicitly needed in a certain application (e.g., see
Chapter 8). A Z type-checker will quickly discover any attempt by a specifier to bend
the rules of Z and try to use it in a higher order manner, as in HOL [178] for example.
However, unfortunately there are some untype-checked Z specifications are incorrect
because of this problem.
Z has been a relatively fluid language during its lifetime. The lack of tools in the
early days of its development was a positive asset since it allowed new ideas to be tried
experimentally with little overhead. However as Z has become more established, and
used increasingly in industry, the need for a standard notation to allow mechanical tool
support has increased. The current de facto standard widely used by academics and
industrial users alike, is that laid down in Spivey’s Z Notation: A Reference Manual
(often know as the Z Reference Manual, or ‘ZRM’ for short). This is now in its 2nd
edition [381]. This is the notation generally used in this book. The development
of an international Z standard is in progress [79]. Once this is accepted it is likely
to supersede [381] since tool builders will probably then adopt it as the notation of
choice.
This completes the introductory part of the book. As previously mentioned, a com-
prehensive introduction to Z is impossible in a single chapter. If you still require
further grounding in the use of Z, please consult one or more of the numerous Z text-
books available (as listed on page 244) before proceeding with the rest of the book.
Subsequent the chapters present a number of case studies of specifications in Z, nearly
all of implemented (and hopefully useful!) systems.
II
Network Services
The use of the Z notation to document network services in a formal and precise manner
is presented. In Chapter 4, a general introduction to User and Implementor Manuals
is given, using a simple service as an example. A manual for a more substantial file
system service is included in Chapter 5.
Chapter 4
Documentation using Z
The Z notation has been applied to the formal specification of resource managers
or ‘services’ within a distributed system. A formal description gives a more precise
understanding of the behaviour of a service and, when combined with informal text,
is sufficiently readable for the specification to be used for documentation purposes.
Two types of manual have been produced, one presenting the external view of the
service (for users) and another describing the internal view (for implementors).
A common service framework deals with standard aspects of services. Parts of a
simple User and Implementor Manual are presented as an example.
4.1 Introduction
The aim of this chapter is to introduce and illustrate a formal style of specifying and
documenting system components. The components considered in the study are ser-
vices within a distributed computing system [57].
First an introduction to the style of specification is presented. It considers how a
service can be modelled in the Z specification language, and the way in which such
specifications can be used in documenting both the user’s and the implementor’s view
of a service. Next an example of a service specification is given. This example de-
scribes a very simple service, the Reservation Service, and serves to demonstrate the
style of User Manual developed by the project. Additionally a simple example of an
implementation-oriented specification in the form of an Implementor Manual for the
Reservation Service is presented. Finally some experience gained from the work is
discussed.
More complex services have been documented and implemented but these are not
presented here to keep the length to a manageable size. Chapter 5 presents a single
more realistically sized manual.
The Reservation Service was developed as a part of the Distributed Computing Soft-
ware (DCS) Project at the Programming Research Group within the Oxford University
Computing Laboratory. The goal of the project was to investigate the use of formal
techniques in the design and documentation of services for a loosely-coupled dis-
tributed operating system, based on the model of autonomous clients having access to
a number of shared facilities. Several services have been designed and documented in
the manner described here, and implementations of them have been provided for, and
used by, members of the Programming Research Group.
67
68 Formal Specification and Documentation using Z
A number of monographs were produced by the project [55, 56, 172]. These pro-
vide more information for those interested in the details of the work of the project.
In particular, the User and Implementor Manuals for the Reservation Service and a
(much larger) Block Storage Service, together with the Common Service Framework,
covering standard facilities such as authentication and accounting, are presented in
their entirety.
4.2 Motivation
It is fundamental to the design of any complex artefact, and of computer systems in
particular, that an appropriate means of describing and communicating the design is
used.
A very important line of communication is between the designer and the user of the
system. It is only if this communication is accomplished satisfactorily that the designer
can have any expectation of meeting the requirements of the user and, likewise, the
user have any expectation of being able to make proper use of the finished product.
No less important is the communication from the designer to the implementor of
the system. This is necessary to ensure that the finished product does indeed have the
characteristics that the designer specified.
The aim of the work described here is the improved communication between de-
signer, user and implementor which can be achieved by the use of formal specification
in the design and documentation of computer systems.
4.2.2 Documentation
AOP - AS0
User view: AS
Rel Rel0
COP - CS0
Implementor view: CS
operation COP must, given an initial state CS which relates to AS according to Rel,
produce a new state CS0 which relates to AS0 according to Rel0 . This can be expressed
more formally as:
∀ AS; CS • pre AOP ∧ Rel ⇒ pre COP
∀ AS; CS; CS0 • pre AOP ∧ COP ∧ Rel ⇒ (∃ AS0 • AOP ∧ Rel0 )
Note that input and output variables have been ignored in the above for simplicity of
presentation. For a fuller treatment, see page 138 of [381].
The ‘pre ’ schema operator gives the precondition of a schema in which all the after
(dashed) state and output components (ending with ‘!’) are existentially quantified.
The concrete state is thus considered as a data refinement of the abstract state, and
each of the concrete operations must model the same behaviour on the concrete state
as the corresponding abstract operation does on the abstract state.
The relationships between the two models can be illustrated as in Figure 4.1.
The manuals make use of some definitions from the Common Service Framework.
In particular, some given sets of data values are not formally elaborated further:
[UserNum, Report]
UserNum is the set of numbers which identify system users; Report is the set of re-
ports showing the outcome of an operation. Two individual unique special users are
assumed:
ManagerNum, GuestNum : UserNum
ManagerNum 6= GuestNum
ManagerNum is the identity of the manager of a service; GuestNum is the identity
of the guest (unauthenticated) user.
Time and intervals of time may be modelled are natural numbers for convenience,
to allow standard arithmetic operations to be available on them:
Time == N
Interval == N
ZeroInterval == 0
Time is the set of date/time instants and Interval is the set of time intervals between
such instants. ZeroInterval is a interval with no duration.
Reservations == {r : UserNum →
7 7 Time | #r ≤ Capacity}
(The above is an abbreviation definition, using a finite partial function from UserNum
to Time.)
The state of the Reservation Service records the shutdown time most recently set by
the service manager (shutdown) and the set of current reservations (resns). The guest
user cannot make reservations.
RS
shutdown : Time
resns : Reservations
GuestNum ∈
/ dom resns
(RS is a schema with two declarations and a single predicate. This is a method of
textually collecting together pieces of mathematics to aid structuring of specifications.)
Initially the shutdown is set to a default value and there are no reservations.
InitShutdownTime : Time
InitRS
RS0
shutdown0 = InitShutdownTime
resns0 = ∅
(Schemas may be included in other schemas. Declarations are merged (matching dec-
larations combine into one), and predicates are conjoined. If a schema name is deco-
rated (e.g., the 0 above), all the components are also decorated. Note that predicates
on successive lines in a schema are conjoined by default.)
The service is in its initial state every time it is powered up.
(‘!’ signifies outputs and ‘?’ signifies inputs. Φ is just part of the name of the schema,
used here to indicate an incomplete specification.)
Operations may change the state of the Reservation Service.
b RS ∧ RS0 ∧ ΦBasicParams
∆RS =
(∆RS is defined as a horizontal as opposed to a vertical schema definition here. ∆
74 Formal Specification and Documentation using Z
4.5.3 Reports
There are a number of possible error reports from the operations, all of which have
different values:
SuccessReport,
NotAvailableReport,
TooManyUsersReport,
NotManagerReport,
NotKnownUserReport : Report
hSuccessReport, NotAvailableReport, TooManyUsersReport,
NotManagerReport, NotKnownUserReporti ∈ iseq Report
The report! output parameter of each operation indicates either that the operation
succeeded or suggests why it failed.
Success indicates successful completion of an operation.
Success
report! : Report
report! = SuccessReport
If a reservation cannot be made due to early shutdown, the shutdown time itself is
returned in until!. Note that a reservation of zero interval will not cause this error.
NotAvailable
ΞRS
interval? : Interval
until! : Time
interval? 6= ZeroInterval
shutdown < now + interval?
until! = shutdown
report! = NotAvailableReport
Chapter 4 Documentation using Z 75
The service has finite capacity for recording reservations; the report TooManyUsers
occurs when that capacity would be exceeded. The report cannot occur if the client
has a reservation (since it is overwritten by the new one).
TooManyUsers
ΞRS
#resns = Capacity
clientnum ∈
/ dom resns
report! = TooManyUsersReport
Some operations can only be executed by the service manager, and return an error
otherwise:
NotManager
clientnum : UserNum
report! : Report
clientnum 6= ManagerNum
report! = NotManagerReport
The guest user cannot make reservations, and an error is returned if this user tries to
do so:
NotKnownUser
clientnum : UserNum
report! : Report
clientnum = GuestNum
report! = NotKnownUserReport
RESERVE
Abstract
Reserve ( interval? : Interval;
until! : Time;
report! : Report )
A reservation is made for a period of time (interval?), and returns the expiry time of
the new reservation (until!).
A client can cancel a reservation by making a new reservation in which interval? is
zero; this will then be removed by the next scavenge.
Definition ∗
Reservesuccess
∆RS
interval? : Interval
until! : Time
until! = now + interval?
shutdown0 = shutdown
resns0 = resns ⊕ {clientnum 7→ until!}
Reports †
b (Reservesuccess ∧ Success)
Reserve =
⊕ TooManyUsers
⊕ NotAvailable
⊕ NotKnownUser
∗ In the Definition section, ⊕ is used for relational overriding. Any existing entry under clientnum in resns
is removed and a new entry with value until! is added.
† In the Reports section, ⊕ is applied to schemas for schema overriding. Mathematically, this can be
defined as A ⊕ B = b (A ∧ ¬ pre B) ∨ B, where pre B is the precondition of the B schema in which all
after state and output components have been existentially quantified. In practice this means that the error
conditions are ‘checked’ in reverse order.
78 Formal Specification and Documentation using Z
Money == N
ΦParams
ΦBasicParams
op? : Op
cost! : Money
There is a fixed cost for each different successful operation. All clients who make a
reservation will also be charged an amount depending on the requested interval.
ReserveOp, SetShutdownOp, StatusOp : Op
ReserveCost, TimeCost, SetShutdownCost,
StatusCost, ErrorCost : Money
hReserveOp, SetShutdownOp, StatusOpi ∈ iseq Op
RSTariff
ΦParams
interval? : Interval
op? = ReserveOp ⇒ cost! = ReserveCost + (TimeCost ∗ interval?)
op? = SetShutdownOp ⇒ cost! = SetShutdownCost
op? = StatusOp ⇒ cost! = StatusCost
cRS
shutd : Time
users : UserArray
times : TimeArray
(users −
B {Unused}) ∈ (Index
7 UserNum)
B performs range anti-restriction of a function (in this case, all Unused entries are
(−
removed from the users array), and 7 indicates a partial injection or one-to-one func-
tion.)
Each authentic client can have at most one entry in the users array, all other entries
being unused.
Initially the shutdown time has the default value and all the entries in the user array
are unused. (It will not matter what values are held in the time array.)
cInitRS
cRS0
shutd0 = InitShutdownTime
users0 = (λ s : Index • Unused)
This completes the specification of the concrete state, its initialization. and its change
of state in general terms.
The four service operations are redefined in this manual in terms of the refined con-
crete state. As in the User Manual, the description of each operation has three sections,
entitled Abstract, Definition and Reports.
Each schema definition may be conveniently implemented as a procedure in the
final program. Again, only the definition of the Reserve operation is included here.
Note that the TooManyUsers report schema has been directly incorporated in the im-
plementation of this operation.
The other error reports remain similar, except that the abstract state is replaced by
the concrete state:
Chapter 4 Documentation using Z 81
cNotAvailable
ΞcRS
interval? : Interval
until! : Time
interval? 6= ZeroInterval
shutd < now + interval?
until! = shutd
report! = NotAvailableReport
cNotKnownUser
ΞRS
clientnum = GuestNum
report! = NotKnownUserReport
82 Formal Specification and Documentation using Z
Abstract RESERVE
4.7 Experience
The Reservation Service is one of a number of services designed by the project. Other
services include a Time Service, a Block Storage Service and a File Service. Ser-
vices can act as clients to other services if required. For example, the File Service is
designed to make use of the Block Storage Service. Each service is designed to be
simple and to perform one function. Taking the File Service again, this does not sup-
ply human readable file names or any file organization. If this is needed, a Directory
Service could be used.
This section details some of the experiences of the project. Problems and advantages
of using formal methods, and Z in particular, are discussed.
using Z [171, 246, 248, 308, 400, 423, 429, 431, 440, 441] and also data refinement
[208, 238, 294]. Parallel refinement, linked with CSP [215], has also been consid-
ered [427, 438], as have object-oriented aspects [19, 257, 420]. The correctness of
real programming languages, such as Ada, with respect to a Z specification is also
an important issue [366]. In the case of safety-critical applications, timing can be-
come an important issue for hard real-time systems where it is an essential part of the
specification that the deadlines be met [271, 272].
Work at Oxford and elsewhere has considered the step from specification into pro-
gramming language in more detail [295, 299]. For example, the Reserve operation has
been systematically refined into Dijkstra’s language of weakest preconditions [296].
The DCS project concentrated on the ‘architectural’ aspects of system design, taking
a top-down approach in which the structure of the implementation was of greatest
concern.
the issues of errors in the implementation of services or in the network over which
they are accessed.
sensible approach is to return some standard error value in these cases. Output param-
eters may be checked for this value by the client if desired.
is the reason it was not included in the original version of the service. However it is
likely that its inclusion would have prevented the problem just described from arising.
4.8 Conclusions
It is possible to use a formal specification language successfully both to guide the
design of system components and also to document the resultant design. The specifi-
cation language Z, after some experimentation to devise an appropriate style of man-
ual presentation, has been used in both User and Implementor Manuals for system
services.
As well as being more precise than conventional informal documentation, such for-
mal designs are necessary if the correctness of implementations are of concern, though
proof of correctness is still laborious.
The initial desire to present the formal specifications as part of the manuals for the
services has forced the designs to be simple, and has concentrated our attention on
easing the presentation of formal notation.
In Chapter 5, immediately following this chapter, a more substantial example of a
User Manual is provided.
Chapter 5
This chapter presents the User Manual for a more substantial network service
along the lines described in Chapter 4. The service provides file storage facilities to
clients via a number of remote procedure calls. These are modelled as operations
in the Z specification provided here.
MaxFileSize : N
As well as containing the client’s data, the file records as its owner the user number
of the client who submitted it, and it records the time of its original creation and last
update. Whenever a file is created, an expiry time must be given by the client; it is the
time until which the service is obliged to store the file. After this time, a file is said
to have expired, and can be discarded by the service without notification of the client.
89
90 Formal Specification and Documentation using Z
This expiry time may be changed later if required. The creation time, last update time
and expiry time are always ordered:
≤ : Time ↔ Time
( ≤ ) ∈ total order
Here total order defines a total order on Time (see page 54).
A file identifier will be issued by the service when the file is created, chosen from a
set of such identifiers:
[FileId]
This becomes the client’s reference to the file. Any subsequent operations on the file
will require this identifier. Operations which update the file contents will return a new
name. Hence files are immutable in the sense that a known valid file identifier will
either access a single fixed file or return an error if it has been destroyed.
The service contains a mapping from file identifiers to files; it also contains a finite
set of new file identifiers which have not yet been issued. When a new identifier is
issued, it is taken from this set. There is a special NullFileId which is never issued by
the service.
NullFileId : FileId
FS
files : FileId →
7 7 File
newids : F FileId
newids ∩ dom files = ∅
NullFileId ∈
/ newids
NullFileId can be used by clients’ applications to indicate ‘no file’ (similarly to the use
of the nil pointer in a programming language).
Initially there are no files, and all identifiers except the NullFileId are potentially
available:
InitFS
FS0
files0 = ∅
newids0 = FileId \ {NullFileId}
Each file storage service operation can only be performed by an authentic client:
clientnum : UserNum
During an operation, the service can ask the time service for the current time:
now : Time
Every operation the service can perform for a client provides a report as output, nor-
mally SuccessReport (see later):
report! : Report
Chapter 5 A File Storage Service 91
Finally, any identifier issued by an operation is removed from the set of new ids, and
so can never be issued again:
newids0 = newids \ dom files0
These general aspects of operations on the file storage service are gathered together in
a single schema:
∆FS
FS
FS0
clientnum : UserNum
now : Time
report! : Report
newids0 = newids \ dom files0
Sometimes the state of the file storage service is left unaffected by an operation, par-
ticularly if an error is detected or it is a status operation:
b [∆FS | θFS0 = θFS]
ΞFS =
Many file storage service operations require an existing file id? to be supplied by the
user. The File details are then available to the operation. A partially specified schema
is used to include this information for all operations which take an id? as input:
ΦFileId?
∆FS
id? : FileId
File
θFile = files id?
All operations which create a new file return a new file id!. The new File0 details are
then available to the operation. Guest users cannot create files. The client owns the
new file which has been updated now. The file is added to the set of files stored by
the service. Another partial schema includes all this information for operations which
produce a file id! as output:
ΦFileId!
∆FS
id! : FileId
File0
clientnum 6= GuestNum
owner0 = clientnum
updated0 = now
id! ∈ newids
files0 = files ∪ {id! 7→ θFile0 }
Some of the file operations access sections of the file contents. Three functions are
useful for these definitions:
92 Formal Specification and Documentation using Z
[B]
after ,
for : (seq B) × N → (seq B)
shifted : (seq B) × N → (N →7 B)
∀ s : seq B; n : N •
s after n = ({0} − C succn ) o9 s ∧
s for n = (1 . . n) C s ∧
s shifted n = succ−n o9 s
Intuitively, an operation may access the contents of a file after a certain position, for
a given number of bytes. Additionally, it is possible to update the contents of a file
using data which has been shifted by a specified offset.
It is possible for ‘holes’ to be created in a file’s contents which have never been
previously set to any value if data is written to a file at a position after its current
length or the file length is set to be greater than the current length. A Background
value will be supplied by the service if such a location is accessed subsequently.
Background : ByteVal
holes : seq ByteVal
dom holes = 1 . . MaxFileSize
ran holes = {Background}
Note that a file size ranges from zero up to a maximum size.
Size == 0 . . MaxFileSize
NoSuchFile
Chapter 5 A File Storage Service 93
NoSuchFile
ΞFS
id? : FileId
id? ∈
/ dom files
report! = NoSuchFileReport
This report is given if there is no file stored under id?; note that this may be because
the file expired and has been scavenged.
NoSpace
NoSpace
ΞFS
report! = NoSpaceReport
A new file cannot be created when the service’s storage capacity is exhausted. The file
storage service capacity is not modelled here, but it is guaranteed that the state of the
service will be unaffected in this case.
NotOwner
NotOwner
ΞFS
owner : UserNum
owner 6= clientnum
report! = NotOwnerReport
A client operations which destroys a file must be performed by the owner of the file.
NotKnownUser
This is defined in the Common Service Framework document [55].∗ In addition, the
Common Service Framework defines:
IsKnownUser
clientnum : UserNum
clientnum 6= GuestNum
NEWFILE
Abstract
NewFile ( expires? : Time;
id! : FileId;
report! : Report )
A file is formed with a specified expiry time, and is stored by the service under the
new file id!. The new file contains no data.
Definition
NewFile
∆FS
expires? : Time
ΦFileId!
created0 = now
expires0 = max{expires?, now}
contents0 = hi
The owner of the file is the client. Guest users cannot create new files.
If an expiry time in the past is given, then the expiry time of the file is set to now.
A new identifier is chosen which has never before been issued, and the new empty file
is stored under that id.
Reports
b (NewFile ∧ IsKnownUser ∧ Success)
NewFile1 =
⊕ NoSpace
⊕ (ΞFS ∧ NotKnownUser)
96 Formal Specification and Documentation using Z
WRITEFILE
Abstract
WriteFile ( id? : FileId;
offset? : Size;
data? : Data;
id! : FileId;
report! : Report )
An existing file with the given id? is updated with the new data? at the specified offset?
in the file to produce a new file with a new id!. The original file is unaffected.
Definition
WriteFile
∆FS
ΦFileId?
offset? : Size
data? : Data
ΦFileId!
created0 = created
expires0 = expires
contents0 = (holes for offset?)⊕
contents⊕
Size C (data? shifted offset?)
The creation and expiry times of the updated file are the same as the original file.
Any client apart from the guest user may write to a file. The owner of the new file is
the client.
A new identifier is chosen which has never previously been issued, and the new file is
stored under that id.
The new file will contain ‘holes’ if the offset given is past the end of the existing file.
Reports
b (WriteFile ∧ IsKnownUser ∧ Success)
WriteFile1 =
⊕ NoSpace
⊕ NoSuchFile
⊕ (ΞFS ∧ NotKnownUser)
Chapter 5 A File Storage Service 97
READFILE
Abstract
ReadFile ( id? : FileId;
offset? : Size;
length? : Size;
data! : Data;
report! : Report )
Data at the specified offset? and of the given length? in the file called id? is returned.
Definition
ReadFile
ΞFS
ΦFileId?
offset?,
length? : Size
data! : Data
data! = contents after offset? for length?
DESTROYFILE
Abstract
DestroyFile ( id? : FileId;
report! : Report )
The file stored under id? is removed from the service.
Definition
DestroyFile
∆FS
ΦFileId?
clientnum = owner
files0 = {id?} −
C files
FILESTATUS
Abstract
FileStatus ( id? : FileId;
owner! : UserNum;
created! : Time;
updated! : Time;
expires! : Time;
length! : Size;
report! : Report )
The status of the file stored under id? is returned to the client.
Definition
FileStatus
ΞFS
ΦFileId?
owner! : UserNum;
created!,
updated!,
expires! : Time;
length! : Size
owner! = owner
created! = created
updated! = updated
expires! = expires
length! = #contents
SETFILEEXPIRY
Abstract
SetFileExpiry ( id? : FileId;
expires? : Time;
id! : FileId;
report! : Report )
An existing file stored under id? is used to created a new file with a new id! and a new
expiry time.
Definition
SetFileExpiry
∆FS
ΦFileId?
expires? : Time
ΦFileId!
created0 = created
expires0 = max{expires?, now}
contents0 = contents
SETFILELENGTH
Abstract
SetFileLength ( id? : FileId;
length? : Size;
id! : FileId;
report! : Report )
The length of the file stored under id? is changed to length?.
Definition
SetFileLength
∆FS
ΦFileId?
length? : Size
ΦFileId!
created0 = created
expires0 = expires
contents0 = (holes ⊕ contents) for length?
A new identifier is chosen which has never previously been issued, and the new file is
stored under that identifier.
The new file contains ‘holes’ after the previous contents if the new length? is greater
than the previous length of the file.
Reports
b (SetFileLength ∧ IsKnownUser ∧ Success)
SetFileLength1 =
⊕ NoSpace
⊕ NoSuchFile
⊕ (ΞFS ∧ NotKnownUser)
102 Formal Specification and Documentation using Z
Definition
ScavengeFile
ΦFileId?
clientnum = FileService
expires < now
files0 = {id?} −
C files
5.6 Security
The service provides limited security in two areas; in both cases it depends on certain
values being chosen from such a large set that they are hard to guess.
A client may not access a file unless he knows its id, and file ids are hard to guess.
The identifier of any file is initially known only to its creator; the service will never
tell any client the identifier of a file he does not own.
104 Formal Specification and Documentation using Z
Tariff
∆FS
op? : Op
ΦFileId?
ΦFileId!
data! : Data
idset! : F FileId
cost! : Money
report! = SuccessReport ⇒
op? = NewFileOp ⇒ cost! = NewFileCost
op? = WriteFileOp ⇒ cost! = WriteFileCost
+ StoreByteCost ∗ (expires0 − updated0 ) ∗ #contents0
op? = ReadFileOp ⇒ cost! = ReadFileCost + ReadByteCost ∗ #data!
op? = DestroyFileOp ⇒ cost! = DestroyFileCost
− StoreByteCost ∗ (expires0 − updated0 ) ∗ #contents0
op? = FileStatusOp ⇒ cost! = FileStatusCost
op? = SetFileExpiryOp ⇒ cost! = SetFileExpiryCost
+ StoreByteCost ∗ (expires0 − expires) ∗ #contents0
op? = SetFileLengthOp ⇒ cost! = SetFileLengthCost
+ StoreByteCost ∗ (expires0 − updated0 )
∗ (#contents0 − #contents)
report! ∈ {NoSuchFileReport, NoSpaceReport, NotOwnerReport,
NotKnownUserReport} ⇒ cost! = FSErrorCost
Files may be destroyed only by their owners, and user identifiers are hard to guess.
Files may be updated, but this creates a new file with a new file id. The original file
is left unaffected. Files are only removed from the service when they are destroyed or
after their expiry time has passed.
III
UNIX Software
The UNIX operating system is widely used on workstations throughout the world.
Here, two pieces of software designed to run under UNIX are presented. In Chap-
ter 6 a text justification tool is formalized. An event-based input system designed for
workstations is presented in Chapter 7.
Chapter 6
sn = s a (s(n − 1))
109
110 Formal Specification and Documentation using Z
This definition will prove useful in the subsequent specification in this chapter. A
number of theorems apply to rep:
s : seq X ` s0 = hi
s : seq X ` s1 = s
n:N ` hin = hi
s : seq X; n : N ` #(sn) = #s ∗ n
s : seq X; n : N1 ` ran(sn) = ran s
s : seq X; n : N ` ∀m : N | m < n •
(sn) after (#s ∗ m) for n = s
Similarly the right-hand end of the line can be aligned, again if it is not too long.
Corresponding functions which clip the line first may also be defined.
left,
centre,
right : N → LINE → LINE
∀ n : N; l : LINE •
left n l = left0 n (clip l) ∧
centre n l = centre0 n (clip l) ∧
right n l = right0 n (clip l)
6.2.2 Documents
TEXT
text : DOC
b TEXT ∧ TEXT 0
∆TEXT =
The left, centre and right functions may be combined and selected using an option to
define which operation is required.
POS0
∆TEXT
option? : Option
column? : N
option? = LeftOption ⇒ text0 = text o9 (left column?)
option? = CentreOption ⇒ text0 = text o9 (centre column?)
option? = RightOption ⇒ text0 = text o9 (right column?)
In the previous section, it has been assumed that all the characters in lines are printable
characters (of the same printing width). In practice, an additional tab character is often
used for horizontal tabbing.
6.3.1 Tabs
The horizontal tab may be included in the character set as a new unique character:
tab : CHAR
tab 6= space
The visual effect of this special tab character is to ‘tabulate’ to the next tab column
position from the current position. This normally occurs at, for example, every eighth
column under UNIX. The distance between tab column positions is always greater than
one character position. Otherwise it would be equivalent to a space, and thus of little
use.
tabsize : N
tabsize > 1
The tab character introduces additional complication into the specification of manip-
ulation of text files. We shall now consider some functions useful for specifying such
manipulation.
Below is a generic function which splits a sequence into a series of segments of a
given non-zero length. Flattening these segments gives the original sequence. The last
segment may be of smaller size than the rest.
Chapter 6 A Text Formatting Tool 113
[X]
split : (seq X) × N1 → seq(seq X)
∀ s : seq1 X; n : N1 ; ss : seq1 (seq1 X) •
hi split n = hi ∧
s split n = ss ⇔
a/ ss = s ∧
(∀ t : seq X | t ∈ ran(front ss) • #t = n) ∧
0 < #(last ss) ≤ n
The trailing spaces of a line segment can be converted to a tab if the line segment
has the length of the distance between tab column positions. There should also be
more than one trailing space since this will reduce the length of the line and make the
substitution using a tab character worthwhile.
addtab : LINE →
7 LINE
∀ l : LINE | tab ∈
/ ran l •
(#l = tabsize ∧ #(clipright l) < #l − 1) ⇒
addtab l = (clipright l) a htabi ∧
(#l 6= tabsize ∨ #(clipright l) ≥ #l − 1) ⇒
addtab l = l
These functions may be combined together to convert spaces in a line to tabs where
appropriate:
unexpand : LINE →
7 LINE
∀ l : LINE | tab ∈
/ ran l •
unexpand l = a/((l split tabsize) o9 addtab)
This function should only be applied to lines not containing tabs and in this case
always reduces the length of the line, or leaves it the same.
` ∀ l : LINE | tab ∈
/ ran l • #(unexpand l) ≤ #l
Now consider a function to cut a sequence into a series of segments after each occur-
rence of a non-empty pattern.
[X]
cut : (seq X) × (seq1 X) →
7 seq(seq X)
(s a p a t) cut p = hs a pi a (t cut p)
Note that combining these segments back together again results in the original se-
quence:
114 Formal Specification and Documentation using Z
6.3.2 Lines
A document may be implemented by separating lines with a non-empty unique new-
line character sequence:
nl : seq1 CHAR
space ∈
/ ran nl
tab ∈
/ ran nl
These characters are not normally printable. For example, under UNIX this sequence
Chapter 6 A Text Formatting Tool 115
normally consists of the ASCII line-feed ‘control’ character. Under some other op-
erating systems it can consist of a combination of the carriage return and line-feed
characters. The characters should not occur within any line.
Consider a function which combines a sequence of segments using another se-
quence as a terminator for each of the segments.
[X]
comb : (seq(seq X)) × (seq X) → seq X
∀ s, p : seq X; ss : seq(seq X) •
hi comb p = hi ∧
hsi comb p = s a p ∧
By using a terminator rather than a separator the empty sequence (e.g., an empty
document) and a sequence containing the empty sequence (e.g. a document containing
a single empty line) may be differentiated.
p : seq X ` hi comb p = hi
[X]
sep : (seq X) × (seq1 X) → seq(seq X)
∀ s : seq X; p : seq1 X; ss : seq(seq X) •
s sep p = ss ⇔
ss comb p = s ∧
( ∀ t : seq X | t ∈ ran ss • ¬ (p ⊆ t) )
Note that the sequence to be separated must be terminated with the pattern or be empty
to be valid.
6.4 Files
A UNIX file is implemented as a sequence of characters [298], possibly containing tab
characters and newline sequences.
On input, a number of such files are to be converted into a single document without
tab characters or newline sequences.
116 Formal Specification and Documentation using Z
PrePOS0
TEXT
input? : seq FILE
PostPOS0
blanks? : Blanks
output! : FILE
TEXT 0
blanks? = Yes ⇒ output! = text0 comb nl
blanks? = No ⇒ output! = (text0 o9 unexpand) comb nl
These schemas may be combined to produce a new specification for the behaviour of
an implementation of the tool under UNIX.
6.5 Conclusion
This specification is based on a simple text processing tool which was written in the
programming language C [244] for use under the UNIX operating system. There are
some differences, but these and the manual page for this tool are included on page 118
for comparison.
Of course, normally a formal specification should be written before an implemen-
tation is produced. In this case this was not so because the author was not enlightened
when he wrote the original program some years ago. However there are still bene-
fits in producing a post hoc specification. This can be useful if a product is to be
re-engineered [319]. It can also help in improving the documentation of an existing
system [41, 80].
This chapter shows that text processing concepts may be documented using a for-
mal notation. By formalizing a system, ambiguity and misunderstanding are reduced.
Additionally, reasoning about the properties of the system becomes easier and can be
done with more confidence. Software developed from formal specifications is likely
to contain less errors. Studies on industrially sized examples of software development
have confirmed this view [247]. For these reasons, it is hoped that formal specifica-
tion will become more widely used in the field of practical software engineering in the
future.
The specification was previous published as an article [44]; it is included by kind
permission of the Institution of Electrical Engineers (IEE), UK.
Chapter 6 A Text Formatting Tool 117
An Event-based Input
System
In this chapter a design is given for an event-based input system for use on graphics
workstations that overcomes problems associated with some earlier designs. An
interface is specified which allows a client to select events to be queued from the set
of those available, get events from the input queue, put events in the input queue,
flush the input queue, and connect a set of polled events to a queued event. The
system has been designed with the intention of being implementable on a number
of systems and has also been formally specified using the Z specification language.
The system has been implemented on UNIX workstations.
7.1 Motivation
Many existing input systems have been based on the design of a particular device or
subsystem and/or have been specialized to the needs of a particular window system.
This has several problems which are discussed in [80]. The event queue system is
independent of any particular application or window system. It provides a set of gen-
eral purpose interfaces and is extensible to accommodate new input devices and event
types. This results in a system that is useful to a diverse range of applications.
The event queue is a system module analogous to the UNIX operating system [37]
tty handler for dealing with the standard ASCII terminal user interface. It provides
a set of procedures and data structures which a physical device driver, or client (user
process) may access. The event queue provides a set of logical devices with fixed
semantics. A given logical device abstracts from the large variety of physical devices
which may possibly implement it. The event queue system was first implemented
under UNIX on a large VAX system (11/785) with a large variety of attached input
devices, and later on MicroVAX II workstations [80].
Several existing systems were considered in the design of the present system. Short-
comings of existing input systems (such as those associated with the X Window Sys-
tem [357, 358, 359]) influenced this design.
In this chapter, Z is used to describe the operation of the system formally. An ab-
stract state of the system is presented, and then the effect of individual library routines
on the state is given. In addition, the corresponding C programming language [244]
declarations are included in italics before the formal description where appropriate to
aid those familiar with the C programming language.
119
120 Formal Specification and Documentation using Z
char == 0 . . 27 − 1
short == −215 . . 215 − 1
int == −231 . . 231 − 1
unsigned char == 0 . . 28 − 1
unsigned short == 0 . . 216 − 1
unsigned int == 0 . . 232 − 1
Event
device : qDevice
value : qValue
There are three different types of device in the system described here: button, valuator
and keyboard. Valuators may be absolute or relative.
qType == unsigned char
event will be either 0 indicating that the button went up, or 1 indicating that the button
went down. Valuator devices have a range value associated with them. For example
MOUSEX, TABLETY, KNOB15, or CLOCK are valuator devices. Valuator devices
may be relative or absolute. For example we might have a MOUSEX device which
returns absolute mouse x positions, or a MOUSEDX device which returns relative
mouse x positions (deltas) or both. Keyboard devices return character code values.
For example, the device ASCIIKEYBOARD is a device which returns ASCII values in
the low order 7 bits of qValue.
The conceptual state of the system is introduced briefly here. Each component is
covered more fully when the operations are introduced.
The state of the system includes a finite number of devices. Each of these has a type
and a value. Valuator devices also have a delta resolution.
Device
type : qType
value : qValue
delta : short
The devices may be enabled. A sequence of events awaits processing by the client.
A number of devices may be bound to a device. A pair of devices may be associated
with the x and y coordinates of the cursor.
State
devices : qDevice →7 7 Device
enabled : F qDevice
events : seq Event
bindings : qDevice → 7 7 seq qDevice
cursor : qDevice × qDevice
enabled ⊆ dom devices
dom bindings = dom devices
0∈/ dom devices
Initially, much of the state is zero or empty. A number of devices are configured in
the system, but there are no enabled or bound devices.
122 Formal Specification and Documentation using Z
InitState
State0
devices0 6= ∅
enabled0 = ∅
events0 = hi
ran bindings0 = {hi}
cursor0 = (0, 0)
∀ dev : qDevice | dev ∈ dom devices0 •
(devices0 dev).value = 0 ∧
(devices0 dev).delta = 0
∆State
State
State0
dom devices0 = dom devices
∀ dev : qDevice | dev ∈ dom devices •
(devices0 dev).type = (devices dev).type
Some operations do not affect the state. (Note that in practice the actual device values
change asynchronously but this does not affect the abstract specification.)
For most operations, only a small part of the state is changed. The following schemas
are useful in the definition of subsequent operations, by specifying that all but one of
the state components is unaffected.
Device values may change asynchronously. Button values can only be 0 and 1. For
valuator devices, the change must be greater than the delta resolution of the device.
Keyboards only return ASCII characters.
Chapter 7 An Event-based Input System 123
AsyncChange
ΦDevice
device : qDevice
Device
Device0
θDevice = devices(device)
type0 = type
delta0 = delta
type = Button ⇒ value0 = {0 7→ 1, 1 7→ 0}value
type = AbsValuator ⇒ abs(value0 − value) ≥ delta
type = RelValuator ⇒ value0 ≥ delta
type = Keyboard ⇒ value0 ∈ char
devices0 = devices ⊕ {device 7→ θDevice0 }
If the device is enabled, this causes an event. This is added to the end of the event
queue together with any associated enabled bound device events. The corresponding
current device value is recorded in each event.
QueueEvent
ΦEvent
Event
bound devs : seq qDevice
bound events : seq Event
device ∈ enabled
value = (devices device).value
events0 = events a hθEventi a bound events
bound devs = bindings(device) enabled
#bound events = #bound devs
∀ i : N | i ∈ dom bound devs •
(bound events i).device = bound devs(i) ∧
(bound events i).value = (devices (bound devs i)).value
AsyncEvent∗ =
b AsyncEvent0 ∨ AsyncEvent1 ∨ AsyncEvent2 ∨ . . .
These asynchronous events may be thought of as occurring in sequence with opera-
tions invoked by the client. Each operation can be considered as being atomic.
boolean isvaluator(device)
qDevice device;
boolean isrelative(device)
qDevice device;
boolean isabsolute(device)
qDevice device;
boolean iskeyboard(device)
qDevice device;
A partially specified schema may be used to capture the general features of these
operations. Then each operation may be defined in terms of this schema.
ΦIs
ΞState
device? : qDevice
qtype : F qType
is : boolean
(devices device?).type ∈ qtype ⇒ is = TRUE
(devices device?).type ∈
/ qtype ⇒ is = FALSE
When a device value changes, an event is entered in the input event-queue if this device
has been selected for queuing by the client with a qdevice() request.
int qdevice(device)
qDevice device;
QDevice
ΦEnable
device? : qDevice
enabled0 = enabled ∪ {device?}
Once a device has been selected by qdevice() an event will be placed in the event
queue whenever the device changes value. Devices which have not been queued will
not cause events to be entered in the event queue.
Events which are presently being queued may be deselected for queuing with the
unqdevice() request.
int unqdevice(device)
qDevice device;
UnqDevice
ΦEnable
device? : qDevice
enabled0 = enabled \ {device?}
Certain devices such as MOUSEX or CLOCK are either high resolution or ‘noisy’ and
may thus generate more events than the client actually wishes to see. The threshold()
interface allows the client to specify that a minimum change must occur in the device’s
value before an event is entered in the queue.
Threshold
ΦDevice
device? : qDevice
delta? : short
Device
Device0
θDevice = devices(device?)
type0 = type
value0 = value
delta0 = delta?
devices0 = devices ⊕ {device? 7→ θDevice0 }
If the device has been selected for queuing by qdevice() then a change of at least delta
must occur on its associated value before an event will be placed in the queue.†
GetEvent
ΦEvent
pValue! : qValue
getevent! : qDevice
Event
θEvent = head events
pValue! = value
getevent! = device
events0 = tail events
This operation blocks until an event is available. Hence a number of events may be
necessary beforehand.
b [AsyncEvent∗ | #events0 > 0] o9 GetEvent
GetEvent1 =
Recall that an input event consists of two values – one identifying the device which
generated the event and one giving the value associated with the device at the time of
the event. getevent() returns the device identifier, and places the value associated with
the device for this event in the location pointed to by pValue. The client’s usage is:
short value;
† This interface only really makes sense for valuator type devices. There is also a problem for devices
which are relative versus absolute as this interface implies that the system knows how to determine what
is a change as opposed to an absolute value from the device.
Chapter 7 An Event-based Input System 127
qDevice device;
...
device = getevent(&value);
For efficiency we are often interested in reading a number of events in one procedure
invocation. The getevents() request performs this function.
GetEvents
ΦEvent
count? : int
EventArray! : int →
7 7 Event
getevents! : qDevice
EventArray! = succ o9 (events for count?)
getevents! = (head events).device
events0 = events after count?
getevents returns the device associated with the first event and returns an array of count
events in EventArray. getevents() does not return until all count requested events have
been returned.
Similarly to getevent(), a number of events may be necessary beforehand.
GetEvents1 =
b
[AsyncEvent∗ ; count? : int | #events0 ≥ count?] o9 GetEvents
Events may be ‘posted’ (i.e., placed) at the end of the input queue with the postevent
request.
PostEvent
ΦEvent
count? : int
pDevice? : int → 7 7 qDevice
pValue? : int →
7 7 qValue
count events are entered in the event queue with device id’s given by the list pDevice
and values given in the list pValue. postevent() allows a client to simulate physical
or virtual events generated by some other device, or to implement a pseudo-device to
synthesize some new class of events (e.g., for a window manager or other software
process). It is important that the client be able to enter several events into the queue
as an atomic action. postevent() assures that the list of events passed in will be placed
contiguously in the event queue, uninterrupted by other events which may occur during
the call.
QTest
ΞState
qtest! : qDevice
events 6= hi ⇒ qtest! = (head events).device
events = hi ⇒ qtest! = 0
qtest() returns the device identifier associated with the first input event in the queue,
or 0 if the queue is empty. The client may use qtest() to provide a non-blocking use
of the input queue. This is implemented by using qtest() to see that there is an event
and only then performing a getevent() or getevents() if input is available.
MaxBindings : N1
ConnectEvent
ΦBinding
device?,
bound device? : qDevice
connectevent! : int
bound devs : seq qDevice
bound devs = bindings(device?)
#bound devs < MaxBindings ⇒
bindings0 =
bindings ⊕ {device? 7→ bound devs a hbound device?i} ∧
connectevent! > 0
#bound devs ≥ MaxBindings ⇒
bindings0 = bindings ∧
connectevent! < 0
The bound device will be examined and register an event whenever the device device
generates an event. When an event occurs on device, an event will be placed in the
event queue for that device, and for each device bound to this device by connectevent().
This interface allows the client to cause the information associated with several de-
vices to be entered in the event queue whenever a certain event occurs. connectevent()
is simply called more than once, once for each device to be bound to the queued device.
Devices which have been bound to a queued device by connectevent() will cause the
system to enter events associated with the bound devices immediately after the queued
event, without any intervening events, and in the order established by the invocations
to connectevent(). There is an implementation limit on the number of devices which
can be bound to another device with connectevent().‡ connectevent() returns an error
code less than 0 if it was unable to honour the request, positive non-zero if successful.
The association created between device and bound device by connectevent() is di-
rected. That is, if we bind TABLETX to BUTTON156 with:
connectevent( BUTTON156, TABLETX );
This establishes that when BUTTON156 changes we also produce a TABLETX event,
but not the converse. We may of course establish the other relationship with:
connectevent( TABLETX, BUTTON156 );
The relationships may be thought of as a depth-one directed graph with device as
the root node and the bound device(s) as the related leaf node(s).
An example of the use of connectevent() is as follows – we wish to note the mouse’s
x and y position whenever the mouse’s left button is depressed. We do not wish to
know the mouse’s position at any other time but when the left button is depressed, and
‡ This should be some reasonable number such as 8 or 16, based on the type of devices, and the things that
clients are likely to want to do. These implementation limits may be changed as application requirements
direct.
130 Formal Specification and Documentation using Z
therefore do not wish to select input events based on MOUSEX or MOUSEY. We will
select to queue the mouse left button and then bind the mouse x value and mouse y
value to it with connectevent():
qdevice( MOUSELEFT );
connectevent( MOUSELEFT, MOUSEX );
connectevent( MOUSELEFT, MOUSEY );
It may be necessary to undo the binding between two devices. This function is
performed by the disconnectevent() request.
int disconnectevent(device, bound_device)
qDevice device, bound_device;
DisconnectEvent
ΦBinding
device?,
bound device? : qDevice
disconnectevent! : int
bound devs : seq qDevice
bound devs = bindings(device?)
bound device? ∈ ran bound devs ⇒
bindings0 = bindings ⊕
{device? 7→ bound devs (qDevice \ {bound device?})} ∧
disconnectevent! 6= 0
bound device? ∈/ ran bound devs ⇒
bindings0 = bindings ∧
disconnectevent! = 0
The request returns non-zero on success, and 0 for failure. Failure will be due to the
fact that the bound device referred to was not bound to the device.
AttachCsr
ΦCursor
xdevice?,
ydevice? : qDevice
cursor0 = (xdevice?, ydevice?)
Chapter 7 An Event-based Input System 131
CURSORX and CURSORY are devices in their own right and may be queued with
qdevice like any other device.
Instruction Sets
Hardware as well as software can be specified using the Z notation. The basic con-
cepts concerning machine words and their manipulation are given in Chapter 8. These
definitions are used in Chapter 9 to specify part of the instruction set for the Inmos
Transputer microprocessor family.
Chapter 8
Machine Words
Generic operations on machine words are described at the bit-level that are useful
in the specification of microprocessors at the instruction set level and below. These
definitions are used for the specification of part of an instruction set in Chapter 9.
These are organized into words. Bit positions within a word are numbered consecu-
tively from zero upwards:
Word == { w : N →
7 7 Bit | #w > 0 ∧ dom w = 0 . . #w − 1 }
The values of the least significant bit (LSB) and the most significant bit (MSB) of a
word are often of special interest.
LSB, MSB : Word → Bit
∀ w : Word •
LSB w = w 0 ∧
MSB w = w (#w − 1)
Bit values correspond to numeric values:
bitval : Bit N
bitval = { 0 7→ 0, 1 7→ 1 }
The unsigned value of a word may be defined by:
val : Word → N
∀ w : Word •
#w = 1 ⇒ val w = bitval(LSB w) ∧
#w > 1 ⇒ val w = bitval(LSB w) + 2 ∗ val(succ o9 w)
In general, val is not an injective function for words of variable size:
135
136 Formal Specification and Documentation using Z
∀ w1 , w2 : Word •
w1 a w2 = w1 ∪ (pred#w1 o9 w2 )
Note that this definition of concatenation together with the definition of LSB given ear-
lier mean that the machine is ‘little-endian’; for words of any size the least significant
bit is always the 0th bit of the word.
Generalized concatenation allows a (non-empty) sequence of words to be concate-
nated into one word.
Chapter 8 Machine Words 137
∀ w : Word • a/hwi = w
∀ s, t : seq1 Word •
a/(s a t) = (a/ s) a (a/ t)
∼ : Bit
→ Bit
∼ = {0 7→ 1, 1 7→ 0 }
Bits may be combined by logical AND (‘•’), bitwise logical (inclusive) OR (‘ + ’) and
bitwise logical (exclusive) XOR (‘
+
’).
These definitions are easily upgraded to bitwise logical operations on words. The
one’s complement of a word is given by inverting all its bits:
∼ : Word
→ Word
∀ w : Word •
∼ w = w o9 ∼
WordPair == { w : N →
7 7 (Bit × Bit) | #w > 0 ∧ dom w = 0 . . #w − 1 }
• , + ,
+
: Word × Word → Word
∀ w1 , w2 : Word •
w1 • w2 = (w1 pair w2 ) o9 ( • )∧
w1 + w2 = (w1 pair w2 ) o9 ( + )∧
w1
+
w2 = (w1 pair w2 ) o9 (
+
)
The logical values false and true are represented by Twords with values 0 and 1 re-
spectively:
False == 0
True == 1
A word may be shifted left or right. Zeroes are shifted into the vacant positions.
Chapter 8 Machine Words 139
: Word × N → Word
: Word × N → Word
∀ w : Word •
w0=w∧
w0=w∧
w 1 = ({ #w } −
C pred o9 w) ∪ { 0 7→ 0 } ∧
w 1 = { #w − 1 7→ 0 } ∪ (succ o9 w) ∧
(∀n : N •
w (n + 1) = (w n) 1 ∧
w (n + 1) = (w n) 1 )
Note that addition is not commutative in the general case for words of differing length
since the word size of the result is determined by the size of the first work to be added:
` ∃ w1 , w2 : Word • w1 + w2 6= w2 + w1
However if attention is restricted to words of a fixed size the commutativity property
does hold:
` ∀ w1 , w2 : Word | #w1 = #w2 • w1 + w2 = w2 + w1
Multiplication may be defined inductively in terms of addition.
* : Word × N → Word
∀ w : Word •
w * 0 = zero w ∧
( ∀ n : N • w * n = w + w * (n − 1) )
For convenience the following postfix function is used to distinguish hexadecimal and
decimal number strings.
H : seq HEXCHAR → N
hi H = 0 ∧
( ∀ x : HEXCHAR; s : seq HEXCHAR •
(s a hxi) H = 16 ∗ s H + hex x )
In Chapter 9, the formal definitions provided in this chapter are used as a basis for
defining some of the instructions in the Inmos Transputer instruction set.
Chapter 9
9.1 Instructions
The following Transputer instructions are covered in this chapter:
• pfix val – prefix value.
• nfix val – negative prefix value.
• ldc con – load constant.
• ldl adr – load local from memory address.
• stl adr – store local to memory address.
• ldlp adr – load local pointer.
• adc con – add constant.
• eqc con – equals constant.
• cj adr – conditional jump to a memory address.
• j adr – unconditional jump to a memory address.
• opr – arithmetic and other operations.
Note that a sequence of pfix and nfix instructions is used to increase the size of
constant or address available to the next instruction. They are not used at the Assembly
Language level.
The opr instruction above performs a number of arithmetic and logical operations,
and also the following operations:
• gt – greater than test.
• rev – reverse registers.
• in – input a message from a channel.
143
144 Formal Specification and Documentation using Z
9.2.1 Registers
The Transputer has six principle working registers. Other special purpose registers
are introduced when required. Three of the working registers form an evaluation stack
which is used as a workspace by most instructions.
EVALUATION STACK
Areg : Tword
Breg : Tword
Creg : Tword
The other three working registers are the instruction pointer, which points to the
next instruction to be executed, the operand register, which is described in a later
section, and the workspace pointer. The process running on the Transputer has a
workspace in memory and the workspace pointer references the workspace of the ex-
ecuting process.
REGISTERS
EVALUATION STACK
Oreg : Tword
Wptr : Tword
Iptr : Tword
As with a conventional stack, the basic operations on the evaluation stack are pushes
and pops.
Chapter 9 The Transputer Instruction Set 145
PUSH
∆EVALUATION STACK
Breg0 = Areg
Creg0 = Breg
POP
∆EVALUATION STACK
Areg0 = Breg
Breg0 = Creg
The Areg is at the top of the stack and the result is normally returned in this register as
Areg0 .
9.2.2 Memory
The memory of the Transputer may be regarded as a function from addresses to bytes.
An address is a Tword. Each address is composed of a word address component and
a byte selector component. The byte selector selects a byte within a machine word.
To allow each byte within a word to be addressed the number of bits within a Tword
allocated to the byte selector is the smallest power of 2 which is at least as large as
BytesPerWord. The byte selector occupies the least significant end of the word.
The number of bits in a word allocated to the byte selector is determined as follows:
ByteSelectLength : N
2ByteSelectLength−1 < BytesPerWord ≤ 2ByteSelectLength
Using this the functions ByteSelector and WordAddress can be defined:
ByteSelector : Tword → Word
∀ w : Tword •
ByteSelector w = (0 . . ByteSelectLength − 1) C w
MEMORY REP
ByteMem : Address → Byte
WordMem : TwordAddress → Tword
Bytes : TwordAddress → seq Byte
∀ a : TwordAddress •
Bytes a = { n : N | n < BytesPerWord •
n + 1 7→ ByteMem (ByteIndex a n) } ∧
WordMem a = a/(Bytes a)
The ROM area will normally hold the program code and the RAM area will normally
hold the program variables.
Combining the structure and the representation of memory together gives:
b MEMORY REP ∧ MEMORY MAP
MEMORY =
When memory is updated, the memory map (i.e., the RAM and ROM addresses) are
unaffected. In addition, the contents of ROM is always left unchanged. Some instruc-
tions write to memory; these update ByteMem00 below which only updates areas of
memory address space which contain RAM. Areas outside ROM and RAM contain
undefined values.
148 Formal Specification and Documentation using Z
∆MEMORY
MEMORY
MEMORY 0
ΞMEMORY MAP
MEMORY REP00
offchipRAM 0 = offchipRAM
onchipRAM 0 = onchipRAM
ROM C ByteMem0 = ROM C ByteMem
RAM C ByteMem0 = RAM C ByteMem00
Wptr0 = Wptr00
Inclusion of a clock is not strictly necessary in the specification but it allows rea-
soning about the timing of combinations of instructions, should this be desirable in the
future. The clock cycles given for subsequent instructions are taken from [224].
9.2.4 Errors
The Transputer provides a single error flag which may be set by a number of instruc-
tions.
ERROR
ErrorFlag : Bit
9.2.5 Status
The machine may be running or stopped.
Mode ::= running | stopped
STATUS
Status : Mode
After an instruction, the machine may be running or stopped depending on the instruc-
tion itself. Most instructions leave the processor running:
ΞSTATUS
∆STATUS
Status0 = Status
9.3 Instructions
The following basic instructions are included in the Transputer:
Instruction ::=
pfix | nfix | ldc | adc | ldl | stl | ldlp | j | cj | eqc | opr
The opr instruction allows further ALU and other operations which can be expanded
as required. For the Transputer instruction set defined here, the following are specified:
150 Formal Specification and Documentation using Z
Operation ::=
add | sub | mul | div | rem | sum | diff | prod | gt | rev |
and | or | xor | not | shl | shr | in | out |
seterr | testerr | stoperr | stopp
Each instruction and operation is allocated some unique op-code, here defined using
hexadecimal notation:
InstructionOpCode : Instruction N
OperationOpCode : Operation N
InstructionOpCode =
{ pfix 7→ h2i H, nfix 7→ h6i H, ldc 7→ h4i H, adc 7→ h8i H,
ldl 7→ h7i H, stl 7→ hDi H, ldlp 7→ h1i H,
j 7→ h0i H, cj 7→ hAi H, eqc 7→ hCi H, opr 7→ hFi H }
OperationOpCode =
{ add 7→ h0, 5i H, sub 7→ h0, Ci H, mul 7→ h5, 3i H, div 7→ h2, Ci H,
rem 7→ h1, Fi H, sum 7→ h5, 2i H, diff 7→ h0, 4i H, prod 7→ h0, 8i H,
gt 7→ h0, 9i H, rev 7→ h0, 0i H, and 7→ h4, 6i H, or 7→ h4, Bi H,
xor 7→ h3, 3i H, not 7→ h3, 2i H, shl 7→ h4, 1i H, shr 7→ h4, 0i H,
seterr 7→ h1, 0i H, testerr 7→ h2, 9i H, stoperr 7→ h5, 5i H,
in 7→ h0, 7i H, out 7→ h0, Bi H, stopp 7→ h1, 5i H }
All Transputer instructions are single bytes. The most significant 4 bits of the byte
form an op-code and the least significant 4 bits form an operand.
This design of instruction leads to only 16 instructions being available. Other func-
tions are invoked by means of the OPR instruction and are thus operations rather than
instructions.
The operand is not operated on directly but instead it is added into the Operand
Register (Oreg). The instruction then operates on the contents of Oreg:
DECODE
REGISTERS
MEMORY
Orego : Tword
Orego = Oreg + Twrd(Operand(ByteMem Iptr))
It is now possible to define partial schema definitions for instructions and operations.
Chapter 9 The Transputer Instruction Set 151
ΦINSTRUCTION
∆TRANS
Instr : Instruction
DECODE
OpCode(ByteMem Iptr) = InstructionOpCode Instr
ΦOPERATION
ΦINSTRUCTION
Opr : Operation
Instr = opr
Orego = Twrd(OperationOpCode Opr)
The instruction pointer (Iptr) points to the current instruction to be executed. Most
instructions simply increment Iptr on completion. As was noted previously addresses
are not necessarily continuous and so the function NextInst increments Iptr to the next
value which is a valid address.
NextInst : Address → Address
∀ a : Address •
NextInst a = ByteIndex a 1
Simple instructions are classified as those which increment Iptr and leave Wptr un-
changed and set Oreg0 to 0:
ΦSIMPLE
∆REGISTERS
Oreg0 = 0
Wptr0 = Wptr
Iptr0 = NextInst Iptr
b ΦSIMPLE ∧ ΦINSTRUCTION
ΦSIMPLE INSTRUCTION =
ΦSIMPLE OPERATION b ΦSIMPLE ∧ ΦOPERATION
=
ΦSINGLE =
b POP o9 PUSH
Expanding this schema shows how the registers comprising the evaluation stack are
affected:
ΦSINGLE
Areg, Breg, Creg : Tword
Areg0 , Breg0 , Creg0 : Tword
Breg0 = Breg
Creg0 = Creg
Double operand instructions take two parameters from the evaluation stack, perform
some operation on them and return a result to the evaluation stack.
ΦDOUBLE =
b POP o9 POP o9 PUSH
ΦDOUBLE
Areg, Breg, Creg : Tword
Areg0 , Breg0 , Creg0 : Tword
Breg0 = Creg
The OPR instruction uses the contents of Oreg to determine which operation to exe-
cute. Two instructions are provided to manipulate Oreg and set up these operations.
PFIX
ΦINSTRUCTION
ΞEVALUATION STACK
ΞTRANS
Oreg0 = Orego 4
Wptr0 = Wptr
Iptr0 = Iptr + 1
Cycles = 1
Instr = pfix
Chapter 9 The Transputer Instruction Set 153
NFIX
ΦINSTRUCTION
ΞEVALUATION STACK
ΞTRANS
Oreg0 = (∼ Orego ) 4
Wptr0 = Wptr
Iptr0 = Iptr + 1
Cycles = 1
Instr = nfix
This section describes those instructions which load values from memory to the eval-
uation stack or store values from the evaluation stack into memory. The timings for
instructions which read from or write to memory are applicable to on-chip RAM only.
LDL loads a local variable into the evaluation stack. A local variable is addressed by
its offset from Wptr.
LDL
ΦSIMPLE INSTRUCTION
PUSH
ΞTRANS
Areg0 = WorkSpace Orego
(Wptr + Orego ) ∈ onchipRAM ⇒ Cycles = 2
Instr = ldl
STL stores the value at the top of the evaluation stack into a local variable.
154 Formal Specification and Documentation using Z
STL
ΦSIMPLE INSTRUCTION
POP
ΞERROR
ΞSTATUS
Orego ∈ dom WorkSpace ⇒
WorkSpace00 = WorkSpace ⊕ {Orego 7→ Areg }
(Wptr + Orego ) ∈ onchipRAM ⇒ Cycles = 1
Instr = stl
ADC adds a constant to the value at the top of the evaluation stack.
ADC
ΦSIMPLE INSTRUCTION
ΦSINGLE
ΞMEMORY
ΞSTATUS
Areg0 = Areg +s Orego
Cycles = 1
Instr = adc
(Areg, ( +s ), Orego ) ∈ InRange ⇒ ErrorFlag0 = ErrorFlag
/ InRange ⇒ ErrorFlag0 = Set
(Areg, ( +s ), Orego ) ∈
add operation
ADD
ΦSIMPLE OPERATION
ΦDOUBLE
ΞMEMORY
ΞSTATUS
Areg0 = Breg +s Areg
Cycles = 1
Opr = add
(Areg, ( +s ), Breg) ∈ InRange ⇒ ErrorFlag0 = ErrorFlag
/ InRange ⇒ ErrorFlag0 = Set
(Areg, ( +s ), Breg) ∈
sub operation
SUB
ΦSIMPLE OPERATION
ΦDOUBLE
ΞMEMORY
ΞSTATUS
Areg0 = Breg −s Areg
Cycles = 1
Opr = sub
(Breg, ( −s ), Areg) ∈ InRange ⇒ ErrorFlag0 = ErrorFlag
/ InRange ⇒ ErrorFlag0 = Set
(Breg, ( −s ), Areg) ∈
156 Formal Specification and Documentation using Z
mul operation
MUL
ΦSIMPLE OPERATION
ΦDOUBLE
ΞMEMORY
ΞSTATUS
Areg0 = Breg ∗s Areg
Cycles = WordLength + 6
Opr = mul
(Breg, ( ∗s ), Areg) ∈ InRange ⇒ ErrorFlag0 = ErrorFlag
/ InRange ⇒ ErrorFlag0 = Set
(Breg, ( ∗s ), Areg) ∈
div operation
DIV performs an integer division of Breg by Areg. The case Areg = 0 leads to an
error. An error also occurs if Areg = -1 and Breg = MostNeg since MostNeg ÷s -1 =
MostPos +s 1 which is not representable in a Tword.
DIV
ΦSIMPLE OPERATION
ΦDOUBLE
ΞMEMORY
ΞSTATUS
(Areg 6= 0) ∧ (Areg 6= -1 ∨ Breg 6= MostNeg) ⇒
( Areg0 = Breg ÷s Areg ∧ ErrorFlag0 = ErrorFlag )
(Areg = 0) ∨ (Areg = -1 ∧ Breg = MostNeg) ⇒
ErrorFlag0 = Set
Cycles = WordLength + 7
Opr = div
rem operation
REM gives the remainder when Breg is divided by Areg. The error cases are the same
as for DIV.
Chapter 9 The Transputer Instruction Set 157
REM
ΦSIMPLE OPERATION
ΦDOUBLE
ΞMEMORY
ΞSTATUS
(Areg 6= 0) ∧ (Areg 6= -1 ∨ Breg 6= MostNeg) ⇒
( Areg0 = Breg |s Areg ∧ ErrorFlag0 = ErrorFlag )
(Areg = 0) ∨ (Areg = -1 ∧ Breg = MostNeg) ⇒
ErrorFlag0 = Set
Cycles = WordLength + 5
Opr = rem
SUM, DIFF and PROD do the same as ADD, SUB and MUL respectively except that
they never set ErrorFlag. PROD can also be faster than MUL in certain circumstances.
sum operation
SUM
ΦSIMPLE OPERATION
ΦDOUBLE
ΞTRANS
Areg0 = Breg +s Areg
Cycles = 1
Opr = sum
diff operation
DIFF
ΦSIMPLE OPERATION
ΦDOUBLE
ΞTRANS
Areg0 = Breg −s Areg
Cycles = 1
Opr = diff
prod operation
PROD
ΦSIMPLE OPERATION
ΦDOUBLE
ΞTRANS
Areg0 = Breg ∗s Areg
Cycles = (HighestSetBit Areg) + 4
Opr = prod
158 Formal Specification and Documentation using Z
and operation
AND
ΦSIMPLE OPERATION
ΦDOUBLE
ΞTRANS
Areg0 = Breg • Areg
Cycles = 1
Opr = and
or operation
OR
ΦSIMPLE OPERATION
ΦDOUBLE
ΞTRANS
Areg0 = Breg + Areg
Cycles = 1
Opr = or
xor operation
XOR
ΦSIMPLE OPERATION
ΦDOUBLE
ΞTRANS
Areg0 = Breg
+
Areg
Cycles = 1
Opr = xor
not operation
NOT
ΦSIMPLE OPERATION
ΦSINGLE
ΞTRANS
Areg0 = ∼ Areg
Cycles = 1
Opr = not
Chapter 9 The Transputer Instruction Set 159
Two shift instructions are provided. Both shift zeroes into the vacated positions. Other
kinds of shift must be manufactured from a combination of shift and logical instruc-
tions.
shl operation
SHL
ΦSIMPLE OPERATION
ΦDOUBLE
ΞTRANS
Areg0 = Breg (val Areg)
Cycles = (val Areg) + 2
Opr = shl
shr operation
SHR
ΦSIMPLE OPERATION
ΦDOUBLE
ΞTRANS
Areg0 = Breg (val Areg)
Cycles = (val Areg) + 2
Opr = shr
This section describes a variety of instructions which return Boolean values according
to the result obtained from their operations.
EQC tests Areg against the operand in Orego , returning the result in Areg.
EQC
ΦSIMPLE INSTRUCTION
ΦSINGLE
ΞTRANS
Areg = Orego ⇒ Areg0 = True
Areg 6= Orego ⇒ Areg0 = False
Cycles = 2
Instr = eqc
160 Formal Specification and Documentation using Z
gt operation
GT tests Breg against Areg returning the result in Areg. The operands are treated as
signed integers.
GT
ΦSIMPLE OPERATION
ΦDOUBLE
ΞTRANS
num Breg > num Areg ⇒ Areg0 = True
num Breg ≤ num Areg ⇒ Areg0 = False
Cycles = 1
Opr = gt
testerr operation
TESTERR tests the ErrorFlag returning the result on the evaluation stack.
TESTERR
ΦSIMPLE OPERATION
PUSH
ΞTRANS
ΞSTATUS
ErrorFlag = Set ⇒ (ErrorFlag0 = Clear ∧ Areg0 = False)
ErrorFlag = Clear ⇒ (ErrorFlag0 = Set ∧ Areg0 = True)
Cycles = 3
Opr = testerr
stoperr operation
STOPERR stops the machine if the ErrorFlag is set.
Chapter 9 The Transputer Instruction Set 161
STOPERR
ΦOPERATION
ΞEVALUATION STACK
ΞMEMORY
ΞERROR
ErrorFlag = Set ⇒ Status0 = stopped
ErrorFlag = Clear ⇒ Status0 = Status
Cycles = 2
Opr = stoperr
This section describes the branch instructions. Since all the branch instructions po-
tentially cause a discontinuity in the value of Iptr the schema ΦSIMPLE is no longer
appropriate. Instead the schema ΦBRANCH is defined.
ΦBRANCH
ΦINSTRUCTION
ΞTRANS
JumpAddr : Address
Wptr0 = Wptr
Oreg0 = 0
JumpAddr = ByteIndex(NextInst Iptr) Orego
j adr instruction
J jumps to an address specified as a byte offset from the instruction following the J
instruction.
J
ΦBRANCH
ΞEVALUATION STACK
Iptr0 = JumpAddr
Cycles = 3
Instr = j
cj adr instruction
CJ causes a jump to a byte offset from the instruction following the CJ instruction if
Areg is 0.
162 Formal Specification and Documentation using Z
CJ
ΦBRANCH
Areg = 0 ⇒
( ΞEVALUATION STACK ∧ Iptr0 = JumpAddr ∧ Cycles = 4 )
Areg 6= 0 ⇒
( POP ∧ Iptr0 = NextInst Iptr ∧ Cycles = 2 )
Instr = cj
in instruction
IN reads a sequence of bytes into memory starting at the address specified by Creg.
Areg specifies the length of the sequence. Breg defines the channel address being used.
IN
ΦSIMPLE OPERATION
ΞERROR
ΞSTATUS
Input? : seq Byte
chan! : TwordAddress
#Input? = val Areg
Breg ∈ InChannels
chan! = Breg
ByteMem00 = ByteMem ⊕
{ i : N | i ∈ 1 . . val Areg • (ByteIndex Creg (i − 1)) 7→ (Input? i) }
Cycles ≥ 2 ∗ ((#Input? + WordLength − 1) div WordLength) + 18
Opr = in
out instruction
OUT writes a sequence of bytes from memory starting at the address specified by Creg.
Areg specifies the length of the sequence. Breg defines the channel address being used.
Chapter 9 The Transputer Instruction Set 163
OUT
ΦSIMPLE OPERATION
ΞTRANS
Output! : seq Byte
chan! : TwordAddress
Breg ∈ OutChannels
chan! = Breg
Output! =
{ i : N | i ∈ 1 . . val Areg • i 7→ ByteMem(ByteIndex Creg (i − 1)) }
Cycles ≥ 2 ∗ ((#Output! + WordLength − 1) div WordLength) + 20
Opr = out
stopp operation
STOPP stops the processor. Iptr is saved in the work space so it can be analyzed later
if required.
STOPP
ΦSIMPLE OPERATION
ΞEVALUATION STACK
ΞERROR
Status0 = stopped
WorkSpace00 = WorkSpace ⊕ {Twrd(−1) 7→ Iptr0 }
Cycles = 11
Opr = stopp
MemStart : TwordAddress
ResetCode : Address
These should normally be in RAM and ROM respectively for useful operation of the
Transputer.
After start-up, the clock is initialized to zero for convenience and the processor is
running.
InitTRANS
TRANS0
Oreg0 = 0
Wptr0 = MemStart
Iptr0 = ResetCode
Clk0 = 0
Status0 = running
9.6 Conclusions
This specification is perhaps rather baroque for the number of processor instructions
which it describes. This is because it has been produced from a more complete de-
scription of the actual Transputer instruction set [149]. The technique of factoring out
common portions of specification becomes more effective for larger instruction sets.
Chapter 9 The Transputer Instruction Set 165
Additionally the instructions are specified to the bit level. While this is useful for
those wishing to refine this description further down into the levels of hardware, the
compiler writer may prefer a more abstract description in a notation more akin to the
description of the high-level programming language [62, 216].
Since arithmetic operations are defined in terms of words here, overflow conditions
are easily detected. This is an aspect which is easily overlooked in more abstract
specifications, but one which can often cause errors in practice. All resources in a real
machine are finite whereas in a specification it is easy to include infinite objects (e.g.,
natural numbers).
V
Graphics
Some basic graphical concepts concerning pixels (‘picture elements’) are presented in
Chapter 10. These are used to specify the raster-op function, an important graphical
operation, in Chapter 11, and also a number of window systems later in the book.
Chapter 10
10.1 Background
The interest in formalizing aspects of computer graphics and interactive systems is
gradually increasing [132]. For example, parts of the ISO/IEC GKS graphics standard
have been formalized using Z [12, 13]. Early attempts have demonstrated the necessity
of chosing an appropriate notation for the job [175]. Some formal notations have been
designed with computer processing in mind [114] and readability can be a secondary
consideration. However, in the case of standards, the latter becomes a much more
important factor than the former.
The Human-Computer Interface (HCI) is an important part of most software sys-
tems, and window systems are currently the standard interface for the vast majority of
workstations. Formalizing an HCI in a realistic and useful manner is a difficult task,
but progress is being made in categorizing features of interfaces that may help to en-
sure their reliability in the future [128, 193]. There seems to be considerable scope for
further work in this area.
10.2 Pixels
10.2.1 Pixel positions
A raster graphics display is made up of a set of pixels with positions or coordinates.
These are normally defined in X–Y coordinate space. The display is a fixed size
bounded rectangle in the X–Y plane.
Xsize, Ysize : N1
The offset in a particular direction is specified from zero up by convention. The
position of a pixel may be specified by a pair of X–Y coordinates.
Xrange == 0 . . Xsize − 1
Yrange == 0 . . Ysize − 1
Pixel == Xrange × Yrange
169
170 Formal Specification and Documentation using Z
The pixel at (0, 0) is normally at the upper left-hand corner of the display and the
pixel at (Xsize − 1, Ysize − 1) is at the bottom right by convention on most graphical
computer-based window systems.
Many operations are applied to pairs of pixels.
PixelPair
pix1 , pix2 : Pixel
x1 , x2 : Xrange
y1 , y2 : Yrange
pix1 = (x1 , y1 )
pix2 = (x2 , y2 )
The ‘+’, ‘−’ and ‘≤’ operators may be overloaded to apply to pixel positions. ‘+’
and ‘−’ may be used for moving pixel areas around the display. ‘≤’ can be used to
define pixel ordering from the top left to bottom right.
+ ,
− : (Pixel × Pixel) →
7 Pixel
≤ : Pixel ↔ Pixel
∀ PixelPair •
(x1 + x2 < Xsize ∧ y1 + y2 < Ysize) ⇒
pix1 +pix2 = (x1 + x2 , y1 + y2 ) ∧
(x2 ≤ x1 ∧ y2 ≤ y1 ) ⇒
pix1 −pix2 = (x1 − x2 , y1 − y2 ) ∧
pix1 ≤pix2 ⇔ x1 ≤ x2 ∧ y1 ≤ y2
We can define the offset between any two pixel positions as a pixel offset. This is
defined to wrap round the edge of the pixel area and thus is a total function.
offset : Pixel → Pixel
→ Pixel
∀ PixelPair •
offset pix1 pix2 = ((x1 + x2 ) mod Xsize, (y1 + y2 ) mod Ysize)
A rectangular area of pixels can defined using any two opposing corners (e.g., re-
turned using an attached mouse to sweep between the two). The following functions
return the upper left and lower right pixel positions from two such pixel positions
respectively.
Chapter 10 Basic Graphical Concepts 171
min ,
max : (Pixel × Pixel) → Pixel
∀ PixelPair •
pix1 min pix2 = (min{x1 , x2 }, min{y1 , y2 }) ∧
pix1 max pix2 = (max{x1 , x2 }, max{y1 , y2 })
example when clearing a window down to the background colour. A function to set
the range of a relation to a particular value is useful for this.
[P, V]
setval : V → (P →
7 V) → (P →
7 V)
∀ v : V; p : P → 7 V•
setval v p = ( µ m : P →
7 V | (dom m = dom p ∧ ran m = {v}) )
[P, V]
overlaps : (P →
7 V) ↔ (P →
7 V)
∀ p1 , p2 : P →
7 V•
p1 overlaps p2 ⇔ dom p1 ∩ dom p2 6= ∅
A sequence of pixel maps may be overlaid in the order given by the sequence. It is
convenient to define a distributed overriding operator for this.
[P, V]
⊕/ : seq(P →
7 V) → (P →
7 V)
⊕/hi = ∅
∀p : P →
7 V • ⊕/hpi = p
10.3 Windows
A series of windows on a display screen may be viewed as a sequence in which each
window is laid on the screen in the order defined by the sequence (bottom first, top
last). If some of the windows are removed from a sequence, it is sometimes desirable
to ‘squash’ the remaining windows into a sequence again, keeping the windows in the
same order, but ensuring that they are numbered sequentially from one upwards. The
standard Z toolkit squash function (see page 118 of [381]) can be used to perform this
operation.
If the windows in a sequence overlap, it is useful to be able to move selected win-
dows so that their contents may be viewed (or hidden). This is analogous to shuffling
a pile of sheets of paper (windows) on a desk (screen). Note that the sheets of paper
may be of different sizes and in different positions on the desk.
We can define functions to ‘select’ and ‘remove’ a set of windows from a sequence
using their identifiers rather than their position in the pile.
[W]
select ,
remove : seq W × P W → seq W
∀ s : seq W; w : P W •
s select w = squash(s B w) ∧
s remove w = squash(s −B w)
We can then ‘raise’ or ‘lower’ these windows to the end or beginning of the sequence
as required.
[W]
raise ,
lower : seq W × P W → seq W
∀ s : seq W; w : P W •
s raise w = (s remove w) a (s select w) ∧
s lower w = (s select w) a (s remove w)
Every window in a system usually has an identifier, denoted ‘Window’, which allows
it to be accessed uniquely.
[Window]
The generic functions defined in this section will normally be applied to such identi-
fiers.
Windows often contain text. Thus, a text string is needed sometimes (e.g., for a title
of a window). This is denoted as ‘String’. The string may be empty.
[String]
‘’ : String
This concludes the basic definitions which will be used as required in Chapter 11 and
Part VI.
Chapter 11
Raster-Op Functions
Raster-op functions are useful when moving areas of pixels (e.g., parts of windows)
around the screen on graphics display systems. Raster-op is now widely used in
graphics systems, in particular for window systems. This chapter formally specifies
raster-op functions and gives an example of its use. It makes use of some of the
basic graphic concepts formalized in Chapter 10. Readers not familiar with ‘raster-
op’ may prefer to do some background reading first (e.g., see [158, 312]).
Given two pixel values, we may perform a bit-wise ‘NAND’ (‘not and’) on the two
values to produce a new value. If both bits are set then the result is clear; if either bit
is clear then the result is set.
All the other binary and unary logical functions may be defined in terms of this func-
tion. For example, we can define a unary ‘NOT’ function.
175
176 Formal Specification and Documentation using Z
AND ,
OR ,
XOR : (Value × Value) → Value
∀ val1 , val2 : Value •
val1 AND val2 = NOT(val1 NAND val2 ) ∧
val1 OR val2 = (NOT val1 ) NAND (NOT val2 ) ∧
val1 XOR val2 = (val1 OR val2 ) AND (val1 NAND val2 )
Two pixels in a pair of pixel maps with the same shape are considered to have the
same position if the same offset function which relates the two maps also relates the
two pixels. This is captured in ‘samepos’ relation below. If the relation is true then
it implies that the two pixels are in the same relative position within two pixel maps
with the same shape. That is to say, if one of the pixel maps were to be moved on top
of the other then one pixel would be exactly on top of the other.
samepos : (Pixel × Pixmap) ↔ (Pixel × Pixmap)
∀ pix1 , pix2 : Pixel; MapPair |
pix1 ∈ dom map1 ∧ pix2 ∈ dom map2 •
(pix1 , map1 ) samepos (pix2 , map2 ) ⇔
( ∃ pix0 : Pixel •
dom((offset pix0 ) o9 map1 ) = dom map2 ∧
pix1 7→ pix2 ∈ offset pix0 )
We may define operations similar to the bit-wise operations on values to apply to pixel
maps. In this case by convention, the last operand of the function has the same domain
as the result of the function. We start by defining the ‘nand’ function.
Chapter 11 Raster-Op Functions 177
Note that this operation is not commutative, unlike ‘NAND’ since the second operand
defines the domain of the result of the function. Specifically, if the domains of the
pixel maps differ, the ordering is important. If the domains are the same then the
ordering is unimportant.
Using the basic ‘nand’ function, we may define fifteen further operations. Four of
these degenerate to monadic functions. ‘noop’ leaves a pixel map unaffected, ‘not’
inverts all bits, ‘clear’ clears all the bits and ‘set’ sets all the bits.
noop,
not,
clear,
set : Pixmap → Pixmap
∀ map : Pixmap •
noop map = map ∧
not map = map nand map ∧
clear map = map nand (not map) ∧
set map = not(clear map)
There are five more important operators. These correspond to standard logical opera-
tions except ‘copy’ which is extremely useful for moving pixel maps.
and ,
or ,
xor ,
nor ,
copy : (Pixmap × Pixmap) →
7 Pixmap
∀ MapPair •
map1 and map2 = not(map1 nand map2 ) ∧
map1 or map2 = (not map1 ) nand (not map2 ) ∧
map1 xor map2 = (map1 or map2 ) and (map1 nand map2 ) ∧
map1 nor map2 = not(map1 or map2 ) ∧
map1 copy map2 = map1 or (clear map2 )
The rest of the operations are used less often but are detailed here for completeness.
178 Formal Specification and Documentation using Z
copyInverted ,
andReverse ,
andInverted ,
orReverse ,
orInverted ,
equiv : (Pixmap × Pixmap) →
7 Pixmap
∀ MapPair •
map1 copyInverted map2 = (not map1 ) or (clear map2 ) ∧
map1 andReverse map2 = map1 and (not map2 ) ∧
map1 andInverted map2 = (not map1 ) and map2 ∧
map1 orReverse map2 = map1 or (not map2 ) ∧
map1 orInverted map2 = (not map1 ) or map2 ∧
map1 equiv map2 = (not map1 ) xor map2
This covers the sixteen possible raster-op Boolean functions on two values.
Display
screen : Pixmap
During changes to the screen, its size does not change although the pixel values dis-
played on the screen may be updated.
∆Display
Display
Display0
dom screen0 = dom screen
The screen may be updated using one of the raster-op functions previously defined.
Some functions require a source and destination area while others degenerate into a
single area.
RasterOp1
∆Display
area? : P Pixel
op? : Pixmap → Pixmap
screen0 = screen ⊕ op?(area? C screen)
Chapter 11 Raster-Op Functions 179
RasterOp2
∆Display
area? : P Pixel
from? : Pixel
op? : (Pixmap × Pixmap) →
7 Pixmap
screen0 = screen ⊕
op? ( ((offset from?)(| area? |)) C screen , area? C screen )
b SepPair ∧ SepPair0
∆SepPair =
We may swap a pair of pixel maps with the same shape using the ‘copy’ operation.
CopySwap
∆SepPair
map01 = map2 copy map1
map02 = map1 copy map2
In practice, these two ‘copy’ operations cannot be carried out simultaneously. A third
copy is necessary and additionally a temporary pixel map area is required. This can
easily be expressed by using three schemas, one for each operation, and then combin-
ing them using the schema composition operator (‘o9’). This is left as a exercise for the
reader.
Alternatively, the ‘xor’ raster-op function may be used. Three sequential operations
are still necessary, but the use of a temporary buffer area is eliminated. The following
two schemas ‘xor’ one or other of a pair of pixel maps with its opposite number.
Xor1
∆SepPair
map01 = map2 xor map1
map02 = map2
Xor2
∆SepPair
map01 = map1
map02 = map1 xor map2
180 Formal Specification and Documentation using Z
A swap may be achieved between the two pixel maps by applying ‘xor’ three times
sequentially as follows.
XorSwap =
b Xor1 o9 Xor2 o9 Xor1
By symmetry, the following is also true.
∆SepPair ` XorSwap ⇔ (Xor2 o9 Xor1 o9 Xor2 )
The XorSwap operation has exactly the same effect as using the ‘copy’ operator twice
simultaneously, as in the CopySwap operation.
∆SepPair ` CopySwap ⇔ XorSwap
11.4 Conclusion
In this chapter we have formally specified the raster-op function and how this may
be applied to a graphics display. We have given an example of its use for swapping
areas of a display. By defining operations performed on rectangular areas, we have
specified some of the underlying operations necessary for a window system. Three
different window systems are formalized in Part VI.
VI
Window Systems
A number of operations for three window systems are formally specified using Z,
namely WM in Chapter 12, the Blit in Chapter 13, and the widely used X window
system in Chapter 14. The specifications make use of some of the graphical definitions
in Part V. Finally, Chapter 15 briefly compares the three window systems and draws
some general conclusions about the use of Z for specifying realistically sized systems.
Chapter 12
The user can request a window to lie within a specified range of dimensions and can
also explicitly ask for a window body to be hidden from view or exposed on the screen.
Each window has a title which can be set by the user. This information is used by the
window manager to lay out the window on the screen, although there is no guarantee
that what the user asks for is what the user gets!
183
184 Formal Specification and Documentation using Z
Control
title : String
control : HideExpose
xylimits : Pixel × Pixel
(first xylimits)≤(second xylimits)
WM0
windows : F Window
current : Window
contents : Window →
7 Info
Undefined ∈
/ windows
windows = dom contents
current ∈ windows ∪ {Undefined}
The display screen consists of the background overlaid with windows. The window
pixel maps do not overlap. All windows are contained within the background area.
WM1
WM0
maps : Window → 7 Pixmap
areas : Window → 7 (P Pixel)
screen, background : Pixmap
maps = contents o9 (λ Info • map)
areas = contents o9 (λ Info • area)
disjoint areas
S
(ran areas) ⊆ dom background
S
screen = background ⊕ (ran maps)
You can have as many windows as you need, subject to the restriction that the WM
process can handle at most 20 windows, including hidden windows and windows re-
quested by other programs, at one time.
Chapter 12 The ITC ‘WM’ Window Manager 185
MaxWindows : N
MaxWindows = 20
We can include this limitation in our model of the state.
b [ WM1 | #windows ≤ MaxWindows ]
WM2 =
The size of a window on the user’s display is one of the resources that the Window
Manager allocates. A program can request a given size, and WM will take the re-
quested size into account when making decisions, but it does not guarantee a particular
size. This process is modelled as a function of the system. The number of windows is
not changed by this function. Additionally, control information supplied by the user is
left unchanged.
WINDOWS == Window →
7 Info
WM
WM2
adjust : WINDOWS → WINDOWS
∀ w, w0 : WINDOWS | w0 = adjust w •
#w0 = #w ∧
w0 o9 (λ Info • θControl) = w o9 (λ Info • θControl)
Operations change the state of the system. However the background and hence the
size of the screen remains constant. Additionally the algorithm to adjust the size of
windows does not change.
∆WM
WM
WM 0
background0 = background
adjust0 = adjust
can be used to shorten subsequence specifications of these operations and reduce rep-
etition. The names of such schemas are prepended with ‘Φ’ to distinguish these from
actual operations.
ΦCurrent
∆WM
Info
Info0
current ∈ windows
current0 = current
θInfo = contents current
contents0 = adjust (contents ⊕ {current 7→ θInfo0 })
This leaves a valid current window the same, but updates the information associated
with it in some (as yet unspecified) way.
The size of the body of the currently selected window can be returned. If the window
is actually hidden (i.e., WM has adjusted the window to display the header only), then
the returned size is empty.
GetDimensions
ΦCurrent
wh! : Pixel
xy1 , xy2 : Pixel
θInfo0 = θInfo
dom body = xy1 . .xy2
wh! = xy2 −xy1
ExposeMe
ΦCurrent
map0 = map
title0 = title
control0 = Expose
xylimits0 = xylimits
Note that the state of ‘control’ before the operation has not been checked above, so
HideMe0 will leave a hidden window hidden and ExposeMe0 will leave a visible win-
dow exposed.
A window may be explicitly selected as the current window, until another window is
selected or created. All output will be sent to the selected window.
SelectWindow
∆WM
w? : Window
w? ∈ windows
current0 = w?
contents0 = contents
The title of a window may be set. This involves placing a text string in the header
section of the window contents.
SetTitle
ΦCurrent
s? : String
map0 = map
title0 = s?
control0 = control
xylimits0 = xylimits
ClearWindow
ΦCurrent
header0 = header
body0 = setval White body
title0 = title
control0 = control
xylimits0 = xylimits
Other operations supplied by the WM library include line, text and string drawing,
raster operations, operations to save and restore parts of the picture, input handling,
menus, mouse input, etc. In addition, new operations may be added; at the time that
this specification was originally formulated WM was still under development.
12.3 Errors
There is a Null window identifier which is never a valid window.
Null : Window
b [ WM | Null ∈
WMerr = / windows ]
∆WM and ΞWM are redefined appropriately.
Some operations return a window identifier. If this is non-null then the operation is
successful.
SuccessWM
∆WMerr
w! : Window
w! 6= Null
Alternatively a error may occur. There is a limit on the number of windows which
WM can handle. This could cause an error when creating a new window.
TooManyWindows
ΞWMerr
w! : Window
#windows ≥ MaxWindows
w! = Null
NoCurrentWindow
ΞWMerr
current = Undefined
b SelectWindow ∨ InvalidWindow
SelectWindow1 =
A window may always be hidden or exposed, even if this does not affect its state, so
no error schemas are required for the HideMe and ExposeMe operations.
Initially there are no hosts (and hence no window managers) on the network.
b [ ITC0 | hosts0 = ∅ ]
InitITC =
Operations cause changes on the network.
b ITC ∧ ITC0
∆ITC =
Hosts can be added to the system (e.g., booting up) and removed (e.g., crashing or
powering down).
Chapter 12 The ITC ‘WM’ Window Manager 191
AddHost
∆ITC
host? : String
host? ∈
/ hosts ∪ {‘’}
hosts0 = hosts ∪ {host?}
wms0 = wms
RemoveHost
∆ITC
host? : String
host? ∈ hosts
hosts0 = hosts \ {host?}
wms0 = {host?} C wms
Operations can be initiated on a particular ‘local’ host. These do not affect the host
names on the network.
ΦHost
∆ITC
localhost : String
hosts0 = hosts
localhost ∈ hosts
ExecWM
ΦHost
initwm : WM
localhost ∈
/ dom wms
wms0 = wms ∪ {localhost 7→ initwm}
KillWM
ΦHost
localhost ∈ dom wms
wms0 = {localhost} −
C wms
WM operations can be modelled in the global context of the network by updating the
state of WM on a particular local host which is already running WM.
192 Formal Specification and Documentation using Z
ΦWM
ΦHost
∆WM
host : String
θWM = wms host
θWM 0 = wms0 host
The Window Manager on the local host can be requested to create new windows on
any machine on the ITC network that is running a WM process by supplying the appro-
priate host name. Alternatively, specifying a null host parameter results in a request
for a window on the local machine. This is the normal mode of operation.
NewWindowITC
NewWindow1
ΦWM
host? : String
host? = ‘’ ⇒ host = localhost
host? 6= ‘’ ⇒ host = host?
Other window operations discussed previously may be described in the global network
context. For example:
b DeleteWindow1 ∧ ΦWM
DeleteWindowITC =
If the current window is on the local machine, then the operation is executed locally,
otherwise it is carried out over the network.
12.6 Comments
The WM window manager provides a simple system with non-overlapping windows.
Hence no notion of window ordering is required. The idea of a ‘current’ window for
each process using WM means that this information is held as part of the state of the
system and need not be specified as input to many window operations. Windows are
Chapter 12 The ITC ‘WM’ Window Manager 193
automatically reduced in size by the system when there is not enough space on the
screen. This simplifies the task of organizing windows for the user.
The next chapter considers another window system, the Blit.
Chapter 13
Blit Windows
The Blit [16, 329], developed at Bell Labs, Murray Hill, is more like an intelligent
terminal than a workstation. It is diskless and, at the time of its design, interacted
with a remote host running the Bell Labs Eighth Edition UNIX via a 9600 baud
(slow) RS-232 serial line. It has its own simple process scheduler and a bit-mapped
display. Programs can be run on the Blit (downloaded from the remote host), on
the remote host itself using a standard window terminal emulator process on the
Blit, or on both using two special purpose programs which interact with each other
over the serial line. Deciding how to split a program between the Blit and remote
host is a tricky but interesting problem.
The Blit contains ‘layers’ which are analogous to windows on most other systems.
However there is no protection between layers. Each layer has an rectangular region
on the screen associated with it. Here we model this simply as a partial function from
pixel points to values.
Layer == Window
Point == Pixel
Each pixel point is two-valued – i.e., each window is a simple bit map.
Zsize = 1
Several layers (with associated rectangular windows) may exist simultaneously. The
layers are ordered as a sequence for reasons that will be seen in a moment. There is
an invalid null layer for error returns (see later).
NullLayer : Layer
195
196 Formal Specification and Documentation using Z
Blit0
layers : seq Layer
windows : Layer → 7 Rectangle
rects : seq Rectangle
ran layers = dom windows
NullLayer ∈
/ ran layers
rects = layers o9 windows
Several processes may also exist simultaneously in the Blit. Each process has an
associated program and state. A process may be disabled or enabled. However the
rest of this specification is not concerned with the state of processes, but it is included
here for completeness. Each process is normally associated with a layer. Creating a
process without a layer or vice versa is dangerous.
[Program, StateInfo]
Proc
prog : Program
state : StateInfo
l : Layer
The Blit includes no window ‘manager’ as such since any process has access to the
entire screen. There are a series of processes in the system each identified uniquely by
a process id. There is a null invalid id which is returned by operations to indicate an
error. One of the processes may be assigned to receive mouse and keyboard events.
[Id]
NullId : Id
Blit1
Blit0
procs : Id →7 Proc
receiver : Id
NullId ∈
/ dom procs
receiver ∈ dom procs ∪ {NullId}
∀ proc : ran procs • proc.l ∈ ran layers ∪ {NullLayer}
Blit
Blit2
screen, background : Rectangle
dom(⊕/rects) ⊆ dom background
screen = background ⊕ (⊕/rects)
Operations do not change the default terminal program or the background of the dis-
play.
∆Blit
Blit
Blit0
default0 = default
background0 = background
Similarly, processes are often changed while leaving all the layers in the system unaf-
fected.
ΦProc
∆Blit
layers0 = layers
windows0 = windows
198 Formal Specification and Documentation using Z
A layer may also be de-allocated. The associated process should also be freed for
safety, but this is a separate operation.
DelLayer
ΦLayer
l? : Layer
l? ∈ ran layers
layers0 = layers remove {l?}
windows0 = {l?} −
C windows
A process may be created using the standard user interface to select the rectangle for
the process’s layer. This associates the process with the layer.
Chapter 13 Blit Windows 199
NewWindow0 =
b NewProc o9 NewLayer
b [ NewWindow0 | l! = proc.l ]
NewWindowBlit =
A layer may be selected so that the process in that layer becomes the receiver of mouse
and keyboard events.
ToLayer
ΦProc
l? : Layer
proc : Proc
proc ∈ ran procs
l? = proc.l
procs0 = procs
receiver0 = procs∼ proc
Mouse
xy : Point
buttons : P Buttons
Some pixel positions on the display screen may be associated with a particular layer.
200 Formal Specification and Documentation using Z
This is the layer which is visible at that particular pixel. Otherwise the background is
visible at that point. The gun-sight cursor is used to find a particular layer.
Gunsight
ΞBlit
pos? : Mouse
l! : Layer
pos?.xy ∈ dom(⊕/rects) ⇒
l! = layers(max{n : dom rects | pos?.xy ∈ dom(rects n)})
pos?.xy ∈
/ dom(⊕/rects) ⇒
l! = NullLayer
A non-current layer may be selected using button 1. The layer is pulled to the front of
the screen and made the current layer for keyboard and mouse input.
Top
ΦLayer
l? : Layer
layers0 = layers raise {l?}
windows0 = windows
Current&Top =
b Gunsight>>(ToLayer o9 Top)
13.3 Errors
Successful operations can be reported.
SuccessBlit
∆Blit
l! : Layer
l! 6= NullLayer
Similarly, failures can also be reported. This could be because there is not enough
memory for example.
Failure
ΞBlit
l! : Layer
l! = NullLayer
For example, the operations to create a new layer or process may fail because of an
invalid rectangle or lack of memory.
b (NewLayer ∧ SuccessBlit ) ∨
NewLayerone1 =
(InvalidRect ∧ Failure) ∨ Failure
InvalidLayer
ΞBlit
l? : Layer
l? ∈
/ ran layers
Subwindows are displayed in a particular order within their parent window. This may
203
204 Formal Specification and Documentation using Z
Windows must be ‘mapped’ before they can be displayed. The root window is always
mapped. All of a window’s ancestors (if any) must also be mapped for it to be viewable
on the display. Unviewable windows are mapped but have some ancestor which is
unmapped.
X2
X1
mapped, viewable, unviewable : P Window
mapped ⊆ dom windows
root ∈ mapped
viewable = {c : children | parents∗ (| {c} |) ⊆ mapped} ∪ {root}
unviewable = {c : children | c ∈ (mapped \ viewable)}
Each viewable window has an associated visible pixel map which consists of the pixel
map of the window overlaid with its subwindows (in order) if any. These are ‘clipped’
to the size of the parent window.
The root window covers the entire background of the display screen. The screen
displays the pixel map visible from the root window.
X
X2
visible : Window →
7 Pixmap
screen, background : Pixmap
dom visible = viewable
( ∀ w : viewable •
visible w = (windows w) ⊕ (dom(windows w)C
⊕/(squash((order w) o9 visible))) )
background = windows root
screen = visible root
Chapter 14 The X Window System 205
Initially there are no children and only the root window is mapped. Hence only the
background is displayed.
InitX
X0
windows0 = {root0 7→ background0 }
order0 = {root0 7→ hi}
mapped0 = {root0 }
InitX ` children0 = ∅
Proof:
InitX
{predicate in InitX}
⇒ windows0 = {root0 7→ background0 }
{law of ‘dom’}
⇒ dom windows0 = {root0 }
{predicate in X 0 }
⇒ children0 ∪ {root0 } = {root0 }
{since root0 ∈/ children0 from X 0 }
0
⇒ children = ∅
Such reasoning is normally only done informally in a designer’s head; confirming such
properties serves to increase the confidence that a specification does actually describe
what is wanted.
Consider changes in the window system. The root window identifier and the back-
ground of the screen do not change.
∆X
X
X0
root0 = root
background0 = background
b [ ∆X | θX 0 = θX ]
ΞX =
We can now consider operations on the state of the system; initially, error-free opera-
tions will be presented for simplicity. Error conditions are covered later.
206 Formal Specification and Documentation using Z
Note that the predicates in the schema above fully define the state after the operation
since all the other state components may be derived from those given above. The other
components are included in the state definition to allow us to have different views of
the system, depending on the manner in which we wish to access the state.
Sometimes it is convenient to create several windows at once under a single parent
window. Note that not all the windows requested may be created, but this is indicated
by the information returned. This consists of a partial injection obtained from the
sequence numbers of the windows which are actually created to the window identifiers
which they are allocated.
CreateWindows
∆X
parent? : Window
defs? : seq Pixmap
defs! : N 7 7 Window
parent? ∈ dom windows
dom defs! ⊆ dom defs?
ran defs! ∩ dom windows = ∅
windows0 = windows ∪ (defs!∼ o9 defs?)
We also wish to destroy windows. Given a particular window, we may wish to destroy
a set of windows which are associated with it. We can define a partial specification to
do this as a schema. Exactly which windows are to be destroyed is not specified for
the present.
ΦDestroy
∆X
w? : Window
destroy : P Window
w? ∈ children
windows0 = destroy −
C windows
( ∀ w : dom windows • order0 w = (order w) remove destroy )
mapped0 = mapped \ destroy
Mapping a window raises the window and all its subwindows which have had map
requests. Mapping a window which is already mapped has no effect on the screen – it
does not raise it.
208 Formal Specification and Documentation using Z
MapWindow
ΦMap
parent : Window
parent = parents w?
w? ∈
/ mapped ⇒
order0 = order ⊕ {parent 7→ ((order parent) raise {w?})}
w? ∈ mapped ⇒
order0 = order
mapped0 = mapped ∪ {w?}
All the unmapped subwindows of a given window can be mapped together. The order
in which they are mapped is chosen by the system rather than the caller.
MapSubwindows
ΦMap
neworder : iseq Window
newmapped : P Window
newmapped = subwindows(| {w?} |) \ mapped
ran neworder = newmapped
A window can be unmapped. The window will disappear from view if it was visible.
UnmapWindow
ΦMap
order0 = order
mapped0 = mapped \ {w?}
UnmapSubwindows
ΦMap
order0 = order
mapped0 = mapped \ subwindows(| {w?} |)
Windows may be manipulated in various ways. Given a window, its pixel map may be
updated. It is also raised to the top of the display. We can define a general schema to
simplify the definition of such operations.
Chapter 14 The X Window System 209
ΦWindow
∆X
w? : Window
map : Pixmap
parent : Window
parent = parents w?
windows0 = windows ⊕ {w? 7→ map}
order0 = order ⊕ {parent 7→ ((order parent) raise {w?})}
mapped0 = mapped
MoveWindow
ΦWindow
xy? : Pixel
dom map = dom((offset xy?) o9 (windows w?))
The size of a window may be changed without changing its upper left coordinate. A
new width and height are given. The window is always raised. Changing the size of a
mapped window loses its contents.
ChangeWindow
ΦWindow
wdht? : Pixel
pix1 , pix2 : Pixel
dom(windows w?) = pix1 . .pix2
dom map = pix1 . .(pix1 +wdht?)
The size and location of a window may be configured together by combining the last
two operations. The window is raised and the contents are lost.
ConfigureWindow =
b
(MoveWindow ∆X) o9 (ChangeWindow ∆X)
Some operations explicitly affect the order in which the windows are displayed. A
child window is specified, and window relationships, the windows themselves, and the
set of mapped windows remain unchanged.
210 Formal Specification and Documentation using Z
ΦOrder
∆X
w? : Window
parent : Window
suborder, suborder0 : seq Window
parent = parents w?
windows0 = windows
suborder = order parent
order0 = order ⊕ {parent 7→ suborder0 }
mapped0 = mapped
(Note that as for the ΦWindow schema, parent = parents w? implies that w? ∈
children.)
A window may be ‘raised’ so that no sibling window obscures it. If the windows
are regarded as overlapping sheets of paper stacked on a desk, then raising a window
is analogous to moving the sheet to the top of the stack, while leaving its position on
the desk the same.
RaiseWindow =b
[ ΦOrder | suborder0 = suborder raise {w?} ]
LowerWindow = b
[ ΦOrder | suborder0 = suborder lower {w?} ]
ΦCirc
∆X
w? : Window
submapped, circ : P Window
suborder, suborder0 : seq Window
w? ∈ children
submapped = subwindows(| {w?} |) ∩ mapped
circ = {w : submapped |
( ∃ w2 : submapped • w2 6= w ∧ (visible w2 ) overlaps (visible w) )}
windows0 = windows
suborder = order w?
circ 6= ∅ ⇒ order0 = order ⊕ {w? 7→ suborder0 }
circ = ∅ ⇒ order0 = order
mapped0 = mapped
For a particular window, the lowest mapped child that is partially obscured by another
child may be raised. Repeated executions lead to round robin raising.
CircWindowUp
ΦCirc
circ 6= ∅ ⇒
suborder0 = suborder raise {suborder(min(dom(suborder circ)))}
Similarly, the highest mapped child of a particular window that (partially) obscures
another child may be lowered. Repeated executions lead to round robin lowering.
CircWindowDown
ΦCirc
circ 6= ∅ ⇒
suborder0 = suborder lower
{suborder(max(dom(suborder circ)))}
QueryWindow
ΞX
w? : Window
info! : Pixmap
mapped! : MappedState
w? ∈ children
info! = windows w?
w? ∈
/ mapped ⇒
mapped! = IsUnmapped
parents∗ (| {w?} |) ⊆ mapped ⇒
mapped! = IsMapped
w? ∈ mapped ∧ ¬ (parents+ (| {w?} |) ⊆ mapped) ⇒
mapped! = IsInvisible
We can also find out the window identifiers of the parent and all the children (and
hence the number of children) for a particular window. The children are listed in
current stacking order, from bottommost (first) to topmost (last).
QueryTree
ΞX
w? : Window
parent! : Window
children! : seq Window
parent! = parents w?
children! = order w?
The X system includes many other operations. These include more detailed window
operations, mouse operations, graphics for line drawing and fill operations, screen
raster operations, moving bits and pixels to and from the screen, storing and freeing bit
maps and pixel maps, cursor definition, colour operations, font manipulation routines,
text output to a window, and so on. However the operations covered give an indication
of the basic windowing facilities available under the X system.
14.3 Errors
Many operations return a status report signalling success or failure of the operation.
Let this be denoted ‘Status’. Often a ‘NULL’ status indicates success and a non-NULL
status indicates failure.
[Status]
NULL : Status
The operations covered so far detail what should happen in the event of no errors. In
this case we also wish to report the fact that the operation was successful.
Chapter 14 The X Window System 213
SuccessX
status! : Status
status! = NULL
If errors do occur, then these need to be reported as well. For example, an invalid
parent window may be specified.
InvalidParent
ΞX
parent? : Window
status! : Status
parent? ∈
/ dom windows
status! 6= NULL
We may include these errors with the previously defined operations which ignored
error conditions, to produce total operations.
b (CreateWindow ∧ SuccessX ) ∨ InvalidParent
CreateWindow1 =
All the other operations covered take the following form:
b (DestroyWindow ∧ SuccessX ) ∨ InvalidWindowX
DestroyWindow1 =
Windows have other information associated with them besides their pixel maps and
their mapping status, such as border information. However this is not covered here.
Exposure events that result from window operations are also ignored.
The informal description used to formulate this specification was not completely
clear on a number of points. For example, the exact ordering of windows and their
subwindows is not made explicitly clear after operations which affect this. In partic-
ular, it has been assumed here that raising and lowering a window implies that all its
subwindows are also raised or lowered. Where necessary, an educated guess has been
made as to the behaviour of the system.
Formal Specification of
Existing Systems
A high level description of three existing window systems has been presented in
chapters 12, 13 and 14. Only a few operations for each system have been covered.
A complete description would require a manual for each of the systems; a formal
specification does not necessarily reduce the size of a description using informal
methods. However it does make it much more precise. Because of this, it is possible
to reason about a system and detect inconsistencies in it far more easily than the
case where only an informal specification is available. Even if formal specification
is not used in the final documentation, its use will clarify points which can then be
described informally to the user.
The X window system was originally investigated first. It turned out to be the most
complicated system and took a significant amount of time to formalize. Subsequently,
the specification of WM and the Blit system were comparatively easy.
Since the original specification, Version 11 of X (or X11 as it is normally known)
has become an industry standard and is available on many workstations. The other
two systems are not so widely used. X now includes a library interface built on top of
the main X interface that implements almost all of WM. Hence most WM applications
will run under X without source modification.
215
216 Formal Specification and Documentation using Z
The specifications of the window systems presented here were originally undertaken
as part of the Distributed Computing Software (DCS) Project at the Programming
Research Group within the Oxford University Computing Laboratory [43, 47]. As
well as designing and documenting network services using a formal notation, part of
the brief of the DCS project was to undertake case studies of existing systems and to
formally specify parts of them in Z to gain a greater understanding of their operation.
Originally it had been hoped to compare parts of a number of distributed systems
using Z. However, the authors of potential systems for investigation could only supply
academic papers (not enough information) or the source code (too much information).
What was required was some form of informal documentation for the system. Be-
cause window systems are used directly by users, there seems to be more readable
documentation for such systems.
In each case, omissions and ambiguities in the documentation were discovered by
attempting to formalize the system. Where necessary, intelligent guesses were made
about the actual operation. These were usually correct, but not always.
Subsequently, the formal specifications could be used to update the existing docu-
mentation, or even rewrite it from scratch. Although Z has been developed as a design
tool, it is also well suited for post hoc specifications of existing systems, and for de-
tecting and correcting errors and anomalies in the documentation of such systems [41].
The most important stage of formalizing a system is selecting the right level of
abstraction for modelling its state. This is normally an iterative process. On attempting
to specify an operation one often needs to backtrack to change the abstract state of the
system. In particular, extra state components can be convenient to provide different
views of the system depending on the operation involved.
There are likely to be some inconsistencies between the specifications given in
chapters 12 to 14 and the actual operation of the systems described. This is due to
impreciseness and misunderstanding of the informal documentation used to formulate
these specifications. This illustrates one of the reasons for using formal specifica-
tion techniques – to avoid ambiguity or vagueness and to aid precise communication
of ideas. Because of this, formal notation forces issues to the surface much earlier
in the design process than when using informal description techniques such as natu-
ral language and diagrams. Difficult areas of the design cannot be ignored until the
implementation stage. This reduces the number of backtracks necessary round the
design/implementation cycle.
Additionally, using formal specification techniques should reduce maintenance costs
since more of the errors in a system will be discovered before it is released into the
field. Although specification and design costs will be increased, implementation and
maintenance costs should be lower, reducing overall costs.
Formally specifying an existing system could be particularly useful if it is to be
re-engineered to comply with modern software engineering standards. In such cases
there could be costs benefits by taking such an approach [319].
Chapter 15 Formal Specification of Existing Systems 217
The work for the book was largely supported by the UK Science and Engineering
Research Council (SERC) and its successor, the Engineering and Physical Sciences
Research Council (EPSRC). The author was funded by the SERC on the Distributed
Computing Software project (grant number GR/C/9786.6) from 1985 to 1987, on the
Software Engineering project (on an SERC rolling grant) from 1987 to 1989, on the
collaborative Information Engineering Directorate safemos project (GR/F36491)
from 1989 to 1993 and is currently funded on EPSRC grant number GR/J15186 in-
vestigating Provably Correct Hardware/Software Co-design.
Many people have provided inspiration for and have contributed further over the
years to the material presented here. These include: Rosalind Barden, Peter Breuer,
Stephen Brien, David Brown, Jim Davies, Neil Dunlop, Jim Farr, Roger Gimson, Tim
Gleeson, Mike Gordon, Anthony Hall, Ian Hayes, He Jifeng, Mike Hinchey, Tony
Hoare, Darrel Ince, Steve King, Kevin Lano, Carroll Morgan, John Nicholls, Paritosh
Pandya, Philip Rose, Jeff Sanders, Jane Sinclair, Ib Sørensen, Mike Spivey, Victoria
Stavridou, Susan Stepney, Bernard Sufrin, Stig Topp-Jørgensen and Jim Woodcock.
Please forgive me if I have inadvertently omitted anyone; I am extremely grateful to
the above for providing such a rich environment at Oxford and elsewhere.
Mike Gordon helped in particular with the section on schemas in Chapter 3. Car-
roll Morgan and Roger Gimson were the original team on the Distributed Computing
Software Project, as reported in Chapter 4. David Brown designed the example in
Chapter 7. Jim Farr undertook an MSc. project under my supervision, on which the
specification of the Transputer instruction set presented in Chapter 9 is partially based.
Rob Pike (AT&T), Jim Gettys (DEC), C. Neuwirth (CMU), Dave Presotto (AT&T),
David Rosenthal (CMU), Mahadev Satyanarayanan (CMU), Bob Scheifler (MIT) and
Bill Weihl (MIT) helped provide material, information and access to the window sys-
tems described in Part VI. Susan Stepney and Rosalind Barden of Logica Cambridge
Limited initiated the literature guide in Appendix C as part of the collaborative ZIP
project. Jane Sinclair read the manuscript as it neared completion and gave some
valuable comments.
The book has been formatted using Leslie Lamport’s LATEX document preparation
system [251]. The Z notation has been formatted and type-checked throughout, using
Mike Spivey’s f UZZ package [380].
Finally, thank you to my family, Jane, Alice and Emma, for being so patient and
providing a wonderful environment at home.
219
Appendices
Appendix A gives some general pointers for further information on Z, especially that
which is available on-line. A glossary of the Z notation is provided in Appendix B.
Finally, Appendix C surveys the generally available literature on Z, in conjunction
with a comprehensive bibliography.
Appendix A
Information on Z
This appendix provides some details on how to access information on Z, particu-
larly electronically. It has been adapted from a message that is updated and sent
out monthly on international computer networks.
A more recent version of this information is available on-line on the following
World Wide Web (WWW) hypertext page where it is split into convenient sections:
http://www.faqs.org/faqs/z-faq/
223
224 Formal Specification and Documentation using Z
and Z FORUM, as well as a selection of other Z-related text files. Send an email mes-
sage containing the command ‘help’ to [email protected]
for further information on how to use the server. A command of ‘index z’ will list
the Z-related files. If you have serious trouble accessing the archive server, please
contact the address [email protected].
A.6 Z Tools
Various tools for formatting, type-checking and aiding proofs in Z are available. A
free LATEX style file and documentation can be obtained from the OUCL archive
server. Access ftp://ftp.comlab.ox.ac.uk/pub/Zforum/zed.sty and
the zguide.tex file in the same directory via anonymous FTP. The newer styles
‘csp zed.sty’ which uses the new font selection scheme and ‘zed-csp.sty’
which supports LATEX2e handle CSP and Z symbols, and are available in the same
location. A style for Object-Z ‘oz.sty’ with a guide ‘oz.tex’ is also accessible.
The f UZZ package [380], a syntax and type-checker with a LATEX style option and
fonts, is available from the Spivey Partnership, 10 Warneford Road, Oxford OX4 1LU,
UK. It is compatible with the second edition of Spivey’s Z Reference Manual [381].
Contact Mike Spivey (email [email protected]) for fur-
ther information. Alternatively send the command ‘send z fuzz’ to the OUCL
archive server or access ftp://ftp.comlab.ox.ac.uk/pub/Zforum/fuzz
for brief information and an order form.
CADiZ [237], a UNIX-based suite of tools for checking and typesetting Z specifica-
tions. CADiZ also supports previewing and interactive investigation of specifications.
It is available from York Software Engineering, University of York, York YO1 5DD,
UK (tel +44-1904-433741, fax +44-1904-433744). CADiZ supports a language like
that of the Z Base Standard (Version 1.0). A particular extension allows one speci-
fication document to import another, including the mathematical toolkit as one such
document. Typesetting support is available for both troff and for LATEX. Browsing
operations include display of information deduced by the type-checker (e.g. types of
expressions and uses of variables), expansion of schemas, pre- and postcondition cal-
culation, and simplification by the one-point rule. Work is on-going to provide support
for refinement of Z specifications to Ada programs through a literate program devel-
opment method and integrated proof facilities. Further information is available from
David Jordan at York on [email protected].
ProofPower [236] is a suite of tools supporting specification and proof in Higher
Order Logic (HOL) and in Z. Short courses on ProofPower-Z are available as demand
arises. Information about ProofPower can be obtained automatically from ProofPower-
[email protected]. Contact Roger Jones, International Computers Ltd,
Eskdale Road, Winnersh, Wokingham, Berkshire RG11 5TT, UK (tel +44-1734-693131
ext 6536, fax +44-1734-697636, email [email protected]) for further details.
Zola is a tool that supports the production and typesetting of Z specifications, in-
cluding a type-checker and a Tactical Proof System. The tool is sold commercially and
available to academic users at a special discount. For further information, contact K.
Ashoo, Imperial Software Technology, 62–74 Burleigh Street, Cambridge CB1 1DJ,
UK (tel +44-1223-462400, fax +44-1223-462500, email [email protected]).
ZTC [444] is a Z type-checker available free of charge for educational and non-
226 Formal Specification and Documentation using Z
profit uses. It is intended to be compliant with the 2nd edition of Spivey’s Z Reference
Manual [381]. It accepts LATEX with zed or oz styles, and ZSL – an ASCII version
of Z. ZANS is a research prototype Z animator. Both ZTC and ZANS run on Linux,
SunOS 4.x, Solaris 2.x, HP-UX 9.0, DOS, and extended DOS. They are available
via anonymous FTP under ftp://ise.cs.depaul.edu/pub in the directories
ZANS-x.xx and ZTC-x.xx, where x.xx are version numbers. Contact Xiaoping Jia
[email protected]. for further information.
Formaliser is a syntax-directed WYSIWYG Z editor and interactive type-checker,
running under Microsoft Windows, available from Logica. Contact Susan Stepney,
Logica UK Limited, Cambridge Division, Betjeman House, 104 Hills Road, Cam-
bridge CB2 1LQ, UK (email [email protected], tel +44-1223-366343, fax
+44-1223-251001) for further information.
DST-f UZZ is a set of tools based on the f UZZ package by Mike Spivey, supplying
a Motif based user interface for LATEX based pretty printing, syntax and type check-
ing. A CASE tool interface allows basic functionality for combined application of
Z together with structured specifications. The tools are integrated into SoftBench.
For further information contact Hans-Martin Hoercher, DST Deutsche System-Techik
GmbH, Edisonstrasse 3, D-24145 Kiel, Germany (tel +49-431-7109-478, fax +49-
431-7109-503, email [email protected]).
The B-Tool can be used to check proofs concerning parts of Z specifications. The
B-Toolkit is a set of integrated tools which fully supports the B-Method for formal
software development and is available from B-Core (UK) Limited, Magdalen Cen-
tre, The Oxford Science Park, Oxford OX4 4GA, UK. For further details, contact Ib
Sørensen (email [email protected], tel +44-1865-784520, fax
+44-1865-784518).
Z fonts for Microsoft Windows and Macintosh are available on-line. For hyperlinks
to these and other Z tool resources see the WWW Z page tools section:
http://www.zuser.org/z/#tools
A.7 Courses on Z
There are a number of courses on Z run by industry and academia. Oxford Uni-
versity offers industrial short courses in the use Z. As well as introductory courses,
recent newly developed material includes advanced Z-based courses on proof and
refinement, partly based around the B-Tool. Courses are held in Oxford, or else-
where (e.g., on a company’s premises) if there is enough demand. For further infor-
mation, contact Jim Woodcock (tel +44-1865-283514, fax +44-1865-273839, email
[email protected]).
Logica offer a five day course on Z at company sites. Contact Rosalind Barden
(email [email protected], tel +44-1223-366343 ext 4860, fax +44-1223-
322315) at Logica UK Limited, Betjeman House, 104 Hills Road, Cambridge CB2
1LQ, UK.
Praxis Systems plc runs a range of Z (and other formal methods) courses. For details
contact Anthony Hall on +44-1225-444700 or [email protected].
Formal Systems (Europe) Limited run a range of Z, CSP and other formal methods
courses, primarily in the US and with such lecturers as Jim Woodcock and Bill Roscoe
(both lecturers at the OUCL). For dates and prices contact Kate Pearson (tel +44-1865-
Appendix A Information on Z 227
A.8 Publications
A searchable on-line Z bibliography is available on the World Wide Web under
http://www.zuser.org/z/bib.html
in B IBTEX format. For those without WWW access, an older compressed version is
available via anonymous FTP, together with a formatted compressed P OST S CRIPT
version:
ftp://ftp.comlab.ox.ac.uk/pub/Zforum/z.bib.Z
ftp://ftp.comlab.ox.ac.uk/pub/Zforum/z.ps.Z
Information on Oxford University Programming Research Group (PRG) Technical
Monographs and Reports, including many on Z, is available from the librarian (tel
+44-1865-273837, fax +44-1865-273839, email [email protected]).
Formal Methods: A Survey by S. Austin & G. I. Parkin, March 1993 [18] includes
information on the use and teaching of Z in industry and academia. Contact DITC
Office, Formal Methods Survey, National Laboratory, Teddington, Middlesex TW11
0LW, UK (tel +44-181-943-7002, fax +44-181-977-7091) for a copy.
The following books largely concerning Z have been or are due to be published (in
approximate chronological order):
• I. Hayes (ed.), Specification Case Studies, Prentice Hall International Series in
Computer Science, 1987. (2nd ed., 1993)
• J. M. Spivey, Understanding Z: A specification language and its formal semantics,
Cambridge University Press, 1988.
• D. Ince, An Introduction to Discrete Mathematics, Formal System Specification
and Z, Oxford University Press, 1988. (2nd ed., 1993)
• J. C. P. Woodcock & M. Loomes, Software Engineering Mathematics, Addison-
Wesley, 1989.
• J. M. Spivey, The Z Notation: A reference manual, Prentice Hall International
Series in Computer Science, 1989. (2nd ed., 1992)
Widely used as the current de facto standard for Z.
• A. Diller, Z: An introduction to formal methods, Wiley, 1990.
• J. E. Nicholls (ed.), Z user workshop, Oxford 1989, Springer-Verlag, Workshops in
Computing, 1990.
• B. Potter, J. Sinclair & D. Till, An Introduction to Formal Specification and Z,
Prentice Hall International Series in Computer Science, 1991.
• D. Lightfoot, Formal Specification using Z, MacMillan, 1991.
228 Formal Specification and Documentation using Z
A.9 Object-oriented Z
Several object-oriented extensions to or versions of Z have been proposed. The book
Object Orientation in Z [387], is a collection of papers describing various OOZ ap-
proaches – Hall, ZERO, MooZ, Object-Z, OOZE, Schuman & Pitt, Z++ , ZEST and
Fresco (an OO VDM method) – in the main written by the methods’ inventors, and
all specifying the same two examples. A more recent book entitled Object Oriented
Specification Case Studies [258] surveys the principal methods and languages for for-
mal object-oriented specification, including Z-based approaches. For a fuller list of
relevant publications, see page 249.
A.10 Executable Z
Z is a (non-executable in general) specification language, so there is no such thing as a
Z compiler/linker/etc. as you would expect for a programming language. Some people
have looked at animating subsets of Z for rapid prototyping purposes, using logic and
functional programming for example, but this work is preliminary and is not really the
major point of Z, which is to increase human understandability of the specified sys-
tem and allow the possibility of formal reasoning and development. However, Prolog
seems to be the main favoured language for Z prototyping and some references may
be found in the Z bibliography (see Section A.8) and on page 246.
A.11 Meetings
Regular Z User Meetings (ZUM), now known as the International Conference of Z
Users, have been held for a number of years. Details are issued on the newsgroup
comp.specification.z and sent out on the Z User Group mailing list mentioned
in Section A.12. Information on Z User Meetings is available via WWW under:
http://www.zuser.org/zum/
The proceedings for Z User Meetings have been published in the Springer-Verlag
Workshops in Computing series from the 4th meeting in 1989 until the 8th meeting
in 1994. The proceedings are now published in the Lecture Notes in Computer Sci-
ence series by the same publisher. See page 248 for further information on published
proceedings.
The Refinement Workshop is another relevant series, organized by BCS-FACS in
the UK. The proceedings for these workshops are mainly published in the Springer-
Verlag Workshops in Computing series.
The FME Symposium, the successor to the VDM-Europe series of conferences, is
organized by Formal Methods Europe. The proceedings are published in the Springer-
Verlag Lecture Notes in Computer Science series. The chairman of Formal Methods
Europe is Prof. Peter Lucas, TU Graz, Austria (email [email protected]).
The IFIP WG6.1 International Conference on Formal Description Techniques for
Distributed Systems and Communications Protocols (FORTE) addresses formal tech-
niques and testing methodologies applicable to distributed systems such as Estelle,
LOTOS, SDL, ASN.1, Z, etc.
230 Formal Specification and Documentation using Z
It is also available in printed form from the Oxford University Computing Labo-
ratory librarian (email [email protected], tel +44-1865-273837, fax
+44-1865-273839) by requesting Technical Monograph number PRG-107.
A.16 Corrections
Please send corrections or new relevant information about meetings, books, tools, etc.,
to [email protected]. New questions and model answers are also gratefully
received!
Appendix B
Z Glossary
Names
a,b identifiers
d,e declarations (e.g., a : A; b, ... : B...)
f ,g functions
m,n numbers
p,q predicates
s,t sequences
x,y expressions
A,B sets
C,D bags
Q,R relations
S,T schemas
X schema text (e.g., d, d | p or S)
Definitions
a == x Abbreviated definition
a ::= b | ... Data type definition (or a ::= bhhxii | ...)
[a] Introduction of a given set or basic type (or [a, ...])
a Prefix operator
a Postfix operator
a Infix operator
Logic
true Logical true constant
false Logical false constant
¬p Logical negation
p∧q Logical conjunction
p∨q Logical disjunction
p⇒q Logical implication (¬ p ∨ q)
p⇔q Logical equivalence (p ⇒ q ∧ q ⇒ p)
233
234 Formal Specification and Documentation using Z
∀X • q Universal quantification
∃X • q Existential quantification
∃1 X • q Unique existential quantification
let a == x; ... • p Local definition
Relations
A↔B Relation ( P(A×B) )
a 7→ b Maplet ( (a, b) )
dom R Domain of a relation
ran R Range of a relation
id A Identity relation
Q o9 R Forward relational composition
Q◦R Backward relational composition (R o9 Q)
ACR Domain restriction
A− CR Domain anti-restriction
Appendix B Z Glossary 235
Functions
A→ 7 B Partial functions
A→B Total functions
A 7 B Partial injections
AB Total injections
A→ → 7 B Partial surjections
A→ →B Total surjections
A →B Bijective functions
A→ 77 B Finite partial functions
A 77 B Finite partial injections
fx Function application (or f (x) )
Numbers
Z Set of integers
N Set of natural numbers {0, 1, 2, ...}
N1 Set of non-zero natural numbers (N \ {0})
m+n Addition
m−n Subtraction
m∗n Multiplication
m div n Division
m mod n Modulo arithmetic
m≤n Less than or equal
m<n Less than
m≥n Greater than or equal
m>n Greater than
succ n Successor function {0 7→ 1, 1 7→ 2, ...}
m .. n Number range
min A Minimum of a set of numbers
max A Maximum of a set of numbers
236 Formal Specification and Documentation using Z
Sequences
Bags
Schema notation
S Vertical schema.
d New lines denote ‘ ;’ and ‘∧’. The schema name and pred-
p icate part are optional. The schema may subsequently be
referenced by name in the document.
Appendix B Z Glossary 237
Axiomatic description.
d
The description may be non-unique. The predicate part is
p optional. The definitions apply globally in the document
subsequently.
Conventions
a? Input to an operation
a! Output from an operation
a State component before an operation
a0 State component after an operation
S State schema before an operation
S0 State schema after an operation
∆S Change of state (normally S ∧ S0 )
ΞS No change of state (normally [S ∧ S0 | θS = θS0 ] )
ΦS Partial specification of an operation
`p Theorem
d`p Theorem with declarations ( ` ∀ d • p )
Appendix C
Literature Guide
C.1 Introduction
This literature guide contains a selected list of some pertinent publications for Z users.
Most of those included are readily available, either as books or in journals. A few
unpublished items have been included, where they are particularly relevant and can be
obtained reasonably easily.
Some references in the bibliography at the back of the book are accompanied by an
annotation. This may include a contents list (of a book), a list of the titles of Z related
papers (in a collection) with cross references to the full details, or a summary of the
work. Papers are arranged by subject (with authors and brief details of the subject
matter), together with cross references to the full details in the bibliography.
239
240 Formal Specification and Documentation using Z
C.2.4 Z methodology
Other work towards the development of a ‘method’ for Z itself include:
[23] Barden et al. Z in practice
[187] Hall and McDermid. Towards a Z method using axiomatic specification in Z
(using order sorted algebra and OBJ3 [176] in particular)
[309] Neilson. A rigorous development method from Z to C [244]
[424] Wood. A practical approach using Z and the refinement calculus
[443] Wordsworth. Software development with Z
The application of metrics to formal specifications has been studied:
[418, 20] Whitty and Bainbridge et al. Structural metrics for Z specifications
Appendix C Literature Guide 241
A formal specification in Z can be useful for deciding test cases, etc. Work on testing
is reported in:
[8, 9] Ammann and Offutt. Functional and test specifications based on the category-
partition method
[88] Carrington and Stocks. Formal methods and software testing
[113] Cusack and Wezeman. Deriving tests for objects specified in Z
[188] Hall. Testing with respect to formal specification
[197] Hayes. Specification directed module testing
[390] Stocks. Applying formal methods to software testing
[391] Stocks and Carrington. Deriving software test cases from formal specifica-
tions
[392, 393] Stocks and Carrington. Test templates: a specification-based testing
framework and case study
[280, 282, 281, 368, 367] May, Shepherd et al. T800 transputer FPU development
More technical papers on hardware applications (including embedded software) are:
[24] Barrett. A floating-point number system (IEEE-754 standard)
[38, 39, 45, 61] Bowen. Microprocessor instruction sets (Motorola 6800 and Trans-
puter)
[119, 120, 164, 165, 199] Delisle/Garlan and Hayes. Oscilloscopes, including reuse
of specifications
[242, 243] Kemp. Viper microprocessor
[374] Smith and Duke. Cache coherence protocol (in Object-Z)
[379] Spivey. Real-time kernel
Communications systems and protocols are specified in:
[38] Bowen et al. Network services via remote procedure calls (RPC)
[84] Butler. Service extension (PABX)
[139] Duke et al. Protocol specification and verification using Z
[142] Duke et al. Object-oriented protocol specification (mobile phone system, in
Object-Z)
[179] Gotzhein. Open distributed systems
[196] Haughton. Safety and liveness properties of communication protocols
[276, 278] Mataga and Zave. Formal specification of telephone features
[330] Pilling et al. Inheritance protocols for real-time scheduling
[337] Potter and Till. Gateway functions within a communications network
[445] Zave and Jackson. Specification of switching systems (PBX)
The following papers describe the use of Z for various graphics applications, standards
(especially GKS), and Human-Computer Interfaces (HCI):
[2] Abowd et al. A survey of user interface languages including Z
[10, 11] Arnold et al. Configurable models of graphics systems (GKS)
[43, 47] Bowen. Formal specification of window systems (X in particular)
[80] Brown and Bowen. An extensible input system for UNIX
[129] Dix et al. Human-Computer Interaction (HCI)
[133] Duce et al. Formal specification of Presentation Environments for Multimedia
Objects (PREMO)
[136, 137] Duke and Harrison. Event model of human-system interaction and map-
ping user requirements to implementations
[192] Harrison. Engineering human-error tolerant software
[303, 304] Narayana and Dharap. Formal specification of a Look Manager and a
dialog system
[307] Nehlig and Duce. Formal specification of the GKS design primitive
[398] Sufrin. Formal specification of a display-oriented editor
[397, 400] Sufrin and He. Effective user interfaces and interactive processes
[406] Took. A formal design for an autonomous display manager
Appendix C Literature Guide 243
C.4 Textbooks on Z
[36] Bottaci and Jones. Formal specification using Z: a modelling approach
[126] Diller. Z: an introduction to formal methods (2nd edition)
[203] Hayes et al. Specification case studies (the first book on Z, now in its 2nd
edition, containing an excellent selection of example Z specifications)
[209] Heath, Allum and Dunckley. Introductory logic and formal methods
[222] Imperato. An introduction to Z
[223] Ince. An introduction to discrete mathematics and formal system specification
(2nd edition)
[262] Lightfoot. Formal specification using Z
[286] McMorran and Powell. Z guide for beginners
[320] Norcliffe and Slater. Mathematics of software construction
[336] Potter, Sinclair and Till. An introduction to formal specification and Z (a
popular first textbook on Z)
[346] Rann, Turner and Whitworth. Z: a beginner’s guide
[347] Ratcliff. Introducing specification using Z
[369] Sheppard. An introduction to formal specification with Z and VDM
[437] Woodcock and Loomes. Software engineering mathematics
[443] Wordsworth. Software development with Z
A video course is also available [321, 322].
C.5.4 Refinement
Work on refining Z-like specifications towards an implementation (see also Section C.6.1)
includes:
[19] Bailes and Duke. Class refinement
[24] Barrett. Refinement from Z to microcode via Occam
[27] Baumann. Z and natural semantics programming language theory for algorithm
refinement
[125, 126] Diller. Hoare logic and Part II: Methods of Reasoning
[154, 155, 156] Fidge. Real-time refinement and program development
[171] Gilmore. Correctness-oriented approaches to software development (Z, VDM
and algebraic styles are compared)
[208] He et al. Foundations for data refinement
[230] Jacob. Varieties of refinement
[238] Josephs. Data refinement calculation for Z specifications
[248] King and Sørensen. Specification and design of a library system
[254, 257] Lano and Haughton. Reasoning and refinement in object-oriented spec-
ification languages
[271, 272, 273] Mahoney/Hayes et al. Timed refinement
[308, 309] Neilson. Hierarchical refinement of Z specifications and a rigorous de-
velopment method from Z to C [244]
[365] Sennett. Using refinement to convince (pattern matching in ML)
[366] Sennett. Demonstrating the compliance of Ada programs [341] with Z speci-
fications
[400] Sufrin and He. Specification, analysis and refinement of interactive processes
[420] Whysall and McDermid. Object-oriented specification and refinement
[423] Wood. Software refinery
[430] Woodcock. Implementing promoted operations in Z
[438] Woodcock and Morgan. Refinement of state-based concurrent systems
246 Formal Specification and Documentation using Z
[207] He Jifeng et al. Provably correct systems, including the use of Duration Cal-
culus with schemas for structuring
[252] Lamport. TLZ: Temporal Logic of Actions (TLA) and Z
[271, 272, 273] Mahoney/Hayes et al. Timed refinement
[304] Narayana and Dharap. Invariant properties in a dialog system using Z and
temporal logic
[330] Pilling et al. Inheritance protocols for real-time scheduling
[351] Ruddle. Specification of real-time safety-critical control systems
[372] Smith. An object-oriented approach including a formalization of temporal
logic history invariants
Regular Z User Meetings (ZUM) are organized by the Z User Group (ZUG) and have
had full formally published proceedings since the 4th meeting:
[40] Bowen. 2nd Z User Meeting, Oxford, 1987
[42] Bowen. 3rd Z User Meeting, Oxford, 1988
[313] Nicholls. 4th Z User Meeting, Oxford, 1989
[315] Nicholls. 5th Z User Meeting, Oxford, 1990
[317] Nicholls. 6th Z User Meeting, York, 1991
[70] Bowen and Nicholls. 7th Z User Meeting, London, 1992
[60] Bowen and Hall. 8th Z User Meeting, Cambridge, 1994
[69] Bowen and Hinchey. 9th International Conference of Z Users, Limerick, 1995
The annual Refinement Workshop is organized by the BCS-FACS Special Interest
Group. Papers cover a variety of refinement techniques from specification to code,
and include some Z examples.
[284] McDermid. 1st Refinement Workshop, York, 1988
[300] Morgan and Woodcock. 3rd Refinement Workshop, Hursley, 1990
[301] Morris and Shaw. 4th Refinement Workshop, Cambridge, 1991
[235] Jones et al. 5th refinement Workshop, London, 1992
[405] Till. 6th refinement Workshop, London, 1994
FME Symposia are held every 18 months, organized by Formal Methods Europe.
These grew out of the the later VDM-Europe conferences which included papers on
Z:
[33] Bloomfield et al. VDM’88, Dublin
[32] Bjørner et al. VDM’90, Kiel
[338, 339] Prehn and Toetenel. VDM’91, Noordwijkerhout
[435] Woodcock and Larsen. FME’93, Odense
[302] Naftalin et al. FME’94, Barcelona
WIFT (Workshop on Industrial-strength Formal Specification Techniques) is a US
workshop that held its first meeting in 1994 [159], and is likely to be repeated.
Appendix C Literature Guide 249
C.7 Tools
The ZIP Project tools catalogue lists some tools that support formatting, checking and
proof of Z specifications:
[326] Parker. Z tools catalogue
Details of individual tools may be found in:
[14] Arthan. A proof tool based on HOL which grew into ProofPower (see below)
[58, 59] Bowen and Gordon. Z and HOL (a tool based on higher order logic)
[157] Flynn et al. Formaliser (editor and type-checker)
[236] Jones. ICL ProofPower (a commercial tool based on HOL)
[237, 408] Jordan et al. CADiZ (formatter and type-checker)
[310, 311] Neilson and Prasad. ZedB (a prototype B-based schema expansion and
precondition calculator tool)
[352] Saaltink. Z and EVES (a tool based on ZF set theory)
[380] Spivey. f UZZ (a commercial LATEX formatter and type-checker, 2nd edition)
[444] Xiaoping Jia. ZTC (a freely available type-checker)
http://www.zuser.org/z/bib.html
The bibliography is searchable. The user may provide a regular expression or se-
lect from a number of predefined keywords. Hyperlinks are included to some of the
documents and other relevant details, such is book information, that can be accessed
on-line.
Appendix C Literature Guide 251
Acknowledgements
Thanks are due to all those who suggested references for inclusion in the Z bibliog-
raphy. This guide has been adapted from the collaborative ZIP project bibliography
[386], originally produced by Susan Stepney and Rosalind Barden of Logic Cam-
bridge Limited, together with the on-line Z bibliography held at the Oxford University
Computing Laboratory [49]. Their original contribution is gratefully acknowledged.
Bibliography
253
254 Formal Specification and Documentation using Z
The paper describes a general framework for the formal specification of modu-
lar graphics systems, illustrated by an example taken from the Graphical Kernel
System (GKS) standard.
[11] D. B. Arnold and G. J. Reynolds. Configuring graphics systems components.
IEE/BCS Software Engineering Journal, 3(6):248–256, November 1988.
[12] D. J. Arnold, D. A. Duce, and G. J. Reynolds. An approach to the formal
specification of configurable models of graphics systems. In G. Maréchal, ed-
itor, Proc. EUROGRAPHICS’87, pages 439–463. Elsevier Science Publishers
(North-Holland), 1987.
[13] D. J. Arnold and G. J. Reynolds. Configuring graphics systems components.
IEE/BCS Software Engineering Journal, 3(6):248–256, November 1988.
[14] R. D. Arthan. Formal specification of a proof tool. In Prehn and Toetenel [338],
pages 356–370.
[15] R. D. Arthan. On free type definitions in Z. In Nicholls [317], pages 40–58.
[16] AT&T Bell Laboratories, Murray Hill, New Jersey, USA. UNIXTM Time-
sharing System, Programmer’s Manual, eighth edition, 1985. Volume 1.
[17] S. Aujla, A. Bryant, and L. Semmens. A rigorous review technique: Using
formal notations within conventional development methods. In Proc. 1993
Software Engineering Standards Symposium, pages 247–255. IEEE Computer
Society Press, 1993.
[18] S. Austin and G. I. Parkin. Formal methods: A survey. Technical report, Na-
tional Physical Laboratory, Queens Road, Teddington, Middlesex, TW11 0LW,
UK, March 1993.
[19] C. Bailes and R. Duke. The ecology of class refinement. In Morris and Shaw
[301], pages 185–196.
[20] J. Bainbridge, R. W. Whitty, and J. B. Wordsworth. Obtaining structural metrics
of Z specifications for systems development. In Nicholls [315], pages 269–281.
[21] R. Barden and S. Stepney. Support for using Z. In Bowen and Nicholls [70],
pages 255–280.
[22] R. Barden, S. Stepney, and D. Cooper. The use of Z. In Nicholls [317], pages
99–124.
[23] R. Barden, S. Stepney, and D. Cooper. Z in Practice. BCS Practitioner Series.
Prentice Hall, 1994.
[24] G. Barrett. Formal methods applied to a floating-point number system. IEEE
Transactions on Software Engineering, 15(5):611–621, May 1989.
This paper presents a formalization of the IEEE standard for binary floating-
point arithmetic in Z. The formal specification is refined into four components.
The procedures presented form the basis for the floating-point unit of the In-
mos IMS T800 transputer. This work resulted in a joint UK Queen’s Award
for Technological Achievement for Inmos Ltd and the Oxford University Com-
puting Laboratory in 1990. It was estimated that the approach saved a year in
development time compared to traditional methods.
[25] L. M. Barroca, J. S. Fitzgerald, and L. Spencer. The architectural specification
of an avionic subsystem. In France and Gerhart [159], pages 17–29.
[26] L. M. Barroca and J. A. McDermid. Formal methods: Use and relevance for the
development of safety-critical systems. The Computer Journal, 35(6):579–599,
December 1992.
Bibliography 255
[27] P. Baumann. Z and natural semantics. In Bowen and Hall [60], pages 168–184.
[28] M. Benjamin. A message passing system: An example of combining CSP and
Z. In Nicholls [313], pages 221–228.
[29] M. Benveniste. Writing operational semantics in Z: A structural approach. In
Prehn and Toetenel [338], pages 164–188.
[30] S. Bera. Structuring for the VDM specification language. In Bloomfield et al.
[33], pages 2–25.
[31] J. Bicarregui and B. Ritchie. Invariants, frames and postconditions: A compari-
son of the VDM and B notations. IEEE Transactions on Software Engineering,
21(2):79–89, 1995.
[32] D. Bjørner, C. A. R. Hoare, and H. Langmaack, editors. VDM and Z – Formal
Methods in Software Development, volume 428 of Lecture Notes in Computer
Science. VDM-Europe, Springer-Verlag, 1990.
The 3rd VDM-Europe Symposium was held at Kiel, Germany, 17–21 April
1990. A significant number of papers concerned with Z were presented [89,
135, 164, 123, 179, 185, 246, 354, 383, 412, 438].
[33] R. Bloomfield, L. Marshall, and R. Jones, editors. VDM – The Way Ahead,
volume 328 of Lecture Notes in Computer Science. VDM-Europe, Springer-
Verlag, 1988.
The 2nd VDM-Europe Symposium was held at Dublin, Ireland, 11–16 Septem-
ber 1988. See [3, 30].
[34] D. Blyth, C. Boldyreff, C. Ruggles, and N. Tetteh-Lartey. The case for formal
methods in standards. IEEE Software, pages 65–67, September 1990.
[35] A. Boswell. Specification and validation of a security policy model. IEEE
Transactions on Software Engineering, 21(2):99–106, 1995.
This paper describes the development of a formal security model in Z for
the NATO Air Command and Control System (ACCS): a large, distributed,
multilevel-secure system. The model was subject to manual validation, and
some of the issues and lessons in both writing and validating the model are
discussed.
[36] L. Bottaci and J. Jones. Formal Specification Using Z: A Modelling Approach.
International Thomson Publishing, London, 1995.
[37] S. R. Bourne. The UNIX System. International Computer Science Series.
Addison-Wesley, 1982.
[38] J. P. Bowen. Formal specification and documentation of microprocessor instruc-
tion sets. Microprocessing and Microprogramming, 21(1–5):223–230, August
1987.
[39] J. P. Bowen. The formal specification of a microprocessor instruction set. Tech-
nical Monograph PRG-60, Oxford University Computing Laboratory, Wolfson
Building, Parks Road, Oxford, UK, January 1987.
The Z notation is used to define the Motorola M6800 8-bit microprocessor in-
struction set.
[40] J. P. Bowen, editor. Proc. Z Users Meeting, 1 Wellington Square, Oxford, Wolf-
son Building, Parks Road, Oxford, UK, December 1987. Oxford University
Computing Laboratory.
The 1987 Z Users Meeting was held on Friday 8 December at the Department
of External Studies, Rewley House, 1 Wellington Square, Oxford, UK.
256 Formal Specification and Documentation using Z
[140] R. Duke, P. King, G. A. Rose, and G. Smith. The Object-Z specification lan-
guage. In T. Korson, V. Vaishnavi, and B. Meyer, editors, Technology of Object-
Oriented Languages and Systems: TOOLS 5, pages 465–483. Prentice Hall,
1991.
[141] R. Duke, P. King, G. A. Rose, and G. Smith. The Object-Z specification lan-
guage: Version 1. Technical Report 91-1, Department of Computer Science,
University of Queensland, St. Lucia 4072, Australia, April 1991.
The most complete (and currently the standard) reference on Object-Z. It has
been reprinted by ISO JTC1 WG7 as document number 372. A condensed ver-
sion of this report was published as [140].
[142] R. Duke, G. A. Rose, and A. Lee. Object-oriented protocol specification. In
L. Logrippo, R. L. Probert, and H. Ural, editors, Protocol Specification, Test-
ing, and Verification X, pages 325–338. Elsevier Science Publishers (North-
Holland), 1990.
[143] R. Duke and G. Smith. Temporal logic and Z specifications. Australian Com-
puter Journal, 21(2):62–69, May 1989.
[144] N. J. Dunlop. Formal specification of a windowing system. Msc thesis, Oxford
University Computing Laboratory, UK, 1988.
[145] M. Dyer. The Cleanroom Approach to Quality Software Development. Series
in Software Engineering Practice. John Wiley & Sons, 1992.
[146] M. Engel. Specifying real-time systems with Z and the Duration Calculus. In
Bowen and Hall [60], pages 282–294.
[147] A. S. Evans. Specifying & verifying concurrent systems using Z. In Naftalin
et al. [302], pages 366–400.
[148] A. S. Evans. Visualising concurrent Z specifications. In Bowen and Hall [60],
pages 269–281.
[149] J. R. Farr. A formal specification of the Transputer instruction set. Master’s the-
sis, Oxford University Computing Laboratory, Wolfson Building, Parks Road,
Oxford OX1 3QD, UK, September 1987.
A partial specification of the Inmos Transputer instruction set.
[150] P. C. Fencott, A. J. Galloway, M. A. Lockyer, S. J. O’Brien, and S. Pearson. For-
malising the semantics of Ward/Mellor SA/RT essential models using a process
algebra. In Naftalin et al. [302], pages 681–702.
[151] N. E. Fenton and D. Mole. A note on the use of Z for flowgraph transformation.
Information and Software Technology, 30(7):432–437, 1988.
[152] E. Fergus and D. C. Ince. Z specifications and modal logic. In P. A. V. Hall,
editor, Proc. Software Engineering 90, volume 1 of British Computer Society
Conference Series. Cambridge University Press, 1990.
[153] C. J. Fidge. Specification and verification of real-time behaviour using Z and
RTL. In J. Vytopil, editor, Formal Techniques in Real-Time and Fault-Tolerant
Systems, Lecture Notes in Computer Science, pages 393–410. Springer-Verlag,
1992.
[154] C. J. Fidge. Real-time refinement. In Woodcock and Larsen [435], pages 314–
331.
[155] C. J. Fidge. Adding real time to formal program development. In Naftalin et al.
[302], pages 618–638.
264 Formal Specification and Documentation using Z
[156] C. J. Fidge. Proof obligations for real-time refinement. In Till [405], pages
279–305.
[157] M. Flynn, T. Hoverd, and D. Brazier. Formaliser – an interactive support tool
for Z. In Nicholls [313], pages 128–141.
[158] J. D. Foley et al. Computer Graphics: Principles and Practice. Addison-
Wesley, 1990.
[159] R. B. France and S. L. Gerhart, editors. Proc. Workshop on Industrial-strength
Formal Specification Techniques. IEEE Computer Society Press, 1995.
[160] N. E. Fuchs. Specifications are (preferably) executable. IEE/BCS Software
Engineering Journal, 7(5):323–334, September 1992.
[161] P. H. B. Gardiner, P. J. Lupton, and J. C. P. Woodcock. A simpler semantics for
Z. In Nicholls [315], pages 3–11.
[162] D. Garlan. Integrating formal methods into a professional master of software
engineering program. In Bowen and Hall [60], pages 71–85.
[163] D. Garlan. Making formal methods effective for professional software en-
gineers. Information and Software Technology, 37(5-6):261–268, May–June
1995.
Revised version of [162].
[164] D. Garlan and N. Delisle. Formal specifications as reusable frameworks. In
Bjørner et al. [32], pages 150–163.
[165] D. Garlan and N. Delisle. Formal specification of an architecture for a family
of instrumentation systems. In Hinchey and Bowen [213], pages 55–72.
[166] D. Garlan and D. Notkin. Formalizing design spaces: Implicit invocation mech-
anisms. In Prehn and Toetenel [338], pages 31–45.
[167] S. L. Gerhart. Applications of formal methods: Developing virtuoso software.
IEEE Software, 7(5):6–10, September 1990.
This is an introduction to a special issue on Formal Methods with an emphasis
on Z in particular. It was published in conjunction with special Formal Methods
issues of IEEE Transactions on Software Engineering and IEEE Computer. See
also [120, 184, 303, 379, 421].
[168] S. L. Gerhart, D. Craigen, and T. J. Ralston. Observations on industrial practice
using formal methods. In Proc. 15th International Conference on Software
Engineering (ICSE), Baltimore, Maryland, USA, May 1993.
[169] S. L. Gerhart, D. Craigen, and T. J. Ralston. Experience with formal methods
in critical systems. IEEE Software, 11(1):21–28, January 1994.
Several commercial and exploratory cases in which Z features heavily are
briefly presented on page 24. See also [250].
[170] W. W. Gibbs. Software’s chronic crisis. Scientific American, 271(3):86–95,
September 1994.
[171] S. Gilmore. Correctness-oriented approaches to software development. Tech-
nical Report ECS-LFCS-91-147 (also CST-76-91), Department of Computer
Science, University of Edinburgh, Edinburgh EH9 3JZ, UK, 1991.
This PhD thesis provides a critical evaluation of Z, VDM and algebraic specifi-
cations.
[172] R. B. Gimson. The formal documentation of a Block Storage Service. Tech-
nical Monograph PRG-62, Oxford University Computing Laboratory, Wolfson
Building, Parks Road, Oxford, UK, August 1987.
Bibliography 265
[299] C. C. Morgan and T. Vickers, editors. On the Refinement Calculus. Formal Ap-
proaches to Computing and Information Technology series (FACIT). Springer-
Verlag, 1994.
This book collects together the work accomplished at Oxford on the refinement
calculus: the rigorous development, from state-based assertional specification,
of executable imperative code.
[300] C. C. Morgan and J. C. P. Woodcock, editors. 3rd Refinement Workshop, Work-
shops in Computing. Springer-Verlag, 1991.
The workshop was held at the IBM Laboratories, Hursley Park, UK, 9–11 Jan-
uary 1990. See [365].
[301] J. M. Morris and R. C. Shaw, editors. 4th Refinement Workshop, Workshops in
Computing. Springer-Verlag, 1991.
The workshop was held at Cambridge, UK, 9–11 January 1991. For Z related
papers, see [19, 230, 271, 423, 430, 420].
[302] M. Naftalin, T. Denvir, and M. Bertran, editors. FME’94: Industrial Benefit of
Formal Methods, volume 873 of Lecture Notes in Computer Science. Formal
Methods Europe, Springer-Verlag, 1994.
The 2nd FME Symposium was held at Barcelona, Spain, 24–28 October 1994.
Z-related papers include [64, 103, 115, 147, 150, 155, 225, 264]. B-related pa-
pers include [118, 349, 395].
[303] K. T. Narayana and S. Dharap. Formal specification of a look manager. IEEE
Transactions on Software Engineering, 16(9):1089–1103, September 1990.
A formal specification of the look manager of a dialog system is presented in
Z. This deals with the presentation of visual aspects of objects and the editing
of those visual aspects.
[304] K. T. Narayana and S. Dharap. Invariant properties in a dialog system. ACM
SIGSOFT Software Engineering Notes, 15(4):67–79, September 1990.
[305] T. C. Nash. Using Z to describe large systems. In Nicholls [313], pages 150–
178.
[306] C. Neesham. Safe conduct. Computing, pages 18–20, 12 November 1992.
[307] Ph. W. Nehlig and D. A. Duce. GKS-9x: The design output primitive, an
approach to specification. Computer Graphics Forum, 13(3):C–381–C–392,
1994.
[308] D. S. Neilson. Hierarchical refinement of a Z specification. In McDermid [284].
[309] D. S. Neilson. From Z to C: Illustration of a rigorous development method.
Technical Monograph PRG-101, Oxford University Computing Laboratory,
Wolfson Building, Parks Road, Oxford, UK, 1990.
[310] D. S. Neilson. Machine support for Z: The zedB tool. In Nicholls [315], pages
105–128.
[311] D. S. Neilson and D. Prasad. zedB: A proof tool for Z built on B. In Nicholls
[317], pages 243–258.
[312] W. M. Newman and R. F. Sproull. Principles of Interactive Computer Graphics.
Computer Science Series. McGraw-Hill, 2nd edition, 1981.
[313] J. E. Nicholls, editor. Z User Workshop, Oxford 1989, Workshops in Comput-
ing. Springer-Verlag, 1990.
Proceedings of the Fourth Annual Z User Meeting, Wolfson College & Rewley
House, Oxford, UK, 14–15 December 1989. Published in collaboration with
274 Formal Specification and Documentation using Z
the British Computer Society. For the opening address see [324]. For individual
papers, see [28, 81, 82, 101, 124, 157, 180, 198, 210, 232, 255, 305, 328, 370,
382, 418].
[314] J. E. Nicholls. A survey of Z courses in the UK. In Z User Workshop, Oxford
1990 [315], pages 343–350.
[315] J. E. Nicholls, editor. Z User Workshop, Oxford 1990, Workshops in Comput-
ing. Springer-Verlag, 1991.
Proceedings of the Fifth Annual Z User Meeting, Lady Margaret Hall, Ox-
ford, UK, 17–18 December 1990. Published in collaboration with the British
Computer Society. For individual papers, see [20, 76, 84, 98, 161, 181, 200,
211, 219, 234, 237, 253, 287, 292, 310, 314, 322, 344, 363, 419, 442]. The
proceedings also includes an Introduction and Opening Remarks, a Selected Z
Bibliography, a selection of posters and information on Z tools.
[316] J. E. Nicholls. Domains of application for formal methods. In Z User Workshop,
York 1991 [317], pages 145–156.
[317] J. E. Nicholls, editor. Z User Workshop, York 1991, Workshops in Computing.
Springer-Verlag, 1992.
Proceedings of the Sixth Annual Z User Meeting, York, UK. Published in
collaboration with the British Computer Society. For individual papers, see
[15, 22, 117, 86, 125, 134, 192, 311, 316, 333, 352, 371, 402, 410, 433, 446].
[318] J. E. Nicholls. Plain guide to the Z base standard. In Bowen and Nicholls [70],
pages 52–61.
[319] C. J. Nix and B. P. Collins. The use of software engineering, including the
Z notation, in the development of CICS. Quality Assurance, 14(3):103–110,
September 1988.
[320] A. Norcliffe and G. Slater. Mathematics for Software Construction. Series in
Mathematics and its Applications. Ellis Horwood, 1991.
Contents: Why mathematics; Getting started: sets and logic; Developing ideas:
schemas; Functions; Functions in action; A real problem from start to finish:
a drinks machine; Sequences; Relations; Generating programs from specifica-
tions: refinement; The role of proof; More examples of specifications; Con-
cluding remarks; Answers to exercises.
[321] A. Norcliffe and S. Valentine. Z readers video course. PAVIC Publications,
1992. Sheffield Hallam University, 33 Collegiate Crescent, Sheffield S10 2BP,
UK.
Video-based Training Course on the Z Specification Language. The course con-
sists of 5 videos, each of approximately one hour duration, together with sup-
porting texts and case studies.
[322] A. Norcliffe and S. H. Valentine. A video-based training course in reading Z
specifications. In Nicholls [315], pages 337–342.
[323] G. Normington. Cleanroom and Z. In Bowen and Nicholls [70], pages 281–293.
[324] B. Oakley. The state of use of formal methods. In Nicholls [313], pages 1–5.
A record of the opening address at ZUM’89.
[325] A. Palay et al. The Andrew toolkit: An overview. In Proc. Winter USENIX
Technical Conference, Dallas, USA, pages 9–21, 1988.
[326] C. E. Parker. Z tools catalogue. ZIP project report ZIP/BAe/90/020, British
Bibliography 275
[340] I. Pyle. Software engineers and the IEE. Software Engineering Journal,
1(2):66–68, March 1986.
[341] I. C. Pyle. Developing Safety Systems: A Guide Using Ada. Prentice Hall, 1991.
[342] G-H. B. Rafsanjani and S. J. Colwill. From Object-Z to C++ : A structural
mapping. In Bowen and Nicholls [70], pages 166–179.
[343] RAISE Language Group. The RAISE Specification Language. BCS Practitioner
Series. Prentice Hall International, 1992.
[344] G. P. Randell. Data flow diagrams and Z. In Nicholls [315], pages 216–227.
[345] G. P. Randell. Improving the translation from data flow diagrams into Z by in-
corporating the data dictionary. Report no. 92004, RSRE, Ministry of Defence,
Malvern, Worcestershire, UK, January 1992.
[346] D. Rann, J. Turner, and J. Whitworth. Z: A Beginner’s Guide. Chapman & Hall,
London, 1994.
[347] B. Ratcliff. Introducing Specification Using Z: A Practical Case Study Ap-
proach. International Series in Software Engineering. McGraw-Hill, 1994.
[348] N. R. Reizer, G. D. Abowd, B. C. Meyers, and P. R. H. Place. Using formal
methods for requirements specification of a proposed POSIX standard. In IEEE
International Conference on Requirements Engineering (ICRE’94), April 1994.
[349] B. Ritchie, J. Bicarregui, and H. P. Haughton. Experiences in using the abstract
machine notation in a GKS case study. In Naftalin et al. [302], pages 93–104.
[350] P. Rose. A partial specification of the M68000 microprocessor. Master’s the-
sis, Oxford University Computing Laboratory, Wolfson Building, Parks Road,
Oxford OX1 3QD, UK, September 1987.
A partial specification of the Motorola 68000 instruction set.
[351] A. R. Ruddle. Formal methods in the specification of real-time, safety-critical
control systems. In Bowen and Nicholls [70], pages 131–146.
[352] M. Saaltink. Z and Eves. In Nicholls [317], pages 223–242.
[353] H. Saiedian. The mathematics of computing. Journal of Computer Science
Education, 3(3):203–221, 1992.
[354] A. C. A. Sampaio and S. L. Meira. Modular extensions to Z. In Bjørner et al.
[32], pages 211–232.
[355] J. W. Sanders. Two topics in interface refinement. Digest of Papers, Refinement
Workshop, King’s Manor, University of York, UK, 1988.
[356] M. Satyanarayanan. The ITC project: An experiment in large-scale distributed
personal computing. CMU Report CMU-ITC-035, Information Technology
Center (ITC), Carnegie-Mellon University, USA, October 1984.
[357] R. Scheifler and J. Gettys. The X window system. ACM Transactions on Graph-
ics, 5(2):79–109, April 1986.
[358] R. Scheifler and J. Gettys. The X Window System. Digital Press, Bedford, MA,
USA, 1989.
[359] R. Scheifler and J. Gettys. The X window system. In A. R. Meyer, J. V. Gut-
tag, R. L. Rivest, and P. Szolovits, editors, Research Directions in Computer
Science: An MIT Perspective, chapter 5, pages 75–92. The MIT Press, 1991.
[360] R. Scheifler, J. Gettys, and R. Newman. X Window System: C Library and
Protocol Reference. Digital Press, Bedford, MA, USA, 1988.
Bibliography 277
[378] J. M. Spivey. A guide to the zed style option. Oxford University Computing
Laboratory, December 1990.
A description of the Z style option ‘zed.sty’ for use with the LATEX document
preparation system [251].
[379] J. M. Spivey. Specifying a real-time kernel. IEEE Software, 7(5):21–28,
September 1990.
This case study of an embedded real-time kernel shows that mathematical tech-
niques have an important role to play in documenting systems and avoiding
design flaws.
[380] J. M. Spivey. The f UZZ Manual. Computing Science Consultancy, 34 West-
lands Grove, Stockton Lane, York YO3 0EF, UK, 2nd edition, July 1992.
The manual describes a Z type-checker and ‘fuzz.sty’ style option for LATEX
documents [251]. The package is compatible with the book, The Z Notation: A
Reference Manual by the same author [381].
[381] J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall International
Series in Computer Science, 2nd edition, 1992.
This is a revised edition of the first widely available reference manual on Z
originally published in 1989. The book provides a complete and definitive guide
to the use of Z in specifying information systems, writing specifications and
designing implementations. See also the draft Z standard [79].
Contents: Tutorial introduction; Background; The Z language; The mathemat-
ical tool-kit; Sequential systems; Syntax summary; Changes from the first edi-
tion; Glossary.
[382] J. M. Spivey and B. A. Sufrin. Type inference in Z. In Nicholls [313], pages
6–31.
Also published as [383].
[383] J. M. Spivey and B. A. Sufrin. Type inference in Z. In Bjørner et al. [32], pages
426–438.
[384] R. M. Stein. Safety by formal design. BYTE, page 157, August 1992.
[385] S. Stepney. High Integrity Compilation: A Case Study. Prentice Hall, 1993.
[386] S. Stepney and R. Barden. Annotated Z bibliography. Bulletin of the European
Association of Theoretical Computer Science, 50:280–313, June 1993.
[387] S. Stepney, R. Barden, and D. Cooper, editors. Object Orientation in Z. Work-
shops in Computing. Springer-Verlag, 1992.
This is a collection of papers describing various OOZ approaches – Hall, ZERO,
MooZ, Object-Z, OOZE, Schuman & Pitt, Z++ , ZEST and Fresco (an object-
oriented VDM method) – in the main written by the methods’ inventors, and
all specifying the same two examples. The collection is a revised and expanded
version of a ZIP report distributed at the 1991 Z User Meeting at York.
[388] S. Stepney, R. Barden, and D. Cooper. A survey of object orientation in Z.
IEE/BCS Software Engineering Journal, 7(2):150–160, March 1992.
[389] S. Stepney and S. P. Lord. Formal specification of an access control system.
Software – Practice and Experience, 17(9):575–593, September 1987.
[390] P. Stocks. Applying formal methods to software testing. PhD thesis, Depart-
ment of Computer Science, University of Queensland, St. Lucia 4072, Aus-
tralia, 1993.
Bibliography 279
[391] P. Stocks and D. A. Carrington. Deriving software test cases from formal spec-
ifications. In 6th Australian Software Engineering Conference, pages 327–340,
July 1991.
[392] P. Stocks and D. A. Carrington. Test template framework: A specification-based
testing case study. In Proc. International Symposium on Software Testing and
Analysis (ISSTA’93), pages 11–18, June 1993.
Also available in a longer form as Technical Report UQCS-255, Department of
Computer Science, University of Queensland.
[393] P. Stocks and D. A. Carrington. Test templates: A specification-based testing
framework. In Proc. 15th International Conference on Software Engineering,
pages 405–414, May 1993.
Also available in a longer form as Technical Report UQCS-243, Department of
Computer Science, University of Queensland.
[394] P. Stocks, K. Raymond, D. Carrington, and A. Lister. Modelling open dis-
tributed systems in Z. Computer Communications, 15(2):103–113, March
1992.
In a special issue on the practical use of FDTs (Formal Description Techniques)
in communications and distributed systems, edited by Dr. Gordon S. Blair.
[395] A. C. Storey and H. P. Haughton. A strategy for the production of verifiable
code using the B method. In Naftalin et al. [302], pages 346–365.
[396] B. Stroustrup. The C++ Programming Language. Addison-Wesley, 2nd edi-
tion, 1991.
[397] B. A. Sufrin. Formal methods and the design of effective user interfaces. In
M. D. Harrison and A. F. Monk, editors, People and Computers: Designing for
Usability. Cambridge University Press, 1986.
[398] B. A. Sufrin. Formal specification of a display-oriented editor. In N. Gehani
and A. D. McGettrick, editors, Software Specification Techniques, International
Computer Science Series, pages 223–267. Addison-Wesley Publishing Com-
pany, 1986.
Originally published in Science of Computer Programming, 1:157–202, 1982.
[399] B. A. Sufrin. Effective industrial application of formal methods. In G. X. Ritter,
editor, Information Processing 89, Proc. 11th IFIP Computer Congress, pages
61–69. Elsevier Science Publishers (North-Holland), 1989.
This paper presents a Z model of the Unix make utility.
[400] B. A. Sufrin and He Jifeng. Specification, analysis and refinement of interac-
tive processes. In M. D. Harrison and H. Thimbleby, editors, Formal Methods
in Human-Computer Interaction, volume 2 of Cambridge Series on Human-
Computer Interaction, chapter 6, pages 153–200. Cambridge University Press,
1990.
A case study on using Z for process modelling.
[401] P. A. Swatman. Using formal specification in the acquisition of information
systems: Educating information systems professionals. In Bowen and Nicholls
[70], pages 205–239.
[402] P. A. Swatman, D. Fowler, and C. Y. M. Gan. Extending the useful application
domain for formal methods. In Nicholls [317], pages 125–144.
[403] M. C. Thomas. The industrial use of formal methods. Microprocessors and
Microsystems, 17(1):31–36, January/February 1993.
280 Formal Specification and Documentation using Z
[404] M. Tierney. The evolution of Def Stan 00-55 and 00-56: an intensification of
the “formal methods debate” in the UK. In Proc. Workshop on Policy Issues in
Systems and Software Development, Brighton, UK, July 1991. Science Policy
Research Unit.
[405] D. Till, editor. 6th Refinement Workshop, Workshop in Computing. Springer-
Verlag, 1994.
The workshop was held at City University, London, UK, 5–7 January 1994. See
[156, 254].
[406] R. Took. The presenter – a formal design for an autonomous display manager.
In I. Sommerville, editor, Software Engineering Environments, pages 151–169.
Peter Peregrinus, London, 1986.
[407] S. Topp-Jørgensen. Reservation Service: Implementation correctness proofs.
Programming Research Group, Oxford University Computing Laboratory, UK,
1987.
[408] I. Toyn and J. A. McDermid. CADiZ: An architecture for Z tools and its imple-
mentation. Technical document, Computer Science Department, University of
York, York YO1 5DD, UK, November 1993.
[409] S. Valentine. The programming language Z−− . Information and Software Tech-
nology, 37(5-6):293–301, May–June 1995.
[410] S. H. Valentine. Z−− , an executable subset of Z. In Nicholls [317], pages
157–187.
[411] S. H. Valentine. Putting numbers into the mathematical toolkit. In Bowen and
Nicholls [70], pages 9–36.
[412] M. J. van Diepen and K. M. van Hee. A formal semantics for Z and the link
between Z and the relational algebra. In Bjørner et al. [32], pages 526–551.
[413] K. M. van Hee, L. J. Somers, and M. Voorhoeve. Z and high level Petri nets. In
Prehn and Toetenel [338], pages 204–219.
[414] D. R. Wallace, D. R. Kuhn, and L. M. Ippolito. An analysis of selected software
safety standards. IEEE AES Magazine, pages 3–14, August 1992.
[415] M. West, D. Nichols, J. Howard, M. Satyanarayanan, and R. Sidebotham. The
ITC distributed file system: Principles and design. CMU Report CMU-ITC-
039, Information Technology Center (ITC), Carnegie-Mellon University, USA,
March 1985.
[416] M. M. West and B. M. Eaglestone. Software development: Two approaches
to animation of Z specifications using Prolog. IEE/BCS Software Engineering
Journal, 7(4):264–276, July 1992.
[417] C. Wezeman and A. Judge. Z for managed objects. In Bowen and Hall [60],
pages 108–119.
[418] R. W. Whitty. Structural metrics for Z specifications. In Nicholls [313], pages
186–191.
[419] P. J. Whysall and J. A. McDermid. An approach to object-oriented specification
using Z. In Nicholls [315], pages 193–215.
[420] P. J. Whysall and J. A. McDermid. Object-oriented specification and refine-
ment. In Morris and Shaw [301], pages 151–184.
[421] J. M. Wing. A specifier’s introduction to formal methods. IEEE Computer,
23(9):8–24, September 1990.
Bibliography 281
285
286 Formal Specification and Documentation using Z
ANSI , 11 ΦBasicParams, 73
anti-restriction, 43, 234 BBC television, 16
antisymmetric, 37, 54 BCS-FACS, 229, 230, 248
AOP, 70 before state, 6, 56, 237
API, 241 best practice, 17
application areas, 19 bibliography, 227, 250
application of a function, 235 bijection, 42, 235
Application Programming Interface, 241 bijective function, 235
applications, 239, 241, 243 ΦBinding, 122
archive server, 224, 225 Birthday Book, 56
Areg, 144 Bit, 135
arithmetic, 44 bits, 10
functions, 139 BitVal, 171
operators, 141 bitval, 135
ArithOp, 154 bitwise logical functions, 137
Artificial Intelligence, 243 Black, 171
AS, 69 Blanks, 116
ASCII , 9, 109, 115, 119, 121, 122, 131, Blit, 196
226 ∆Blit, 197
ASN.1, 229 ΞBlit, 197
assessment, 27 Blit window system, 10, 195
associative, 37 Blit0 , 195
AsyncChange, 122 Blit1 , 196
AsyncEvent, 123 Blit2 , 196
AsyncEvent∗ , 123 BNF, 20
AsyncEvent0, 123 Book, 54, 55
AsyncEvent1, 123 books, 227, 244
AsyncEvent2, 123 boolean, 120
atomic operation, 6 Boolean type, 64
AttachCsr, 130 bootstrapping, 163
automatic prototyping, 246 Box, 200
axiomatic description, 45, 237 Boyer-Moore, 18, 24
axiomatic specification, 240 ΦBRANCH, 161
Breg, 144
British Computer Society, 230
B-Core (UK) Limited, 226
Button, 120
B-Method, 226, 246
Button1, 199
B-Tool, 18, 226, 246
Button2, 199
B-Toolkit, 226, 246
Button3, 199
Background, 92
Buttons, 199
backward relational composition, 43,
Byte, 137
234
ByteIndex, 146
BadOperation, 93
ByteMem, 146
BadOperationReport, 92
Bytes, 146
bag, 236
ByteSelectLength, 145
difference, 236
ByteSelector, 145
empty, 236
BytesPerWord, 137
membership, 236
ByteVal, 89
union, 236
bags, 236, 247
basic type, 32, 48, 56, 233 C programming language, 119, 240, 245
Index 287
documentation, 3, 19 executable, 4
dom, 234 specification, 246
domain, 234 execution, 229
anti-restriction, 43, 234 ExecWM, 191
restriction, 43, 234 existential quantification, 30
ΦDOUBLE, 152 logical, 234
DRA, 223 schema, 237
DST, 226, 227 expand, 114
DSTf UZZ, 226 Expose, 183
Duration Calculus, 247, 248 ExposeMe, 187
dyad, 154 expression, conditional, 234
expressions, 34, 234
extract from a sequence, 236
EC, 21
EZ, 246
editor, 242, 249
education, 21, 240
educational issues, 224, 240 F, 234
electronic mailing list, 223 FACS Europe newsletter, 230
elements of a set, 32, 234 FACS special interest group, 230
else, 234 Failure, 201
empty FALSE, 120
bag, 236 False, 138
sequence, 49, 236 false, 29, 233
set, 32, 234 FDT, 11
ΦEnable, 122 FILE, 115
engineering practice, 27 File, 89
entity-relationship models, 240 file system, 243
eqc, 143, 149, 150, 159 FileId, 90
EQC, 159, 164 FileStatus, 99
equality, 234 FileStatus1 , 99
equals, 34 FileStatusCost, 102
equiv, 177 FileStatusOp, 103
equivalence, 30 filter a sequence, 236
logical, 233 finite injective sequence, 236
of schemas, 237 finite partial function, 42, 235
ERROR, 148 finite partial injection, 42, 235
error flag, 148 finite sequence, 236
ErrorCost, 78 finite set, 39
ErrorFlag, 148 size, 47, 234
ErrorTariff , 78 finite subset, 234
Estelle, 229 non-empty set, 234
European Commission, 21 first, 38, 234
evaluation stack, 144 first order logic, 64
EVALUATION STACK, 144 Floating Point Unit, 241
Event, 120 floating-point number, 242
ΦEvent, 122 flow-graph, 243
event model, 242 FME, 229, 230, 248
EVES, 24, 249 Symposium, 229
example specification, 56 for, 51, 91
exclusive OR, 138 Formal Description Techniques, 11, 229
EXEC, 164 formal documentation, 19
290 Formal Specification and Documentation using Z
numbers, 235
object-oriented, 229
Object-Z, 250
Reference Manual, 64, 225, 244
refinement, 245
relations, 234
schema notation, 236
semantics, 244
sequences, 236
sets, 234
standard, 11, 230, 244
structuring, 54
syntax, 244
textbooks, 244
toolkit, 43, 244
tools, 225, 226, 249
video course, 244
Z, 47, 235
Z FORUM, 11, 223–225, 230
Z User Group, 230, 248
Z User Meeting, 229, 248
Z++ , 229, 250
Z−− , 246
zed-csp.sty, 225
ZedB tool, 246, 249
Zermelo-Fraenkel, 24, 29
zero, 48, 136
ZeroInterval, 72
ZEST, 229
ZF, 24
ZF set theory, 29, 249
ZIP project, 249
Zola, 225
ZOOM workshop, 250
Zrange, 171
ZRM, 64, 244
Zsize, 171
ZTC type-checker, 29, 225, 249
ZUG, 230, 248
ZUM, 229, 248