Automating Program Verification: Generating Automatic Methods to Determine the Behavior of Algorithms
by Charles D. Lindsey
Major: Computer Science
It was the purpose of the project to develop a windowed program (one which uses a graphical user interface allowing mouse usage, document windows, and menus). This program would apply the p->wp.s.r method, or a similar and proven method, to programs written in an altered guarded command language which may utilize non-tail recursive recursion.
Whether a certain program s will cause r to be true given that p is true can be determined for certain s by user of the p->wp.s.r method. This method is useable on programs written in the guarded command language created by Edsger Djikstra. This language supports iteration, assignment, program composition, and conditional execution. Programs in other languages composed of only these constructs can be translated to the guarded command language without much difficulty.
Computing the p->wp.s.r of an iteration s and some states r and p is complicated. An alternative method was constructed and refined during the project. It involves the programmer supplying certain information about the iteration’s intended behavior, through an invariant and bound function. There is a proven method of showing the iteration’s behavior regarding this information.
Creating C++ functions to utilize this created method and the forms of the p-> wp.s.r method and testing them has been the major accomplishment of the project thus far. I am still researching the verification of non-tail recursive procedures.
I originally requested the funding for computer upgrades, reference materials, and possibly living and travel expenses if it was necessary for me to continue working on the project during the summer. The upgrades to my computer seemed to cost less than I originally expected. Thus, I may be returning a fair amount of the funding originally rewarded.
The project is progressing as I expected. Along with researching the verification of recursive procedures, I am looking into interfacing the work I have done thus far with the Boyer-Moore theorem prover (a very powerful automated theorem prover).