Search |  Contact |  SRI Home Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap.A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A ASRI International.  333 Ravenswood Avenue.  Menlo Park, CA 94025-3493. SRI International is a nonprofit corporation.

Publication in BibTeX Format

@TECHREPORT{AICPub765:1974, AUTHOR={Waldinger, R. J. and Levitt, K. N.}, TITLE={Reasoning About Programs}, ADDRESS={333 Ravenswood Ave., Menlo Park, CA 94025}, INSTITUTION={AI Center, SRI International}, MONTH={Mar}, NUMBER={86}, YEAR={1974}, KEYWORDS={Program verification}, ABSTRACT={This paper describes a theorem prover that embodies knowledge about programming constructs, such as numbers, arrays, lists, and expressions. The program can reason about these concepts and is used as part of a program verification system that uses the Floyd-Naur explication of program semantics. It is implemented in the QA4 language; the QA4 system allows many pieces of strategic knowledge, each expressed as a small program, to be coordinated so that a program stands forward when it is relevant to the problem at hand. The language allows clear, concise representation of this sort of knowledge. The QA4 system also has special facilities for dealing with commutative functions, ordering relations, and equivalence relations; these features are heavily used in this deductive system. The program interrogates the user and asks his advice in the course of a proof. Verifications have been found for Hoare’s FIND program a real-number division algorithm, and some sort programs, as well as for many simpler algorithms. Additional theorems have been proved about a pattern matcher and a version of Robinson’s unification algorithm. The appendix contains a complete, annotated listing of the deductive system and annotated traces of several of the deductions performed by the system.}, NOTE={Originally published October 1973; Revised March 1974} }

SRI International
©2014 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy