PEQcheck: Localized and Context-aware Checking of Functional Equivalence (Technical Report)

A refactoring must preserve the program's functionality. However, not all refactorings are correct. Preservation of the functionality must be checked. Since programs are rarely formally specified, we use the original program as functional specification and check whether the original and refactored program are functionally equivalent. More concretely, our PEQcheck technique follows a common approach and reduces equivalence checking to program verification. To increase efficiency, PEQcheck generates several verification tasks, namely one per refactored code segment and not one per function as typically done by prior work. Additionally, PEQcheck takes the context of the segments into account. For example, only modified, live variables need to be equivalent and read-only variables can be shared between original and refactored code segments. We proved soundness of our PEQcheck technique and implemented it in a prototype tool. Our evaluation shows that the localized checking of PEQcheck can indeed be beneficial.