rdf-syntax-grammar
mods:
  schema location: http://www.loc.gov/mods/v3 http://www.loc.gov/standards/mods/v3/mods-3-2.xsd
  title info:
    title: Algebraic semantics of imperative programs
  name:
    name part: Goguen, Joseph.
    role:
      role term: creator
  name:
    name part: Malcolm, Grant.
  type of resource: text
  genre: bibliography
  genre: Electronic books.
  origin info:
    place:
      place term: mau
    place:
      place term: Cambridge, Mass
    publisher: MIT Press
    date issued: ©1996
    date issued: 1996
    issuance: monographic
  language:
    language term: eng
  physical description:
    form: remote
    extent: 1 online resource (vii, 228 pages) : illustrations.
  abstract: 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.
  note: Joseph A. Goguen and Grant Malcolm.
  subject:
    topic: Programming languages (Electronic computers)
    topic: Semantics
  subject:
    topic: Algebra
  subject:
    topic: COMPUTER SCIENCE/Theoretical Computer Science
  classification: QA76.7 .G62 1996eb
  classification: 005.13/1
  identifier: 0262288451
  identifier: 9780262288453
  identifier: 026207172X
  identifier: 9780262071727
  identifier: 026240365X
  identifier: 9780262403658
  identifier: http://proxy.library.tamu.edu/login
  record info:
    record content source: OCoLC-P
    record creation date: 130208
    record change date: 20221121162616.0
    record identifier: in00004602192
    language of cataloging:
      language term: eng