Is there any formal definition for "refactoring"?

Question

Anyone knows a way to define refactoring in a more formal way?

UPDATE.

A refactoring is a pair R = (pre; T) where pre is the precondition that the program must satisfy, and T is the program transformation.

Answer 1

It's an interesting question and one I hadn't considered. I did a little googling and came up with this paper (PDF) on refactoring in AOP that attempts to apply some mathematical modeling to aspects to show the that functional aspects have the same flexibility as traditional aspects but with reduced complexity. I didn't read the whole paper, but you might find something there.

Another interesting idea would be to think of refactorings along the same lines as compiler optimizations. Essentially, the compiler refactors your code on the fly, although with different goals than code-level refactoring. You'd have to somehow quantify code complexity and readability in a reasonable way to demonstrate how a particular refactoring affects it. Coming up with the model would probably be the hard part.

I also found this paper that establishes an algebra of OO programming and derives some basic laws, then uses those basic rules to derive a more complicated refactoring.

Interesting stuff. Hope this helps.

Answer 2

refactoring is a series of correctness-preserving transformations, but refactoring may result in more general code than the original

so we can't just assert that a refactoring transformation T on program P has the same properties R before and after refactoring, but the properties R' of the refactored program P' should be at least equivalent to R

given program P implies R
refactoring transformation T(P) produces P'
where (P' implies R') and (R' is equivalent to or subsumes R')

we can also assert that the inputs and outputs remain the same or equivalent

but to follow your example, perhaps we want to define a refactoring transformation T as a 4-tuple P,I,O,R where P is the original program, I is the inputs and/or preconditions, O is the outputs and/or postcondition, and R is the transformed program, then assert (using temporal logic?) that

P:I -> O

holds before transformation

T(P) -> R

defines the transformation, and

R:I -> O

holds after transformation

my symbolic math is rusty, but that's a general direction

this would make a good master's thesis, BTW

Answer 3

It could be interesting to note that most of the Refactorings come in pairs:

• Add Parameter - Remove Parameter
• Extract Class/Method - Inline Class/Method
• Pull Up Field/Method - Pull Down Field/Method
• Change Bidirectional Association to Unidirectional - Change Unidirectional Association to Bidirectional
• ...

Applying the two refactorings of the pair is a null transformation.

For a refactoring pair R, R' :

R'(R(code)) = code