Complexity of Synthesizing Inductive Assertions
Ben Wegbreit · Journal of the ACM · 1977
As an adlunct to mechamcal program verification, it is desirable to partmlly mechamze mductwe assertion synthesis.It is generally beheved that mechanical synthesis must be confined to simple assertions or simple extensions to programmer supphed assertions since the general problem of synthesis reqmres deep insight into the program's operation This paper confirms and quantifies this behef A class {R} of programs Is described for which the inductive assertions can be produced directly Then, by extending this class, a new class is obtained for which assertion synthesis reqmres at least nondetermlnlSUC polynomial t~me In fact a specific subset is shown to be NP-complete This yields two results, First, since nondetermimstlc polynomial ume ~s strongly conlectured to require determlmstlc exponenual time, it appears that the general problem of asserUon synthesis Is at least exponentml.Second, the extension from the class {R} is thus shown to be a cause of this time complexity The result is a better understanding of the difficulty of assertion synthesis and its cause KEY WORDS AND PHRASES synthesizing inducuve asseruons, program venficaUon, prowng programs correct, loop lnvarlants, mduct~on ca CATEGOrieS 3 64, 4 19, 4 22, 5.21, 5 24, 5,25 1 IntroducttonIn recent years there'has been considerable work in mechanical program verification, principally using the method of inductive assertions [8].As the explicit specification of inductive assertions by the programmer ts a tedious and error-prone task, much attention has been given to the subproblem of synthesizing, completing, and debugging inductive assertions [1-3, 5-7, 9, 10, 13, 14, 17-19].It seems plausible that practical success will come of this work in the following sense: A mechanical verification system will ultimately be able to accept a program with obvious or relatively unimportant assertions omitted, fill in the details, and verify the program.This raises the question as to whether assertion synthesis is inherently confined to filling in details or whether, on the contrary, it is possible to synthesize assertions by a uniform procedure.In stating this question it is necessary to exercise care since (a) verifying the synthesized assertions requires theorem proving which, for all but the simplest domains, is not uniformly decidable, and (b) assertion synthesis can always be carried out by generating all well-formed formulas as trial assertions.In view of these two caveats, a better phrasing of the question is: Suppose some program with a complete set of inducttve assertions can be verified or rejected in some time N. What can be said concerning the vertfication or reiectton time if the inducuve assertlons are omitted?The principal result of this paper is showing that at least nondeterministic polynomial time is required in the worst case.Since it is strongly conlectured that nondeterministic polynomial time requires deterministic exponential time [12], tt is very likely that assertion synthesis can add exponential ttme to verification.The second result of this paper is a characterization of the circumstances which make assertion synthesis difficult To this end, we exhibit a class {R} of programs for which correct assertions can be obtained directly from the input/output specifications Then, by violating one of the rules Copyrxght