zbMATH — the first resource for mathematics

RAISE specification language. (English) Zbl 0835.68076
BCS Practitioner Series. New York, NY: Prentice Hall. xix, 396 p. (1992).
This is yet another textbook on formal specification, design, and implementation of software. It describes the specification language RAISE (= rigorous approach to industrial software engineering), which allows professional programmers to formulate a property-oriented specification as well as an operational design. The language is based on the well-known ideas on abstract data types that has been researched since the beginning of the seventies, but it also includes more recent concepts on concurrency, nondeterminism, and subtypes. Therefore, the system is suited for a wide spectrum of applications; a tool set is commercially available.
The main part of the book (chapters 2-33) is a tutorial intended as an introduction, whereas the remaining chapters (34-49) can be seen as a reference manual. The tutorial starts with presenting the applicative features and then proceeds to sequential concepts. Finally, concurrency and modules are discussed. This tutorial is well-presented and fulfills its intention; especially, the database example, introduced in chapter 3 and adopted in later chapters again and again, gives a good idea of the concepts of RAISE. The reader, however, must already have a good knowledge of abstract data types and formal proofs. Unfortunately, there are no exercises. Very good features are the bibliography and the clearly arranged index, although the reviewer has not found the index of examples that is announced on p. 389.

68Q60 Specification and verification (program logics, model checking, etc.)
68Q65 Abstract data types; algebraic specification
68-01 Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science