Rewriting of imperative programs into logical equations

This paper describes image: a system for automatically translating programs written in image, a simple imperative language, into a set of first-order equations. This set of equations represents a image program and has a precise mathematical meaning; moreover, the standard techniques for mechanizing equational reasoning can be used for verifying properties of programs. Part of the system itself is formulated abstractly as a set of first-order rewrite rules. Then, the rewrite rules are proven to be terminating and confluent. This means that our system produces, for a given image program, a unique set of equations. In our work, simple imperative programs are equational theories of a logical system within which proofs can be derived.