Formal Specification and Verification of Java Refactorings
Formal Specification and Verification of Java Refactorings
复制标题
Java 重构的形式化规范和验证
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
J. Meseguer
中科院分区：
文献类型：
--
作者：
A. Garrido;J. Meseguer
有大量关于面向对象程序重构的文献，以及许多用于Java编程语言的重构工具。然而，除了少数研究，在实践中很难找到精确的形式化规范的先决条件和自动重构的机制。此外，通常没有正式的证据证明重构是正确的，即，它保留了程序的行为我们提出了一种基于等式语义的Java重构方法。具体来说，我们使用可执行的Java形式语义的Maude语言：（i）正式指定三个有用的Java重构;和（ii）给这些重构的正确性的详细证明，表明他们是行为保持变换。除了为重构工具构建者提供严格的规范和严格的正确性保证的明显好处外，我们的方法还具有可执行性的额外优势：我们的正式重构规范可以直接用于重构Java程序，并产生可证明正确的Java重构工具。
There is an extensive literature about refactorings of object-oriented programs, and many refactoring tools for the Java programming language. However, except for a few studies, in practice it is difficult to find precise formal specifications of the preconditions and mechanisms of automated refactorings. Moreover, there is usually no formal proof that a refactoring is correct, i.e., that it preserves the behavior of the program. We present an equational semantics based approach to Java refactoring. Specifically, we use an executable Java formal semantics in the Maude language to: (i) formally specify three useful Java refactorings; and (ii) give detailed proofs of correctness for two of those refactorings, showing that they are behavior-preserving transformations. Besides the obvious benefits of providing rigorous specifications for refactoring tool builders and rigorous correctness guarantees, our approach has the additional advantage of its executability: our formal refactoring specifications can be used directly to refactor Java programs and yield a provably correct Java refactoring tool.