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.