Review of "Refinement in Z and Object-Z, Foundations and Advanced
Applications" by John Derrick and Eerke Boiten.

The aim of this book is to provide a single reference for the large
amount of recent work on refinements and their verification in Z and
Object-Z. Some readers will use the volume as a starting point before
tackling the primary research literature; others will find everything
they need here.

The authors have set themselves the ambitious task of addressing
simultaneously industrial users of formal methods, researchers in the
field and postgraduate student classes. In my opinion they succeed: as
well as I can judge, this book will indeed be useful to all these
groups. The one caveat is that although the book is technically
self-contained it does not really expect the reader to be learning Z
or Object-Z from scratch. My own knowledge of Z was limited and rusty,
and I struggled in places. Nevertheless, the book is significantly
more accessible than most of the research literature, so those
comparative novices who are well-motivated to relinquish this status
as soon as they may will find this book a useful stepping stone. In
fact I think everybody is likely to welcome the style and readability
of the book. The explanations are careful and are supported by
well-chosen examples. The book is clearly structured both at the part
and the chapter level, and bibliographical notes at the end of each
chapter provide useful leads into the primary literature, as well as
explaining where the ideas that have been presented come from and how
they fit into the history of the subject. Summary introductions to
both the parts and the chapters will help readers to find the parts of
the book most relevant to them.

There are four parts. The first is by far the longest, and will be the
most useful to non-specialists. It consists of eight chapters
introducing the basic concepts of the field. There is a chapter of
introduction to Z, followed by an introduction to the simplest notions
of refinement. Chapter Three expands on these by discussing
refinements of ADTs and introducing upwards and downwards simulations
to prove their existence. This is done in a relational setting, not
specifically in Z. Chapter Four brings us back to the Z world, and
Chapter Five discusses the calculation of simulations, as may be done
in transformational program development approaches. In Chapter Six we
meet promotions, which in certain cases allow the parts of a system to
be specified independently of the structuring of the parts within the
system, and consider when it is true that a promotion of a refinement
is a refinement of a promotion. Chapter Seven relates testing to
refinement, and Part I ends with a chapter presenting a single
simulation rule combining the power of upwards and downwards simulation.

Part II addresses a problem which will be familiar to developers,
namely that interfaces between system components cannot always be kept
constant, as is assumed by naive approaches to refinement and to
transformational program development. Various ways of relaxing the
ground rules are discussed; for example, refining an operation into a
sequence of operations. In Part III we arrive at Object-Z; three
chapters introduce the language, adapt the treatment of refinement to
it in the context of a single class, and widen the scope to systems of
classes, considering compositionality. Finally, Part IV adds
concurrency to the mix, showing how to combine CSP with Object-Z and
apply notions of refinement to the result.

In summary, whilst this book is not going to convert unbelievers to Z,
I think it will be appreciated by anybody with an interest in Z and
Object-Z who is looking for a thorough and approachable overview of
the use of refinement in this context.