Renaming Global Variables in C Mechanically Proved Correct
Most integrated development environments are shipped with refactoring tools. However, their refactoring operations are often known to be unreliable. As a consequence, developers have to test their code after applying an automatic refactoring. In this article, we consider a refactoring operation (re...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2016-07-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1607.02226v1 |
| _version_ | 1811200455457374208 |
|---|---|
| author | Julien Cohen |
| author_facet | Julien Cohen |
| author_sort | Julien Cohen |
| collection | DOAJ |
| description | Most integrated development environments are shipped with refactoring tools. However, their refactoring operations are often known to be unreliable. As a consequence, developers have to test their code after applying an automatic refactoring. In this article, we consider a refactoring operation (renaming of global variables in C), and we prove that its core implementation preserves the set of possible behaviors of transformed programs. That proof of correctness relies on the operational semantics of C provided by CompCert C in Coq. |
| first_indexed | 2024-04-12T02:04:38Z |
| format | Article |
| id | doaj.art-9019a3bab21949b7ac570de3a020dc19 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-12T02:04:38Z |
| publishDate | 2016-07-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-9019a3bab21949b7ac570de3a020dc192022-12-22T03:52:35ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802016-07-01216Proc. VPT 2016506410.4204/EPTCS.216.3:2Renaming Global Variables in C Mechanically Proved CorrectJulien Cohen0 Université de Nantes Most integrated development environments are shipped with refactoring tools. However, their refactoring operations are often known to be unreliable. As a consequence, developers have to test their code after applying an automatic refactoring. In this article, we consider a refactoring operation (renaming of global variables in C), and we prove that its core implementation preserves the set of possible behaviors of transformed programs. That proof of correctness relies on the operational semantics of C provided by CompCert C in Coq.http://arxiv.org/pdf/1607.02226v1 |
| spellingShingle | Julien Cohen Renaming Global Variables in C Mechanically Proved Correct Electronic Proceedings in Theoretical Computer Science |
| title | Renaming Global Variables in C Mechanically Proved Correct |
| title_full | Renaming Global Variables in C Mechanically Proved Correct |
| title_fullStr | Renaming Global Variables in C Mechanically Proved Correct |
| title_full_unstemmed | Renaming Global Variables in C Mechanically Proved Correct |
| title_short | Renaming Global Variables in C Mechanically Proved Correct |
| title_sort | renaming global variables in c mechanically proved correct |
| url | http://arxiv.org/pdf/1607.02226v1 |
| work_keys_str_mv | AT juliencohen renamingglobalvariablesincmechanicallyprovedcorrect |