In this paper we present how refactoring of object-oriented programs can be accomplished by using formal refinement. Our approach is based on the use of refactoring rules designed for a sequential object-oriented language of refinement (rool) similar to Java. We define a strategy that aims at structuring programs according to a layered architecture that involves the application of refactoring rules, object-oriented programming laws, and data and algorithm refinement. As the laws are proved in a weakest precondition semantics of rool, correctness of refactoring is ensured by construction.
Márcio Cornélio, Ana Cavalcanti, & Augusto Sampaio. (2005). Refactoring Towards a Layered Architecture. Electronic Notes in Theoretical Computer Science, 130, 281–300.