Verification Of Refactoring Based On Decomposition

Refactoring is the process of improving the design and quality of existingsoftware by behavior—preserving transformations It is essential to improve thereliability of automated refactoring tools which have been extensively used,however,even very simple rei~actorings may encounter many bugs that lead tonon—behavior preserving transformations Thus the topic about formalverification ofrei~actoring has come up,only in this way can analysis cover eachpossible situation and totally ensure the program behavior preserved,1 e,correctness of the rei~actoring process This topic has offered the prospect oftangible benefits for software development but also significant challenges forverification This paper analyzes the verification methodology of refactoringbased on decomposition,by applying it,chooses one of the rei~actorings"MoveField"to give detailed analysis and verificationThe paper'S main achievements include:(1)This paper analyzes the refactoring verification methodology ofrefactoring,giving detailed analysis in aspects of establishing correctnesscriterion,decomposition on refactoring and object language,implementationformalization,verification and proof It provides the theoretical principle throughout the paper(2) According to the classification of specific refactorings,this paperchooses a proper refactoring called"Move Field"to verify,and follows the stepsof analysis,specification and verification to the method,meanwhile,it alsoverifies the correctness ofthe framework on which the refactoring dependIn summary,this paper analyzes the methodology of decomposition on bothrefactoring itself and the object language,takes the refactoring method"MoveField"as an example to give detailed analysis and description on decomposition,specification and verification This paper makes a certain contribution towardthe work on refactoring verification...