Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
9657440 | Science of Computer Programming | 2005 | 39 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Olivier Ponsini, Carine Fédèle, Emmanuel Kounalis,