VDM '90. VDM and Z - formal methods in software development. 3rd international symposium of VDM Europe, Kiel, FRG, April 17-21, 1990. Proceedings (Q1188662)

[The articles of this volume will not be indexed individually.] This very interesting book is about software specification (in traditional terms, ``analysis''), and, to a somewhat lesser extent, ``design and development'' (i,e., refinement). Most authors are from Europe, with some from the US, Australia and Japan. The papers are essentially based on the viewpoint that specification should be as disciplined as traditional programming --- in fact, it is programming, although at a different abstraction level. It is very important to note, as the authors of the foreword \textit{D. Bjørner} and \textit{H. Langmaack} do, that the papers are ``concerned with bringing real theory to apply to real programming''. The reader may want to consider, for instance, the extensive usage of formal methods in general and of (object) \(Z\) in particular by International Standards Organization for expressing the modeling concept of open distributed processing [ISO/IEC JTC1/SC21/WG7. Recommendation X.905: Basic reference model of open distributed processing. Part 5: Architectural semantics. Document N 434 (18th December 1991)]. To quote from the foreword again, ``we wish the casual reader from industry to adopt the message of \(VDM\) and \(Z\), namely apply formal, model-theoretic techniques in order to have fun, to achieve correct software, etc.''. The application areas successfully dealt with in the papers include databases, open distributed processing, telecommunications, and even hypertext. Often this success is due to the use of formal specifications ``to gain insight into the system and help to clarify the system architecture'' (\textit{D. Lange}) rather than due to formal refinement, proof obligations, etc. In the same manner, formal description of object behavior leads to a drastic improvement over traditional design methodologies that usually lack precise semantic information and therefore ``effectively support the software development process in terms of costs and productivity, but \dots not in terms of quality and reliability'' (\textit{R. di Giovanni} and \textit{P. L. Iachini}). This is especially applicable to information modeling: understanding means creating an implementation-independent formal specification to be used by both the customer and the developer. Objects are used for this purpose because, as \textit{O.-J. Dahl} stressed in his paper, ``objects are useful general purpose tools for concept modeling''. As \textit{C. A. R. Hoare} states in his Preface, ``the obvious advice to the practitioner is to use each notation for its primary intended purpose: \(Z\) for specification and \(VDM\) for development'' because ``there are certain fundamental differences between the structuring principles appropriate to specifications and to development''. This viewpoint is supported by \textit{S. King} in his paper on \(Z\) and the refinement calculus. Other papers use \(VDM\) mostly for sound development of concrete data structures from abstract specifications, with some of them discussing real-life problems typical for a good software engineering effort (\textit{D. Weber-Wulff} notes: ``some of the problems we had were at the exact points where we glossed over the specification and put an `easy' bit that turned out to be wrong''.) C. A. R. Hoare further explains how the distinctive features of \(Z\) arose from the need to simplify and clarify specifications. To quote \textit{A. Sampaio} and \textit{S. Meira}, the papers show ``how simple, nice, and natural it is to write a specification using schemas (and \(Z\) ar large)''. On the other hand, although C. A. R. Hoare suggests that no single notation could be adequate for all purposes, he stresses the common scientific method and common goal of these notations and observes the strong mutual beneficial influence of \(Z\) and \(VDM\). One of the essential aspects of formal specifications --- often considered evident and almost trivial (i.e., the only one possible!) by experienced abstractors and specifiers, but less evident to a casual user --- is the emphasis on semantics of constructs and operations on these constructs rather than just on their signatures. Only a successful formal specification of semantics makes a construct understandable and therefore reusable. Of course, this approach should be used in object analysis and is indeed presented within this framework by several papers in the book. Quite a few papers consider --- explicitly or implicitly --- separation of concerns in specifications, i.e., their disciplined splitting into easily understandable components. This is successfully accomplished by using modularization, abstract data types, or, more generally, the object approach (e.g., in object \(Z\), the semantics aspects of which, including temporality, are defined in the paper by \textit{D. Duke} and \textit{R. Duke}. Some of the most interesting and promising papers on handling large systems are about generic formal specifications to be reused when they are instantiated by particular applications. This approach is advocated, in particular, by object \(Z\), as well as in the hypertext paper by \textit{D. Lange}, in the reusable frameworks paper by \textit{D. Garlan} and \textit{N. Delisle}, etc. Creating and instantiating generic specifications helps to discover important and non-trivial commonalities between seemingly different application areas, and therefore leads to a much better understanding of these areas. It is also instructive to note how the paper by \textit{R. Gotzhein} presents a set of requirements for the use of \(Z\) in open distributed processing and how both object \(Z\) and the (later) frameworks paper \textit{D. Garlan} and \textit{D. Notkin} [Formalizing design spaces: Implicit invocation mechanisms, Lect. Notes in Comput. Sci. 551, 31-44 (1992)] satisfy these requirements, at least partially. This demonstrates a very good cooperation between theory and practice! Note, however, that the problem of determining global semantic integrity constraints (the effect on the system) based on single-object operations is non-trivial: calculation of these constraints is rather cumbersome even for simple cases and may defy the main goal of formalization -- to understand. Occasional papers consider computer assistance essential for the success in creating and refining formal specifications. This viewpoint is debatable: creating a non-trivial specification is a challenging intellectual activity (like non-trivial traditional programming) that demands abstraction and precision, and the help provided by a tool during this activity seems to be rather limited. (Some experienced analysts view ``CASE tools'' as word processors for analysis.) Moreover, computer assistants for refinement usually are not perfect, providing an excuse for (indefinite) postponement of formal methods usage. The choices made by a developer in refinement are often non-trivial, and the amount of reuse here currently is not very substantial. As an interesting example, the \(VDM\) formalization paper by \textit{C. Lafontaine}, \textit{Y. Ledru}, and \textit{P.-Y. Schobbens} shows the use of the \({\mathbf B}\) proof tool that combines interactive and automatic (clerical) proofs, with the majority of proofs, even in simple cases, still requiring user interaction. Several final contributions in the volume deal with formalization and foundation issues (mostly, formalization of semantics). The reader of these interesting papers is often, but not always, supposed to have a substantially more solid (mathematical) maturity than the reader of the previous papers (the papers abount context-based type checking in \(VDM\) and \(Z\) seem to be notable exceptions). In some cases,the shape of mathematical arguments presented by the authors could possibly be improved. This book represents the proceedings of an annual International Symposium. As E. W. Dijkstra remarked some time ago, if 5\% of the presentations at the conference were interesting, the time spent there has been spent properly. The number of interesting papers in this book is substantially larger than 5\%.