Joseph A. Goguen

  • Algebraic Semantics of Imperative Programs

    Algebraic Semantics of Imperative Programs

    Joseph A. Goguen and Grant Malcolm

    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.

    • Hardcover $45.00
  • Research Directions in Object-Oriented Programming

    Gul Agha, David Beech, Daniel G. Bobrow, Ole-Johan Dahl, Joseph A. Goguen, Brent Hailpern, Kenneth M. Kahn, Ole Lehrmann Madsen, David Maier, Andrea Skarra, Harold L. Ossher, Steven Reiss, Herbert Schwetman, Reid Smith, Alan Snyder, Peter Wegner, and Stanley Zdonik

    Once a radical notion, object-oriented programming is one of today's most active research areas.

    Once a radical notion, object-oriented programming is one of today's most active research areas. It is especially well suited to the design of very large software projects involving many programmers all working on the same project. The original contributions in this book will provide researchers and students in programming languages, databases, and programming semantics with the most complete survey of the field available. Broad in scope and deep in its examination of substantive issues, the book focuses on the major topics of object-oriented languages, models of computation, mathematical models, object-oriented databases, and object-oriented environments. The object-oriented languages include Beta, the Scandinavian successor to Simula (a chapter by Bent Kristensen, whose group has had the longest experience with object-oriented programming, reveals how that experience has shaped the group's vision today); CommonObjects, a Lisp-based language with abstraction; Actors, a low-level language for concurrent modularity; and Vulcan, a Prolog-based concurrent object-oriented language. New computational models of inheritance, composite objects, block-structure layered systems, and classification are covered, and theoretical papers on functional object-oriented languages and object-oriented specification are included in the section on mathematical models. The three chapters on object-oriented databases (including David Maier's "Development and Implementation of an Object-Oriented Database Management System," which spans the programming and database worlds by integrating procedural and representational capability and the requirements of multi-user persistent storage) and the two chapters on object-oriented environments provide a representative sample of good research in these two important areas.

    Research Directions in Object-Oriented Programming is included in the Computer Systems series, edited by Herb Schwetman.

    • Hardcover $75.00