Algebraic semantics of imperative programs
Author(s)
Bibliographic Information
Algebraic semantics of imperative programs
(MIT Press series in the foundations of computing)
MIT Press, c1996
Available at 28 libraries
  Aomori
  Iwate
  Miyagi
  Akita
  Yamagata
  Fukushima
  Ibaraki
  Tochigi
  Gunma
  Saitama
  Chiba
  Tokyo
  Kanagawa
  Niigata
  Toyama
  Ishikawa
  Fukui
  Yamanashi
  Nagano
  Gifu
  Shizuoka
  Aichi
  Mie
  Shiga
  Kyoto
  Osaka
  Hyogo
  Nara
  Wakayama
  Tottori
  Shimane
  Okayama
  Hiroshima
  Yamaguchi
  Tokushima
  Kagawa
  Ehime
  Kochi
  Fukuoka
  Saga
  Nagasaki
  Kumamoto
  Oita
  Miyazaki
  Kagoshima
  Okinawa
  Korea
  China
  Thailand
  United Kingdom
  Germany
  Switzerland
  France
  Belgium
  Netherlands
  Sweden
  Norway
  United States of America
Note
Includes bibliographical references and index
Description and Table of Contents
Description
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.
Table of Contents
- Part 1 Background in general algebra and OBJ: signatures
- algebras
- terms
- variables
- equations
- rewriting and equational deduction - attributes of operations, denotational semantics for objects, the theorem of constants
- importing modules
- literature. Part 2 Stores, variables, values, and assignment: stores, variables, and values - OBJ's built-in inequality
- assignment. Part 3 Composition and conditionals: sequential composition
- conditionals
- structural induction. Part 4 Proving programme correctness: example - absolute value
- sample - computing the maximum of two values. Part 5 Iteration: invariants - example - greatest common divisor
- termination. Part 6 Arrays: some simple examples
- exercises
- specifications and proofs. Part 7 Procedures: non-recursive procedures - procedures with no parameters, procedures with varparameters, procedures with expparameters
- recursive procedures - procedures with no parameters, procedures with varparameters. Part 8 Some comparison with other approaches
- summary of the semantics
- first order logic and induction
- order sorted algebra
- OBJ3 syntax
- instructors' guide.
by "Nielsen BookData"