Generating algebraic laws from imperative programs

AbstractThe use of verifiers for proving the correctness of concrete programs is well known and has been amply described in the literature. Here we focus on further, perhaps more general tasks such verifiers can perform. Given a program that is assumed to be correct, we derive a set of axioms for the data structures involved. In the simplest case, we study an abstract program interchanging the contents of two variables. The verification conditions generated by our verifier, NPPV, are a set of equations specifying quasigroups. Other examples reveal the notion of “strategy” from the verification of an abstract game-playing program, or show the correspondence between inductive proofs of numeric properties and verification of a program searching for a counterexample. Finally, we apply NPPV on Wand's example showing the incompleteness of Hoare's logic. We also give a simplified proof of Wand's result