Files in this item



application/pdfAlgebraic Seman ... ss of its Refactorings.pdf (201kB)
(no description provided)PDF


Title:Algebraic Semantics of the C Preprocessor and Correctness of its Refactorings
Author(s):Garrido, Alejandra; Meseguer, José; Johnson, Ralph
Subject(s):computer science
Abstract: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.
Issue Date:2006-02
Genre:Technical Report
Other Identifier(s):UIUCDCS-R-2006-2688
Rights Information:You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).
Date Available in IDEALS:2009-04-20

This item appears in the following Collection(s)

Item Statistics