Algebraic semantics of imperative programs.

*(English)*Zbl 0887.68066
MIT Press Series in the Foundations of Computing. Cambridge, MA: MIT Press. xii, 228 p. (1996).

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.

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.

Reviewer: R.Horsch (Markdorf)