Rewriting of imperative programs into logical equations

This paper describes SOSSubC: a system for automatically translating programs written in SubC, a simple imperative language, into a set of first-order equations. This set of equations represents a SubC 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 SubC 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.