Algebraic semantics of imperative programs / Joseph A. Goguen and Grant Malcolm.
1996
QA76.7 .G62 1996eb
Linked e-resources
Linked Resource
Online Access through The MIT Press Direct
Details
Title
Algebraic semantics of imperative programs / Joseph A. Goguen and Grant Malcolm.
Author
Goguen, Joseph.
ISBN
0262288451 (electronic bk.)
9780262288453 (electronic bk.)
026207172X
9780262071727
026240365X
9780262403658
9780262288453 (electronic bk.)
026207172X
9780262071727
026240365X
9780262403658
Publication Details
Cambridge, Mass. : MIT Press, ©1996.
Language
English
Description
1 online resource (vii, 228 pages) : illustrations.
Call Number
QA76.7 .G62 1996eb
Dewey Decimal Classification
005.13/1
Summary
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.
Access Note
Access limited to authorized users.
Source of Description
OCLC-licensed vendor bibliographic record.
Added Author
Malcolm, Grant.
Record Appears in
Online Resources > Ebooks
All Resources
All Resources