The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.03 - Sept. (1975 vol.1)
pp: 328-338
J Strother Moore , Xerox Palo Alto Research Center, Palo Alto, Calif. 94304
ABSTRACT
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.
INDEX TERMS
Iterative methods, Artificial intelligence, Indexes, Packaging, Periodic structures, Argon, Equations, structural induction, Automatic theorem proving, Lisp, program verification
CITATION
J Strother Moore, "Introducing iteration into the Pure Lisp theorem prover", IEEE Transactions on Software Engineering, vol.1, no. 3, pp. 328-338, Sept. 1975, doi:10.1109/TSE.1975.6312857
35 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool