Proving Horn Clause Specifications of Imperative Programs

We present a method for verifying the correctness of an imperative program with respect to a specification defined in terms of a set of possibly recursive Horn clauses. Given a program prog, we consider a partial correctness specification of the form {phi} prog {psi}, where the assertions phi and psi are predicates defined by a set Spec of Horn clauses. The verification method consists in: (i) encoding the function computed by the program prog (according to the semantics of the imperative language) as a set OpSem of clauses, and then (ii) constructing a set PC of Horn clauses and a predicate p such that if p is false in the least model of PC, that is, M(PC) 6|= p, then {phi} prog {psi} is valid. We also present an extension of the verification method for showing total correctness of programs. Then we present a general proof technique based on unfold/fold transformations of Horn clauses, for checking whether or not M(PC) |= p holds. We also outline a strategy for guiding the application of the unfold/fold transformation rules and performing correctness proofs in an automatic way. Finally, we show some experimental results based on a preliminary implementation of our method.