The term 'refactor' means to change the structure of your code in some way that preserves its behaviour. However usually we don't tend to have all that much in the way of guarantees, or verification that what we did was successful.
The options available to do so would be:
- To use a pre-existing tool to do the refactor for you (but this may involve certain expectations on the format of your code, e.g. it may require the code to be a library)
- To "roll your own" verifier from scratch, particular to your needs.
In the next section I'm going to discuss both in regards to a specific problem, a 'simple' task of removing an antipattern known as "early returns".
This post is the 1st of a series on Refactor verification, investigating how to verify the correctness of refactors (or automating the human error away). Read on for discussion of early returns