SOS C- : A SYSTEM FOR INTERPRETINGOPERATIONAL SEMANTICS OF C- PROGRAMS

This paper describes a system for automatically trans- forming programs written in a simple imperative language (called C--), into a set of first-order equations. This means that a set of first-order equations used to represent a C-- program already has a precise mathematical meaning; moreover, the standard techniques for mechanizing equa- tional reasoning can be used for verifying properties of pro - grams. This work shows that simple imperative programs can be seen as fully formalized logical systems, within which theorems can be proved. The system itself is formu- lated abstractly as a set of first-order rewrite rules. Then, it is proven to be terminating and confluent using the RRL system.