A large software system often needs a precise specification of its intended behaviour. In order to achieve precision, specifications are written in a specification language with a well-defined syntax and formal semantics (a semantics by which the meaning of constructs in the language is precisely described using established concepts from mathematics). Formal specification refers to the use of such a specification language in writing specifications.
This book describes the outcome of a project which addressed the problem of giving a formal semantics for a specification language. This area is still in development. A main aim of this book is to illustrate a particular approach to tackle the problem of giving a formal semantics for a specification language. The language used for illustration, known as VVSL, extends VDM-SL (the specification language offered by the Vienna Development Method) with features for specifying interfering operations and for modular structuring of specifications. It is a specification language which is directly motivated by actual practices of software engineering.
The particular approach uses a mathematical framework for the semantics of specification languages consisting of the logic MPLomega, the algebra DA (a model of modular specification based on this logic) and lambda-pi-calculus (a variant of classical lambda calculus). It was first applied to the recently developed specification language COLD-K. This book contains a presentation of this mathematical framework and a presentation of a formal semantics of VVSL based on this framework. The latter presentation shows how MPLomega, DA and lambda-pi-calculus are used to give a formal semantics for a specification language. For that purpose, the approach could just as well be applied to another specification language. Indeed, it was applied to VVSL for another main purpose, viz. to provide VVSL with a formal semantics.
VVSL is an interesting specification language. It incorporates the version of VDM-SL used in Systematic Software Development using VDM by C.B. Jones -- published by Prentice Hall International. The extensions of VDM-SL aim to meet actual needs of advanced formal specification tasks (VVSL was first used to produce a formal specification of the PCTE interfaces). Another aim of this book is to demonstrate the practical usefulness of the extensions concerned for realistic specification tasks. It contains two complete formal specifications in VVSL.
One specification describes the basic concepts of the relational data model and the operations which can be performed by a hypothetical relational database management system. The other specification describes the underlying concepts and operations of a hypothetical system for handling concurrent access to a relational database by multiple transactions. Both specifications show how large specifications can be modularly structured in VVSL. The latter specification also shows how operations which interfere through shared state components can be specified in VVSL. Each of these specifications describes an idealization of existing systems of a certain kind. Either provides a reference point against which the correctness of proposed solutions to common problems in systems of the kind concerned can be established.
This book provides research material intended for academic and industrial researchers in computer science interested in formal specification in general or semantics of specification languages in particular. The material concerning semantics of specification languages does not get round real problems which are often not dealt with in theoretical work. This material matters mostly to researchers working on foundational issues of the semantics of specification languages and developers of specification languages. It can also be used as illustration in theoretical courses. Some background in mathematical logic and set theory is assumed. The case study type material is mainly interesting to developers of software systems who are interested in formal specification. It can be used in software engineering courses on formal specification. The case studies are instances of advanced formal specification. They deal with examples of practical application which are not simplified. The case studies are expected to appeal to researchers working on databases as well.
This book is organized as follows. Chapter 1 pays attention to the role of formal specification in formal methods for the development of software. Among other things, the main features of VDM-SL are outlined. The remaining chapters concentrate on VVSL. Chapter 2 gives a general overview of the special features of VVSL. Chapters 3 to 9 are concerned with giving a formal semantics for VVSL. The approach applied in this book uses a mathematical framework which is presented in Chapters 3 and 6. The appropriate specializations and generalizations of this framework for the semantics of VVSL are described in Chapters 4 and 7. The semantics itself is presented in Chapters 5 and 8. Chapter 9 discusses some points raised by the material in Chapters 3 to 8, but for which space could not be found there. Chapters 10 to 13 are concerned with advanced case studies in VVSL. The case studies are related to relational databases. An introduction to them is given in Chapter 10. The underlying concepts of relational database management systems and the operations for data manipulation and data definition which can be performed by such systems are described in Chapters 11 and 12, respectively. Underlying concepts and operations of systems for handling concurrent access to a relational database by multiple transactions are described in Chapter 13. A glossary of the mathematical notation used in this book is provided in Appendix A and a glossary of VVSL notation is provided in Appendix B.
This book is a major revision of my Ph.D. thesis, Syntax and Semantics of VVSL. It has been substantially rewritten and restructured so as to streamline the material. A number of technical changes have made it possible to simplify parts of the material that is concerned with giving a formal semantics for VVSL, including material on the mathematical framework which forms the basis of the semantics. The new Chapter 1 put the material into context.