| 000 | 03301nam a2200517 i 4500 | ||
|---|---|---|---|
| 001 | 6267468 | ||
| 003 | IEEE | ||
| 005 | 20220712204714.0 | ||
| 006 | m o d | ||
| 007 | cr |n||||||||| | ||
| 008 | 151229s1996 maua ob 001 eng d | ||
| 010 | _z 95047440 (print) | ||
| 020 |
_a9780262288453 _qelectronic |
||
| 020 |
_z9780262071727 _qprint |
||
| 020 |
_z026207172X _qhc : alk. paper |
||
| 035 | _a(CaBNVSL)mat06267468 | ||
| 035 | _a(IDAMS)0b000064818b44a8 | ||
| 040 |
_aCaBNVSL _beng _erda _cCaBNVSL _dCaBNVSL |
||
| 050 | 4 |
_aQA76.7 _b.G62 1996eb |
|
| 082 | 0 | 0 |
_a005.13/1 _220 |
| 100 | 1 |
_aGoguen, Joseph, _eauthor. _922964 |
|
| 245 | 1 | 0 |
_aAlgebraic semantics of imperative programs / _cJoseph A. Goguen and Grant Malcolm. |
| 264 | 1 |
_aCambridge, Massachusetts : _bMIT Press, _cc1996. |
|
| 264 | 2 |
_a[Piscataqay, New Jersey] : _bIEEE Xplore, _c[1996] |
|
| 300 |
_a1 PDF (vii, 228 pages) : _billustrations. |
||
| 336 |
_atext _2rdacontent |
||
| 337 |
_aelectronic _2isbdmedia |
||
| 338 |
_aonline resource _2rdacarrier |
||
| 490 | 1 | _aFoundations of computing | |
| 504 | _aIncludes bibliographical references (p. [223]-225) and index. | ||
| 506 | 1 | _aRestricted to subscribers or individual electronic text purchasers. | |
| 520 | _aAlgebraic 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. | ||
| 530 | _aAlso available in print. | ||
| 538 | _aMode of access: World Wide Web | ||
| 588 | _aDescription based on PDF viewed 12/29/2015. | ||
| 650 | 0 |
_aProgramming languages (Electronic computers) _xSemantics. _93865 |
|
| 650 | 0 |
_aAlgebra. _921222 |
|
| 655 | 0 |
_aElectronic books. _93294 |
|
| 700 | 1 |
_aMalcolm, Grant. _922965 |
|
| 710 | 2 |
_aIEEE Xplore (Online Service), _edistributor. _922966 |
|
| 710 | 2 |
_aMIT Press, _epublisher. _922967 |
|
| 776 | 0 | 8 |
_iPrint version: _z9780262071727 |
| 830 | 0 |
_aFoundations of computing _922604 |
|
| 856 | 4 | 2 |
_3Abstract with links to resource _uhttps://ieeexplore.ieee.org/xpl/bkabstractplus.jsp?bkn=6267468 |
| 942 | _cEBK | ||
| 999 |
_c73122 _d73122 |
||