Refactoring is a behaviour - preserving transformation process which is able to improve the design of existing software and raise the quality of software. The extensive use of automated refactoring tools makes it essential to improve the reliability of refactoring. However, even very simple refactoring means may also encounter many bugs and these errors will lead to behaviour inconsistency of the program before and after transformation. Therefore the research direction about formal verification of refactoring approach is suggested, only in this way can the analyses be covered over all possible circumstances and totally ensure the consistency of the program behaviour before and after refactoring, i. e. , the correctness of refactoring process. This direction quite benefits the prospect of software development; meanwhile it is also a significant challenge on the program verification. In this paper we analyse the refactoring verification method based on decomposition, and by applying it, we choose one of the refactoring methods, " Field Moving" , to give detailed analysis and verification. This paper makes certain contribution to the research direction of meliorating the refactoring verification.%重构可以改进既有软件的设计、提高软件质量,是一种行为保持的转化过程.自动化重构工具的广泛使用使得提高它的可靠性变得十分重要,然而即使是很简单的重构方法仍会导致许多错误,这些错误将会导致程序转换前后的行为不一致.因此提出对重构方法的形式化验证,只有这样才能将分析覆盖到所有可能的情况,完全地保证重构前后程序行为的一致性,即重构过程的正确性.该研究方向对软件发展的前景是十分有利的,但同时在程序验证的挑战性上也是十分巨大的.分析了基于分解的重构验证方法,并应用该验证方法,选择重构方法之一的“搬移字段”方法进行了详细的分析和验证.在完善重构验证这一研究方向作出了一定贡献.
展开▼
