Specification of software systems. (Q625100)

This tome is the second, expanded and updated, edition of [the authors, Specification of software systems. Graduate texts in computer science. Berlin: Springer (1998; Zbl 0907.68120)]. It covers a lot of material, and various subsets of the book may be used -- as proposed by the authors -- for different course offerings, from undergraduate to advanced graduate levels, as well as a reference for practitioners, so that, as the authors claim, ``a practitioner who is familiar with one technique can quickly jump start with another technique with little time''. The book is composed of six parts: Specification fundamentals, Formalism fundamentals, Logic, Mathematical abstractions for model-based specifications, Property-oriented specifications, and Model-based specifications. Various formal specification languages and techniques are discussed at length (often with an overemphasis on more elementary aspects, on syntax and syntactic details), and the mathematical background is explicitly presented. An undergraduate course in discrete mathematics, ``fluency in programming'', and ``some software engineering'' are considered by the authors as prerequisites, and ``attainment of some level of mathematical maturity'' is properly mentioned as an asset. Bibliographical notes (usually very good) and exercises are included at the end of each chapter. The authors present a justification for specifications (including domain models and system requirements), but not a lot of motivation, and the existing motivation, especially in the examples, is not very convincing. The examples and even case studies throughout the book are often -- although not always -- simplistic and not too interesting, and at times include relatively lengthy proofs of rather trivial results. A much better and lively motivation -- the ``why'' -- together with a philosophical background for domain engineering, requirements engineering, and software design, and with a huge amount of interesting (formal) specification examples (including errors, unusual situations, etc.) is presented, for example, in [\textit{D. Björner}, Software engineering. Vol. 1--3. Berlin: Springer (2006; Zbl 1095.68020; Zbl 1095.68021; Zbl 1095.68022)]; see also [\textit{J. Woodcock} and \textit{J. Davies}, Using Z. Specification, refinement, and proof. London: Prentice Hall (1996; Zbl 0855.68060)] for an excellent narrative with motivation, examples, and nice proofs. The authors of the book under review, in particular, do not demonstrate that a formal specification -- or at least a rigorous one -- is essential for understanding of the domain and of the technology because reliance on tacit assumptions often leads to failures since different stakeholders usually have substantially -- or somewhat -- different tacit assumptions, and this may be discovered only when an explicit rigorous, or better still, formal, specification is being developed. Quite a few examples of such discoveries exist, and some were described in literature (see, for example, [the reviewer (ed.) and \textit{K. Baclawski} (ed.), Practical foundations of business system specifications. Dordrecht: Kluwer Academic Publishers (2003; Zbl 1027.68147)]). The authors discuss domain models and ontologies and properly mention ``collective interactions among the parts'' of a complex system, as well as the importance of modeling open and evolving systems. Regretfully, these discussions are overly terse and confined to the early chapters of the book. The presentation of ontologies is very primitive and references the OWL language which it is at a too low abstraction level because its target audience usually does not include business domain experts. Clearly, an ontology -- a domain model -- should be understood not only by software engineers. One can only agree with the authors' emphasis on abstraction as an essential concept (described in a separate chapter) and with their criticism of natural language specifications enhanced by diagrams that ``have no inherent semantics unless accompanied by precise annotations''. Nevertheless, the authors of the book under review when discussing ontologies refer mostly to a PhD thesis published in 2009 and use as an example an inadequate and almost semantic-free car ontology (Section 4.4.2) which relies on such ``meaningful names'' as ``has'', ``request'', and ``is a part of'' without providing any precise definitions of semantics of these terms. A book on formal specifications ought to include such examples only as objects of justified criticism. Non-trivial domain models are not explicitly used elsewhere in the book and often are not mentioned. Furthermore, the authors' claim that it is not possible to ``apply formal methods with pencil and paper'' is incorrect because a formal specification without any proofs or syntax checking tools leads to a substantially better understanding of the domain and requirements [\textit{A. Hall}, ``Seven myths of formal methods'', IEEE Software 7, No. 5, 11--19 (1990; \url{doi:10.1109/52.57887})]. The authors mention the inadequacy of using programming languages as specification languages but do not emphasize the main reason of this inadequacy: inappropriate abstraction level. While ``over-specification is an aftermath in programming languages'' (p. 37) may indeed serve as a representation of this reason, this is not sufficient, especially taking into account that business domain concepts and constructs usually substantially differ from data and operations used in programming languages implementations; and formulating requirements in terms of information technology solutions is a wrong approach. On a somewhat related note, it is not necessary the case that in Z a schema describes ``some aspect of the software system being developed'' because Z can be and has been used for business specifications to describe some aspects of business independently of any software systems (see, e.g., [\textit{M. G. Hinchey} (ed.) and \textit{J. P. Bowen} (ed.), Applications of Formal Methods. Prentice Hall International Series in Computer Science. London: Prentice Hall (1995; Zbl 0828.68013)] for such examples using Z and other formal specification languages). The authors properly note in presenting algebraic specifications that ``axiomatic definitions are more abstract than model-based definitions'' (p. 268) and that ``programs describing dissimilar objects and sharing a common structure correspond to an algebra''. These important and valuable observations are regretfully not emphasized. The authors' emphasis on abstraction and separation of concerns as essential concepts, on the importance of modularity in order to contain complexity, and on the need for discussing ``collective interactions among the parts'' of a complex system is clearly appropriate but does not always materialize in their examples. For instance, in the electronic form example (Table 5.2), content concerns are not separated from logical layout and physical presentation concerns, thus making any inevitable changes more difficult to formulate and implement. While the authors mention certain problems associated with the use of specific languages (e.g., ``there is no mechanism in VDM to specify that an operation is periodically performed''), generally it would be very useful for a reader to have a comparative assessment of advantages and disadvantages of these languages. Perhaps more importantly, problems associated with reading (as opposed to writing) formal specifications are not explicitly discussed, although each such specification, if it is to be actually used, will be read much more often -- and by a much more diverse audience -- than written. The authors, however, do provide pretty good English narratives explaining the corresponding fragments of Z, Object-Z, and B specifications. At times, the presentation is overly terse. For example, the important Chapter 8 ``Classification of formal specification methods'' may leave an uninitiated reader rather perplexed. It ought to have been moved or substantially expanded since the explanations there are rather insufficient. Furthermore, even Chapters 9 and 10 on propositional and predicate logic are closer to terse surveys than to tutorials. For a very simple example, modus ponens is used before it is defined. Regretfully, the style and even the grammar are in need of improvement. For example, there are quite a few references to non-existent subsections, and the ``Organization and content'' section of the Preface refers to chapters of the first, rather than the second, edition of this book (but does not say so!), thus making a specification of a product (book) different from its implementation. Three more interesting examples: ``\(k\)-bit binary digits'' (p. 272), ``let us consider the specification of a stack of integers in which the elements who do not exceed the integer on top of the stack is of interest'' (p. 325), and ``the intension of a program or system is in the description of its structure, and program manipulation yields a term with different intension, called its extension, but they have identical behaviors'' (p. 367). There are quite a few typos as well. Summing up, this is a good and useful book on a very important topic, but there is still a room for improvement in its next edition.