Investigating the Use of JML Contracts

Authors

  • Alysson F. Milanez
  • Igor N. S. Ataı́de
  • Tiago L. Massoni

Abstract

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.

Downloads

Published

2022-03-21

Issue

Vol. 2 No. 5 (2021): (Edição Pocket) Anais do Encontro de Computação do Oeste Potiguar

Section

Artigos

Most read articles by the same author(s)

Obs.: This plugin requires at least one statistics/report plugin to be enabled. If your statistics plugins provide more than one metric then please also select a main metric on the admin's site settings page and/or on the journal manager's settings pages.