This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Introducing iteration into the Pure Lisp theorem prover
Sept. 1975 (vol. 1 no. 3)
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.
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
Usage of this product signifies your acceptance of the Terms of Use.