A thought on the correctness of refactoring

The hard part about writing a refactoring tool isn’t the actual code transformation; it’s establishing that the code transformation you wrote didn’t break your code.

The traditional approach to validating the transform is to make it correct by construction.  The focus is on the correctness of the transformation in general, rather than a particular instance of the transformation as applied to a particular codebase.    Getting a transformation right for all possible code bases is hard and requires a lot of semantic knowledge about the language and all of its corner cases.  This is why semantic aware tools like clang-tidy, & clang-modernize are such a big deal.

It’s interesting to think about what the inverse might be.  There are certainly some code changes – regardless of how they’re performed – which are semantically preserving.  For example, replacing tabs with spaces in a C++ file probably doesn’t change a single bit in the final program.*  My strong suspicion is that there are entire classes of transformations which could be validated in this way.  In particular, I wonder how much of the program verification literature could be profitably adapted to this problem.

Assuming you could make this work, it would seem to make writing a one off refactoring tool one heck of a lot simpler.  You could write it using any combination of grep/awk and other text processing tools, not worry about getting it right in general, apply it and just check to see if the result was correct.  If it wasn’t, you fix the bug (exclude that file, be a bit smarter about the language construct, whatever) and repeat.

* For the purposes of this post, let’s ignore undefined behaviour.