Soundness of a Logic-Based Verification Method for Imperative Loops

We present a logic-based verification method for imperative loops (including ones with abrupt termination) and the automatic proof of its soundness. The verification method consists in generating verification conditions for total correctness of an imperative loop annotated with an invariant. We realized, in the Theorema system (www.theorema.org), the automatic proof of the soundness of verification method: if the verification conditions hold, then the imperative loop is totally correct with respect to its given invariant. The approach is simpler than the others because it is based on functional semantics (no additional theory of program execution is necessary) and produces verification conditions in the object theory of the program. The computer-supported proofs reveal the minimal collection of logical assumptions (some from natural number theory) and logical inferences (including induction) which are necessary for the soundness of the verification technique.