Algebraic semantics of imperative programs / (Record no. 73122)
[ view plain ]
| 000 -LEADER | |
|---|---|
| fixed length control field | 03301nam a2200517 i 4500 |
| 001 - CONTROL NUMBER | |
| control field | 6267468 |
| 005 - DATE AND TIME OF LATEST TRANSACTION | |
| control field | 20220712204714.0 |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION | |
| fixed length control field | 151229s1996 maua ob 001 eng d |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| ISBN | 9780262288453 |
| -- | electronic |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| -- | |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| -- | hc : alk. paper |
| 082 00 - CLASSIFICATION NUMBER | |
| Call Number | 005.13/1 |
| 100 1# - AUTHOR NAME | |
| Author | Goguen, Joseph, |
| 245 10 - TITLE STATEMENT | |
| Title | Algebraic semantics of imperative programs / |
| 300 ## - PHYSICAL DESCRIPTION | |
| Number of Pages | 1 PDF (vii, 228 pages) : |
| 490 1# - SERIES STATEMENT | |
| Series statement | Foundations of computing |
| 520 ## - SUMMARY, ETC. | |
| Summary, etc | 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. |
| 650 #0 - SUBJECT ADDED ENTRY--SUBJECT 1 | |
| General subdivision | Semantics. |
| 700 1# - AUTHOR 2 | |
| Author 2 | Malcolm, Grant. |
| 856 42 - ELECTRONIC LOCATION AND ACCESS | |
| Uniform Resource Identifier | https://ieeexplore.ieee.org/xpl/bkabstractplus.jsp?bkn=6267468 |
| 942 ## - ADDED ENTRY ELEMENTS (KOHA) | |
| Koha item type | eBooks |
| 264 #1 - | |
| -- | Cambridge, Massachusetts : |
| -- | MIT Press, |
| -- | c1996. |
| 264 #2 - | |
| -- | [Piscataqay, New Jersey] : |
| -- | IEEE Xplore, |
| -- | [1996] |
| 336 ## - | |
| -- | text |
| -- | rdacontent |
| 337 ## - | |
| -- | electronic |
| -- | isbdmedia |
| 338 ## - | |
| -- | online resource |
| -- | rdacarrier |
| 588 ## - | |
| -- | Description based on PDF viewed 12/29/2015. |
| 650 #0 - SUBJECT ADDED ENTRY--SUBJECT 1 | |
| -- | Programming languages (Electronic computers) |
| 650 #0 - SUBJECT ADDED ENTRY--SUBJECT 1 | |
| -- | Algebra. |
No items available.