The Community for Technology Leaders
Green Image
Issue No. 03 - Sept. (1975 vol. 1)
ISSN: 0098-5589
pp: 328-338
J Strother Moore , Xerox Palo Alto Research Center, Palo Alto, Calif. 94304
It is shown how the Lisp iterative primitives PROG, SETQ, GO, and RETURN may be introduced into the Boyer-Moore method for automatically verifying Pure Lisp programs. This is done by extending some of the previously described heuristics for dealing with recursive functions. The resulting verification procedure uses structural induction to handle both recursion and iteration. The procedure does not actually distinquish between the two and they may be mixed arbitrarily. For example, since properties are stated in terms of user-defined functions, the theorem prover will prove recursively specified properties of iterative functions. Like its predecessor, the procedure does not require user-supplied inductive assertions for the iterative programs.
Iterative methods, Artificial intelligence, Indexes, Packaging, Periodic structures, Argon, Equations, structural induction, Automatic theorem proving, Lisp, program verification

J. S. Moore, "Introducing iteration into the Pure Lisp theorem prover," in IEEE Transactions on Software Engineering, vol. 1, no. , pp. 328-338, 1975.
94 ms
(Ver 3.3 (11022016))