www.btinternet.com/~adrian.larner/review/feijs
Notations for Software Design
Loe MG Feijs,
Hans BM Jonkers, & Cornelius A Middelburg
Springer-Verlag, 1994, 425 pp, softbound
ISBN 0 387 19902 0
A Review by Adrian Larner for the Computer Journal
We can specify and design software using diagrams, or using a formal development language like Z. On the face of it, translations between these two kinds of notation would be useful, and this book boldly attempts them. More than a dozen kinds of diagram are treated, including Data Flow, Nassi-Shneidermann, and State Transition, as well as Sequence Charts. To appreciate the translations, the reader needs merely to digest 200 pages of introduction to the formal language, COLD-1.
“COLD” stands for “Common Object-oriented Language for Design”, but do not be misled into thinking it is Object-oriented. It combines “a wide variety of notations for property-oriented and model-oriented specification, ... in equational style, pre- and post-condition style, inductive definitions, algorithmic definitions in functional as well as imperative style.” It is, in a word, the PL/I of formal development languages.
“The book is self-contained and instead of going into the formal semantics of the language, it will convey a working knowledge of the meaning of the language constructs via the examples, the explanations, and the pictures.” Your reviewer has to report that this working knowledge was not conveyed to him. Surely those that use notations should be able to give their translations into English, and not merely hope that we will latch on to what they mean.
A sort, we are told, is a value set. Then (p89) we are shown an array update definition with input a,n,i: a is of the sort Array, n an index, and i an item. “a” is an “object name”: not (p114) the name of an object, but a “logical variable” (an unvarying pronoun) “of a static nature”. That is, a is an (unchangeable) array value. The post-condition of the array update function is val(a,n)=i, i.e. i is item n of a. Surely this implies that a has changed? But the specification of the update says that only the val function, val(a,n), can change. So perhaps a is unchanged, but val is changed? Or perhaps not: the sort Array is defined as variable, i.e. not a sort at all.
The book appeals, of course, not to the missing informal interpretation of its notation, but to the deliberately omitted formal semantics, which “guarantee that the design can be rigorously analysed.” The motivating case study describes a vending machine: no surprise there, except that it is the weirdest such machine ever analysed; for instance, it is informed individually about each valid coin. What is more, insertion of a valid coin with a value less than the price of any selection stalls the machine; and, while the initial statement of requirements says that each product has a price, the formal specification allows multiple selections, at different prices, for the same product.
Rigorously analysed, not: see your reviewer’s comments on other formal development language texts passim and ad nauseam.
Copyright © 1995, 2001 Adrian Larner. The author asserts all moral rights.
The decorative image of a key (cc004239.gif) used on this page was obtained from IMSI's MasterClips/MasterPhotos© Collection, 1895 Francisco Blvd East, San Rafael, CA 94901-5506, USA.