Algebraic Semantics of Imperative Programs

Front Cover

Algebraic Semantics of Imperative Programs presents a self-contained and novel "executable" introduction to formal reasoning about imperative programs. The authors' primary goal is to improve programming ability by improving intuition about what programs mean and how they run.The semantics of imperative programs is specified in a formal, implemented notation, the language OBJ; this makes the semantics highly rigorous yet simple, and provides support for the mechanical verification of program properties.OBJ was designed for algebraic semantics; its declarations introduce symbols for sorts and functions, its statements are equations, and its computations are equational proofs. Thus, an OBJ "program" is an equational theory, and every OBJ computation proves some theorem about such a theory. This means that an OBJ program used for defining the semantics of a program already has a precise mathematical meaning. Moreover, standard techniques for mechanizing equational reasoning can be used for verifying axioms that describe the effect of imperative programs on abstract machines. These axioms can then be used in mechanical proofs of properties of programs.Intended for advanced undergraduates or beginning graduate students, Algebraic Semantics of Imperative Programs contains many examples and exercises in program verification, all of which can be done in OBJ.

 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

Introduction
1
Background in General Algebra and OBJ
11
Stores Variables Values and Assignment
51
Composition and Conditionals
67
Proving Program Correctness
79
Iteration
91
Arrays
109
Procedures
131
Some Comparison with Other Approaches
169
A Summary of the Semantics
175
B First Order Logic and Induction
185
Order Sorted Algebra
203
OBJ3 Syntax
209
Copyright

Common terms and phrases

About the author (1996)

Grant Malcolm is a Research Officer at the Oxford University Computing Laboratory.

Bibliographic information