What is the closest theory to "The theory of code refactoring"?

Question

We refactor code lots of times as developers. Metaphorically, our program space is an infinite-dimensional Rubik's cube. Things can be rearranged, preserving the code's action, so a "symmetry structure" is at play. You can do things in code that can be factored sort of like distributive law in a ring, but there are way more operations, so things are not that cut-and-dry.

If someone wanted to develop a next-generation IDE that is Refactoring-centered instead of having that as an auxillary feature added in later after centering things around an Editor and Debugger; then what theory should they study?

In other words what is the closest theory or topic in regards to the application of code refactoring? So the theory has to be taught but it also has to apply to real-world languages in a somewhat direct way, such as C++, Python, Java, etc.

Does such a theory exist already?

Answer 1

Basic code refactoring is not about symmetries but rather about equivalences. When code $C$ is transformed by refactoring to become code $C'$, we expect $C$ and $C'$ to "do the same thing". (This applies to simple forms of refactoring only.)

There are several notions of equivalence of code, such as:

• programs $P$ and $Q$ are equivalent when their mathematical meaning is the same
• programs $P$ and $Q$ are equivalent when they satisfy the same assertions in some program logics
• programs $P$ and $Q$ are equivalent when they cannot be distinguished in terms of their behavior

These slides might be helpful.

Anyhow, once a theory of equivalence is established, it can be used to make sure that code refactoring is done correctly, i.e., that no unintended changes in the code were made. People study this topic broadly, the slides linked to above should contain enough buzzwords for you to google around for more.

Of course, not all aspects of code refactoring are about program equivalence. In practice, one might make transformations that obviously change code (such as introducing a new method in a class definition). In such cases one would look at the topic of program transformation.