On the Representation of Imperative Programs in a Logical Framework

摘要

Research on formal verification of imperative programs using some form of representing them in a type theory has been done for years. Generally, the different approaches include a verification conditions generator, which from an annotated program including variants and invariants for while-loops and using a Hoare logic-like specification, produces some propositions to be proved in a logical framework, expressing the program correctness and termination.In this paper we present a direct use of Coq [3] to model imperative programs. This method, and the fact that it is not possible to have not-ending programs in Coq, should allow a more deep understanding of imperative programs semantics [15], and people without big knowledge on type theory could use this theorem prover to verify imperative programs properties. This approach is based on using a fixed-point equality theorem [2] that represents the appropriate reduction rule to be used in our model.In our approach no Hoare logic rules are used for verification of program specifications. This verification is achieved, in a pure constructive setting, directly with the type theory model.