A Calculus for Imperative Programs: Formalization and Implementation

As an extension of our previous work on imperative program verification, we present a formalism for handling the total correctness of While loops in imperative programs, consisting in functional based definitions of the verification conditions for both partial correctness and for termination.A specific feature of our approach is the generation of verification conditions as first order formulae, including the termination condition which is expressed as an induction principle.