Refactoring with contracts

Design by contract is a practical methodology for developing code together with its specification. The contract consists of class invariants and method pre-and postconditions. As the code is refactored, specifications of internal units change with the code. There are mutual influences between the code and the contract. The assertions that constitute the contract are Java expressions; refactorings such as rename method must change these assertions as well as the code. The contract has methodological implications, which serve as preconditions on some refactorings; these must be checked before performing those refactorings. In addition, some contract modifications follow from certain refactorings, and can be done automatically. Development environments that support design by contract must take these influences into account. We report on the implementation in Eclipse of several refactorings that involve both code and contract. These show how contracts are modified in response to code changes, how contracts prevent certain changes, and how new contracts are computed for newly-generated methods and classes