The software industry has suffered big changes in the last two decades and the number of companies working on this business domain is growing from year to year. Every year a significant number of software systems is developed or improved. The reuse of software components was found to be a way to ease the development process, and at the same time reduce the costs associated to it. It is widely believed that this technique will enable software developers to create bigger and more complex systems with guarantee on the its quality and reliability. Despite the failures to introduce reuse as a systematic process on the software development, many efforts have been made to achieve this goal.

The decision to reuse raises a spectrum of issues, from requirements negotiation to product selection and integration. All these issues can lead to an incorrect system, and aiming to that a strong demand for formal methods that help programmers to develop correct programs has been present in software engineering for some time now. The Design-by-Contract (DbC) approach to software development facilitates modular verification and certified code reuse.

The contract for a component can be regarded as a form of enriched software documentation that fully specifies the behavior of that component. So, a well-defined annotation can give us most of the information needed to integrate a reusable component in a new system, as it contains crucial information about some constraints safely obtaining the correct behavior from the component.

In this context, we say that the annotations can be used to verify the validity of every component invocation; in that way, we can guarantee that a correct system will still be correct after the integration of that component. This is the motivation for our research: to find a way to help on the safety reuse of annotated components.

Motivated by these promises of reuse and Design-by-Contract we developed a tool that allows us to to verify whether a concrete calling context preserves the precondition of the reused component, and display, whenever possible, a diagnostic or guidelines to correct any violation found during the verification. To achieve the objectives listed above, the tool implements the caller-based slicing algorithm, that takes into account the calls of an annotated component to certify that it is being correctly used.