mural: a formal development support system.

*(English)*Zbl 0758.68046
Berlin etc.: Springer-Verlag. XIII, 421 p. (1991).

Systematic development of a software system proceeds by making data structures more concrete and by decomposing operations. Formal methods ensure that the version resulting from such a step is correct with respect to the previous version. Since even small examples lead to proofs of considerable size, formal methods cannot be used without appropriate support tools. The book presents such a tool that is called “mural” (an acronym referring to the organizations realizing the project) and that mainly consists of a VDM support tool and a proof assistant. The book is based on papers which were written during the project. Although they have been edited and some material is new, the book is primarily a research report and not a textbook. Without good knowledge of VDM or at least of another formal method, it is difficult to read.

The book is divided into eleven chapters and five appendices. The largest part is Appendix C (88 pp) containing the complete specification of the proof assistant. The first two chapters give a general introduction and an overview of the system. Chapters 3-6 describe the proof assistant in more detail. The third chapter is concerned with the ability of the system to support reasoning in different logics. The chapter illustrates how to set up the axiom systems for classical predicate calculus and for a logic of partial functions. The next chapter is a very detailed walk into the specification of the proof assistant and assumes the reader to be familiar with VDM. Chapter 5 presents the tactic language which allows the user to compose sequences of proof steps, and chapter 6 summarizes the lessons the authors learned during implementing the proof assistant. The following chapters are very short and discuss the support tool for working with VDM and a tool for simulating the behaviour of a specified system without actually implementing it. Chapter 10 presents two case studies: a watchdog for a reactor system and an algorithm for topological sorting.

To sum up, this book is a comprehensive presentation of both the structure of the “mural” system and of the ideas it is based on as well as of the experiences the authors made in realizing this system. It can be recommended to researchers in the field of formal program development.

The book is divided into eleven chapters and five appendices. The largest part is Appendix C (88 pp) containing the complete specification of the proof assistant. The first two chapters give a general introduction and an overview of the system. Chapters 3-6 describe the proof assistant in more detail. The third chapter is concerned with the ability of the system to support reasoning in different logics. The chapter illustrates how to set up the axiom systems for classical predicate calculus and for a logic of partial functions. The next chapter is a very detailed walk into the specification of the proof assistant and assumes the reader to be familiar with VDM. Chapter 5 presents the tactic language which allows the user to compose sequences of proof steps, and chapter 6 summarizes the lessons the authors learned during implementing the proof assistant. The following chapters are very short and discuss the support tool for working with VDM and a tool for simulating the behaviour of a specified system without actually implementing it. Chapter 10 presents two case studies: a watchdog for a reactor system and an algorithm for topological sorting.

To sum up, this book is a comprehensive presentation of both the structure of the “mural” system and of the ideas it is based on as well as of the experiences the authors made in realizing this system. It can be recommended to researchers in the field of formal program development.

Reviewer: H.J.Schneider (Erlangen)

##### MSC:

68Q60 | Specification and verification (program logics, model checking, etc.) |

68N01 | General topics in the theory of software |

68-02 | Research exposition (monographs, survey articles) pertaining to computer science |

03B70 | Logic in computer science |