22C:185 Reserve List (2 hour)


S. Alagic' & M. A. Arbib, The Design of Well-Structured and Correct Programs, Springer-Verlag, 1978, 292 pp.  QA76.6 .A39

axiomatic program proving


R. Backhouse, Syntax of Programming Languages, Prentice-Hall  1979, 301 pp.  QA76.7 .B3

treatment of grammars/BNF


R. S. Boyer & J. S. Moore(eds.), The Correctness Problem in Computer Science, Academic Press, 1981, 279 pp. QA76.6 C663

why program correctness must be proven


W. F. Clocksin & C. S. Mellish, Programming in Prolog, Springer-Verlag, 1987 (4th ed.), 281 pp.  QA76.73.P356 C57


P. Deransart, M. Jourdan & B. Lorho, Attribute Grammars: definitions, systems and bibliography, Springer-Verlag, Lect. Notes in CS, V. 323, 1988, 232 pp.  QA76.7 .D46


J. A. Goguen & G. Malcolm, Algebraic Semantics of Imperative Programs, MIT Press, 1996, 225 pp.


M. J. C. Gordon, The Denotational Description of Programming Languages, Springer-Verlag, 1979, 160 pp.  QA76.7 .G67

informal intro to denotational semantics ideas


M. J. C. Gordon, Programming Language Theory and its Implementation, Prentice-Hall, 1988, 255 pp.  QA76.7 .G673

axiomatic program proving, and l-calculus


D. Gries, The Science of Programming, Springer-Verlag, 1981, 366 pp.

program derivation methodology


M. Hennessy, The Semantics of Programming Languages, Wiley, 1990, 157 pp.  QA76.7 .H45

operational and denotational semantics


Z. Manna, Mathematical Theory of Computation, McGraw-Hill, 1974, 448 pp.

fixpoint theory, program proving - an established reference


P. G. Neumann, Computer Related Risks, Addison-Wesley, 1995, 367 pp.

innumerable examples of catastrophes caused by  incorrect programs


R. D. Tennent, Semantics of Programming Languages, Prentice-Hall, 1991, 236 pp.  QA76.7 .T473

operational, denotational, and axiomatic approaches


R. T. Yeh, Current Trends in Programming Methodology, Vol. IV: Data Structuring, Prentice-Hall, 1978, 321 pp. QA76.6 .C87

see chaps 4 & 5 on algebraic specification