AMAST Mail 1996
[Prev][Next][Index]

new book

Dear Pippo,

I wonder if you would you be so kind as to forward the material below to the
AMAST list?  I think will interest many people there.

By the way, I have not been recieving copies of digests recently; has anything
gone wrong?  Perhaps it is due to my change of address?  And how are you?  I
hope that everything is going very well indeed.

With thanks,

Joseph


******************************************************************************
MIT Press has just published a book which uses algebra in a major way for a
standard computer science course, the semantics of imperative programs, making
the course "executable," and in our experience, greatly helping the students'
intuitions and motivation.  In case the readers of this list may be
interested, some details from the publisher are given below.

With kind regards to all, 

Joseph

(Please note change of address 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.

------- End of forwarded message -------
[ AMAST Mail 1996 | Latest Update | AMAST Mail Meta-Index | AMAST ]