Contract-Based Verification for Aspect-Oriented Refactoring

Refactoring is a method for improving a program´s structure without changing its external behavior. Refactoring is a promising approach to assist reliable and safe software evolution. However, in aspect-oriented programming (AOP), it is not necessarily easy for a programmer to understand the overall behavior of a woven program because the weaving modifies the behavior. Unexpected bugs can be embedded in a program if the programmer does not modify the program carefully. In order to deal with this problem, we propose the notion of RbC (refactoring by contract), a technique to verify refactoring based on contracts. Contracts in RbC consist of preconditions, postconditions, and invariants. A precondition states under which conditions refactoring can be applied. A postcondition states what condition should be verified after refactoring has been accomplished, and an invariant states what conditions refactoring should preserve. After introducing RbC, we check whether refactoring preserves behavior and whether it actually improves internal structure. A contract is described in COW (contract writing language), a language for describing a predicate based on first-order logic. COW provides a set of primitive predicates that represent program structure and behavior. Adopting our approach, software evolution in AOP becomes reliable and safe.