Optimization of Inductive Assertions

Candidate: Warren,Henry Stanley,Jr.


Inductive assertions are assertions placed in the loops of a program, primarily for the purpose of aiding a mechanical correctness prover to prove that the program is correct. Here we assume that the assertions in a program are executed along with the program. That is, the predicate expression of each assertion is evaluated when encountered during program execution, to verify that its value is true. Inductive assertions are particularly expensive in terms of execution time. This is not only because they are in loops, but also because they are frequently themselves loops (quantified expressions). Thus executing them can slow a program's execution by a factor that can be indefinitely large. For example, executing them can change an O(n('2)) process to an O(n('3)) process. This thesis investigates the possibility of optimizing such quantified inductive assertions by substantially reducing the range of quantification. It is shown that many inductive assertions encountered in practice fall into a simple pattern in which the quantifier may, essentially, be removed. This restores the execution time of the program to the same order of magnitude that it would have been if the inductive assertions were not executed. Emphasis is placed on methods that are no more costly in compiler size and execution time than conventional global optimization techniques.