Algebraic Semantics of the C Preprocessor and Correctness of its Refactorings
Alejandra Garrido, José Meseguer, Ralph E. Johnson · Illinois Digital Environment for Access to Learning and Scholarship (University of Illinois at Urbana-Champaign) · 2006
Refactoring has become a popular technique for the development and maintenance of object-oriented systems. We have been working on the refactoring of C programs, including the C preprocessor (Cpp), and we have built CRefactory, a refactoring tool for C programs. The independence of Cpp from the underlying programming language complicates the analysis and refactoring of programs that use Cpp. Nevertheless, that independence is helpful when implementing refactorings on Cpp directives. While refactorings are defined as "behavior preserving transformations", there is usually no formal proof of their correctness. By using rewriting logic and its Maude implementation, we have formally specified the semantics of Cpp and also of some refactorings on Cpp directives. The specifications are then used to formally prove refactoring correctness. This paper describes the formal specifications of Cpp and of three of its refactorings, and presents the proofs of their correctness.