Algebraic Semantics of the C Preprocessor and Correctness of its Refactorings

Garrido, Alejandra; Meseguer, José; Johnson, Ralph

Permalink

https://hdl.handle.net/2142/11162 Copy

Description

Title

Algebraic Semantics of the C Preprocessor and Correctness of its Refactorings

Author(s)

• Garrido, Alejandra
• Meseguer, José
• Johnson, Ralph

Issue Date

2006-02

Keyword(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."

Type of Resource

text

Permalink

http://hdl.handle.net/2142/11162

Copyright and License 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).

Owning Collections