Date: Tue, 1 Oct 1996 21:29:29 -0300 (ADT)
Subject: New Book
Date: Mon, 30 Sep 1996 20:26:31 -0700 (PDT)
From: Joseph Goguen
The book described below does not explicitly use category theory, but almost
everything in it was inspired in one way or another by category theory, and
so some members of this community may be interested in it. I want to express
my thanks to all of you for the wonderful work you are doing, which has
contributed so much to my own personal pleasure and professional life.
With warm regards to all,
Joseph
******************************************************************************
MIT Press has just published an "executable" book for a standard computer
science course, the semantics of imperative programs. In our experience,
being able to execute the semantics and the proofs greatly helps the students'
intuitions and motivation. Some details from the publisher are given below.
******************************************************************************
ALGEBRAIC SEMANTICS OF IMPERATIVE PROGRAMS
Joseph A. Goguen and Grant Malcolm
MIT Press, July 1996
This book is a novel self-contained "executable" introduction to formal
reasoning about 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.
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.
******************************************************************************
CONTENTS
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
A Summary of the Semantics
B First Order Logic and Induction
C Order Sorted Algebra
D OBJ3 Syntax
E Instructors' Guide
*************************************************************************
Prof. Joseph A. Goguen, Dept. Computer Science & Engineering, University of
California at San Diego, 9500 Gilman Drive, La Jolla CA 92093-0114, USA
email: jgoguen@ucsd.edu
www: http://www.comlab.ox.ac.uk/oucl/people/joseph.goguen.html
http://www-cse.ucsd.edu/users/goguen [nothing here yet!]
phone: (619) 534-4197 [my office]; -1246 [dept office]; -7029 [dept fax];
(619) 822-0702 [secy: Lisa Bodecker]
office: 3131 Applied Math & Physics Bldg.