This book is a novel self-contained executable introduction to formal reasoning about imperative programs, and can be used as a text for a standard course on the semantics of imperative programs. Its 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 both highly rigorous and simple, and also provides support for the mechanical verification of program properties. This novel approach, in our experience, greatly helps students' intuitions and motivation. The text can also be used as an introduction to universal algebra for computer scientists, and to applications of theorem proving.

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.

The book is intended for advanced undergraduate or beginning graduate students, and contains many examples and exercises in program verification, all of which can be done in OBJ. The material has been extensively field tested at Oxford University.

  0	Introduction

  1	Background in General Algebra and OBJ
  1.1	Signatures
  1.2	Algebras
  1.3	Terms
  1.4 	Variables
  1.5	Equations
  1.6	Rewriting and Equational Deduction
	  1.6.1	Attributes of operations
	  1.6.2	Denotational semantics for objects
	  1.6.3	The Theorem of Constants
  1.7	Importing Modules
  1.8	Literature
  1.9	Exercises

  2	Stores, Variables, Values and Assignment
  2.1	Stores, Variables, and Values
	  2.1.1	OBJ's built-in inequality
  2.2	Assignment
  2.3	Exercises

  3	Composition and Conditionals
  3.1	Sequential Composition
  3.2	Conditionals
  3.3	Structural Induction
  3.4	Exercises

  4	Proving Program Correctness
  4.1	Example:  Absolute Value
  4.2	Example:  Computing the Maximum of Two Values
  4.3	Exercises

  5	Iteration
  5.1	Invariants
	  5.1.1	Example:  greatest common divisor
  5.2	Termination
  5.3	Exercises

  6	Arrays
  6.1	Some Simple Examples
  6.2	Exercises
  6.3	Specifications and Proofs
  6.4	Exercises

  7	Procedures
  7.1	Non-recursive Procedures
	  7.1.1	Procedures with no parameters
	  7.1.2	Procedures with var-parameters
	  7.1.3	Procedures with exp-parameters
  7.2	Recursive Procedures
	  7.2.1	Procedures with no parameters
	  7.2.2	Procedures with var-parameters
  7.3	Exercises

  8	Some Comparison with Other Approaches

  Appendices:

  A	Summary of the Semantics
  B	First Order Logic and Induction
  C	Order Sorted Algebra
  D	OBJ3 Syntax
  E	Instructors' Guide