Renaming Global Variables in C Mechanically Proved Correct

TL;DR

This paper presents a formally verified method for renaming global variables in C, ensuring that the refactoring preserves program behavior, based on a proof using the operational semantics of C in Coq.

Contribution

It introduces a mechanically proved correct approach to global variable renaming in C, leveraging formal semantics and proof assistants.

Findings

Refactoring preserves program behavior as proven in Coq.

The approach enhances reliability of IDE refactoring tools.

Formal proof guarantees correctness of the renaming operation.

Abstract

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.