Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Refinement in Z and Object-Z : foundations and advanced applications (2nd ed.)
Derrick J., Boiten E., Springer Publishing Company, Incorporated, London, UK, 2014. 499 pp. Type: Book (978-1-447153-54-2)
Date Reviewed: Jan 24 2014

The current success of agile methods in software development has eclipsed the stage-based software life cycle in which specifications assumed a critical role. Agility, a modern slogan for quick and dirty, seems to have the upper hand on formal methods, which are too often associated with painstaking tasks. Despite this perception, the authors of this book remind us that formal methods provide the required foundations for the discipline of software engineering to develop correct software systems. However, reading this book will definitely exacerbate the situation.

This is a slightly revised edition of a monograph that was published in 2001 [1]. It contains a mixture of original text and revised material from research papers published by the authors in various venues. The result is marred by the lack of adequate integration, with redundancies and forward references scattered throughout. Part of this may be attributable to the complexity of the topic itself.

The monograph is divided into four parts of uneven size, with the first part taking up half of the book. Parts 1 and 3 start with introductory chapters on Z and Object-Z, respectively. Readers without a good knowledge of these languages will not benefit from the introductions and will not be able to make any sense of the examples. The other chapters in the first three parts cover the notion of refinement in diverse contexts, moving gradually through more complex semantic environments. Intuitively, refinement is a transformation T of an abstract specification A into a concrete implementation C. To ensure correctness of the process, A, C, and T are expressed formally. The increasing expressiveness of A introduces more complexity in the refinement. Thus, a chapter is dedicated to each type of refinement. The very short Part 4 is a somewhat superficial attempt to combine Z with communicating sequential processes (CSP).

Two complimentary reviews of the first edition [2,3] provide nice summaries. Unlike those reviewers, I do not find the text cohesive, nor do I find the examples interesting. The examples are presented at a superficial level and do not illustrate any of the difficulties that would necessitate the use of formal methods. As for the machinery used to express these refinements, it seems to follow the research on abstract data types as exemplified in Goguen et al.’s paper [4]. Unfortunately, one cannot find the same mathematical elegance.

Consisting mostly of research papers on refinement in Z, this monograph is only suitable for researchers in this same field who are already competent in Z.

Reviewer:  B. Belkhouche Review #: CR141926 (1404-0243)
1) Derrick, J.; Boiten, E. Refinement in Z and Object-Z: foundations and advanced applications (1st ed.). Springer, London, UK, 2001.
2) Stevens, P. Review of Refinement in Z and Object-Z: foundations and advanced applications, by John Derrick and Eerke Boiten. Software Testing, Verification & Reliability 12, 1 (March 2002), 61.
3) Banach, R. Review of Refinement in Z and Object-Z: foundations and advanced applications, by John Derrick and Eerke Boiten. Journal of Logic and Computation 13, 2 (April 2003), 313-314.
4) Goguen, J. A.; Thatcher, J. W.; Wagner, E. G.; Wright, J. B. Initial algebra semantics and continuous algebra. Journal of the ACM 24, 1(1977), 68–95.
Bookmark and Share
  Reviewer Selected
Featured Reviewer
 
 
Requirements/ Specifications (D.2.1 )
 
 
Coding Tools and Techniques (D.2.3 )
 
 
Design Tools and Techniques (D.2.2 )
 
Would you recommend this review?
yes
no
Other reviews under "Requirements/Specifications": Date

Moriconi M. (ed), Lansky A.Type: Article
Dec 1 1985
A unifying framework for structured analysis and design models
Tse T., Cambridge University Press, New York, NY, 1991. Type: Book (9780521391962)
Jun 1 1992
A skeleton interpreter for specialized languages
Steensgaard-Madsen J.  Programming Languages and System Design (, Dresden, East Germany,1861983. Type: Proceedings
Mar 1 1985
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy