scientific article; zbMATH DE number 1042220

MaRDI QIDQ4346205zbMATH OpenFDO

Authors Joseph Goguen, Grant Malcolm

Publication date 3 August 1997

zbMATH Keywords

equational logic imperative programs MODULA2

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

This book presents a self-contained introduction to formal reasoning about imperative programs. It is intended to help undergraduate computing science students to acquire an understanding and basic skills in this subject. A thorough study of this book should improve intuition and ability in imperative programming. The reader is taught how to prove properties of programs while developing the relevant mathematical background. The authors maintain that this can be done in an completely rigorous way -- a way that is not too difficult and too abstract. They base their introduction upon equational logic, i.e. the logic for substituting equals for equals. As they go along, they define the algebraic semantics of imperative progams with recourse to abstract machines. Equational axioms specify the effect of programs on such machines. Programming language features covered in this book are assignment, sequential composition, conditional, while-loop, procedure definition and procedure call. The corresponding equational axioms are used to prove the correctness of programs. Although equational logic may not cover all idiosyncrasies of imperative programs, it has some advantages. For a start, it seems not to scare of that much undergraduate students. But there are more technical points in its favour. It is simple; many problems are decidable that are not in more complex logics; there are efficient algorithms for deciding many of these problems; there are mature tools that embody many of these algorithms. The reader is assumed to be familiar with some imperative programming language, such as C, Pascal, Basic or MODULA2. Furthermore, knowledge of basic mathematics including mathematical induction and first-order logic is required. Other concepts are explained when the need arises. In this book, OBJ, a language especially designed for algebraic semantics, is used to implement equational logic associated with imperative programs. It is introduced in the process. Actually, every OBJ program is an equational theory. Every OBJ computation proves some property about such a theory. With the prerequisites met, any reader should be able to get the gist of algebraic semantics of imperative programs via OBJ as developed in this exquisite textbook.

Recommendations

Cited in

(27)

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4346205)