论文部分内容阅读
重构可以改进既有软件的设计、提高软件质量,是一种行为保持的转化过程。自动化重构工具的广泛使用使得提高它的可靠性变得十分重要,然而即使是很简单的重构方法仍会导致许多错误,这些错误将会导致程序转换前后的行为不一致。因此提出对重构方法的形式化验证,只有这样才能将分析覆盖到所有可能的情况,完全地保证重构前后程序行为的一致性,即重构过程的正确性。该研究方向对软件发展的前景是十分有利的,但同时在程序验证的挑战性上也是十分巨大的。分析了基于分解的重构验证方法,并应用该验证方法,选择重构方法之一的"搬移字段"方法进