Investigating the Use of JML Contracts

Resumen

Design by Contract (DBC) is a methodology from formal methods research that aims the construction of quality software. With DBC the contracts become assertions that can be checked at runtime, fostering reliability for developers. In this work, we investigate the use of JML (Java Modeling Language) contracts by means of seven open-source projects and checked whether the contract used has some relationship with the kind of nonconformance that occurs in each project. For the projects considered, the most common contract types were precondition and postcondition. This result suggests developers apparently prefer to write pre- and postcondition clauses in comparison with invariants. Concerning the relationship between number of contract clauses and number of detected nonconformances, we found a moderate negative correlation; indicating that contracts with more clauses do not imply more nonconformances. This result may indicate developers who write bigger contracts tend to follow those contracts more closely.