Automatically provable specifications
Sergio Antoy · 1987
In the first part of the dissertation a method of program verification based on an expressibility result of the weakest precondition is presented. A new formulation of the weakest precondition is obtained by solving a problem of inductive inference. It is shown that any loop can be annotated with I/O specifications which are most general, naturally provable, and expressive enough to be of interest in practical verifications. The relationships with traditional methods of verification are outlined and examples are presented. In the second part, the specifications for automatically proving theorems arising is actual verifications are formalized and a language for defining algebraic specifications is introduced. A theorem prover for verifying equations about data abstractions is described. The underlying model of computation of the theorem prover is a term rewriting system with built-in knowledge of equality and a general principle of explicit induction. Interesting aspects of the theorem prover are analyzed and examples of formal proofs presented. Beside studying a practical and effective method of loop verification, the research partially characterizes reasonable specifications and proves their importance for loop documention and maintenance. It is also argued that the complexity of the task can be reduced by various tools which, furthermore, can be applied to a class of problems much wider than loop correctness.