COLD-1 is a wide-spectrum specification language with a syntax and semantics which describes the form and meaning of its constructs in a mathematically precise way. It is a common language for describing a software system in any stage of its design, ranging from specification to implementation. The language combines a wide variety of notations for property-oriented and model-oriented specification, including state-based specification, in a unifying semantic framework. Many existing styles of specification are supported: specification in equational style, specification in pre- and post-condition style, inductive definitions, algorithmic definitions in functional as well as imperative style, etc. More than that, it offers facilities for the modular structuring of specifications. COLD stands for ``Common Object-oriented Language for Design''.
The pictorial notations used in this book provide strong links with the present state of the practice. Many methods, that are currently in use, are based on one or more of these notations. The book uses only existing kinds of pictorial notations. It puts them together in a coherent framework, based on COLD-1, and explains practical ways of exploiting them in conjunction with this language. Commonly, a COLD-1 text provides many details whereas each picture presents a particular view that could be obtained from the text by leaving out a lot. The pictures are used to enrich the formal text, but they miss the mathematical precision of the formal text, which guarantees that the design can be rigorously analysed. The pictorial notations addressed include Venn diagrams, state charts, HOOD diagrams, state transition diagrams, data flow diagrams, flow charts, Petri nets, SDL-like diagrams and sequence charts.
The accent of the book is on explaining formal notations for software design. COLD-1 is used because it is a wide-spectrum language: software systems can be described at many levels of detail, in any well-suited combination of styles and according to various paradigms. An additional virtue is the apposite support of modularity, which is important to cope with the size and complexity of many systems. Its permissive mechanisms for naming are also very convenient in practice. The book treats the language in a practical and user-oriented way: the examples, explanations and pictures convey a working knowledge about the meaning of the language constructs. The links established between formal notations and pictorial notations are helpful in two ways: they impart an intuition about the formal notations and they deepen the understanding of the pictorial notations.
COLD-1 was developed at the Philips Research Laboratories in Eindhoven. It is the result of insights gained during about a decade of work in cooperation with industrial divisions of Philips, academic research groups and partners in the ESPRIT projects METEOR and ATMOSPHERE. It has been put into use for real product design within Philips.
This book is intended to be used in software engineering courses. It is also suited for self-study. Some familiarity with logic and elementary set theory is assumed. The book provides material which is suitable for practitioners in software development who are interested in formal notations for software design. The material will also be valuable for students of computer science. Most of it has been used in industrial training courses as well as in academic courses at undergraduate level.
The book is organized as follows. The first part, consisting of Chapters 1 and 2, gives an introduction and a first case study. This part is meant to excite interest in the later chapters and to make them more comprehensible. After reading Chapter 2, which is a case study concerning a vending machine, the reader will be familiar with important COLD-1 notations and pictorial notations. The second part, consisting of Chapters 3, 4 and 5, gives a systematic treatment of all COLD-1 notations. Chapter 3 is concerned with definitions, axioms and theorems, Chapter 4 with modularization, and Chapter 5 with issues related to names, such as overloading and strong typing. The third part, consisting of Chapters 6 to 9, contains a large case study, material on pictorial notations and advanced topics. This part shows the notations in action. Chapter 6, which is a large case study concerning a computer-controlled railway system, shows how the COLD-1 notations presented in the second part can be put to work and used effectively. Chapters 7 and 8 give a systematic treatment of many important pictorial notations and their connections with COLD-1. Finally, Chapter 9 connects several well-established principles, guidelines and techniques of specification and design with COLD-1.
The concrete syntax of COLD-1 is presented in Appendix A. Specifications of the common data types used in this book -- extracted from IGLOO, the ``standard library'' associated with COLD-1 -- are given in Appendix B. A glossary of the terms connected with formal approaches to software development, so far as they are used in this book, are given in Appendix C.