Bad smells naturally arise in source code, usually as a consequence of ad hoc evolution. These smells consist of symptoms that convey likely problems, even though the program is working correctly. Examples of bad smells in object-oriented programs that motivate refactorings [1] stem from classes or methods that are too long to classes using more members from other classes than its own members (Feature Envy [1]). Refactoring activities are often motivated by the detection of bad smells.

Design-by-Contract (DBC) [2] establishes a method for building software by explicitly specifying what each function in a module requires in order to correctly operate, and also specifying what it provides to the caller (contracts). They constitute a collection of assertions— mainly invariants and pre- and post-conditions for methods— that precisely describe what methods require and ensure with respect to client classes. Although DBC is a built-in development method for the Eiffel programming language [3], contracts can also be written with extensions to general-purpose languages, such as the Java Modeling Language (JML) [4].

With the increasing adoption of DBC methodologies in formal software development, evidence of bad design practices can similarly be found in programs that combine actual production code with contracts. If these problems are not addressed properly, they may hinder the quality benefits of DBC development, such as encapsulation, maintainability, and readability.

In this paper, we present a catalog of bad smells that may appear during DBC practice. Six smells were catalogued for this paper; and are described in detail. Smells include symptoms like long specifications with several alternative behavior cases (Long Specs), private fields exposed in public contracts (Open Doors), excessive accesses to fields that represent internal data (Field Obsession), and complex predicates that easily become very difficult to read and understand (Illogical Contracts). This work considers JML as a language for specifying contracts [5]. Smells are described over JML constructs, although several can appear in other DBC languages. Along with names and symptoms, actions are suggested to eliminate or minimize the effect of these smells. It is believed that initiatives towards cataloging bad smells are useful for establishing good design practices in DBC.

The recurrence of the catalogued bad smells are evaluated in two ways: first by describing a small study with graduate student projects, and second by counting occurrences of smells in library classes from the JML models application programming interface (API). This API offers classes that support specifications in JML, many of which present rather complete specifications. The API contains classes with approximately 1,600 lines of contracts. One class was chosen for each category by sampling: out of 113 classes and interfaces, a representative subset of six files was picked. The analyses showed at least one type of bad smell in every exemplar, with a total of seven distinct smells. Despite the focus of this API being verification rather than DBC, it is assumed that they will be read and manipulated by developers, so detecting the presence of bad smells is desirable.

Discussions about related work and conclusions are included into Sections Ⅵ and Ⅶ, respectively. The contributions of this paper are summarized as follows.

A catalog of DBC code smells with JML as the target contract language (Section Ⅳ). Evaluation of bad smells in student projects, and classes from the JML models API (Section Ⅴ).

The JML is a behavioral interface specification language [4] tailored to Java. JML serves to describe contracts with static information that appears in Java declarations and how they act. JML specifications are written in the form of special annotation comments that are inserted directly into the source code of programs. These comments must begin with an at-sign (＠) and can be written in two ways: by using //＠ ... or /*＠ ... ＠*/. The following fragment shows contracts for a class Person [5].

The model modifier introduces specification-only fields, which are also called model fields. A model field should be thought of as an abstraction of a set of concrete fields used in the implementation of this type and its subtypes [6]. In the class Person, there are two model fields, name and weight, representing the concrete attributes _name and _weight via the represents clause, respectively.

The invariant clause defines predicates that are true in all visible states of the objects of a class. The invariant in the example has public visibility and establishes that the value of the attribute _name is different from an empty string, and that the value of _weight is greater than or equal to zero.

JML uses the requires clause to specify the obligations of the caller of a method regarding what must be true to call a method. For instance, the precondition of the method addKgs insists on the added value to be greater than zero. A postcondition specifies the implementor's obligation regarding what must be true at the end of a method, just before it returns to the caller. In JML, the ensures clause introduces a postcondition. In the example, it asserts that the value of the attribute _weight at the end of the method addKgs is equal to the value of the expression \old(weight + kgs). The value of an expression in the pre-state of a method can be referred to by using the \old operator.

The assignable clause gives a frame axiom for a specification. Only the locations named and their associations can be assigned during method execution. In the method addKgs, it is stated that only weight is changeable. The JML modifier purely indicates that the method does not have any side effects and can hence appear in specifications.

In this section, the importance of finding bad smells is expressed, as are the kinds of problems bad smells may bring to DBC/JML developers. As an example, consider a document editing system for LaTeX-based [7] papers. The system allows papers to be written in collaboration using a Web-based interface. The internal structure includes classes, such as Document, Section, and Author, among others. A simplified UML class diagram is shown in Fig. 1.

This diagram shows that a Document can be written by 1 main Author and can have contributions from 0 or many other Authors. The diagram also shows that a Document can have many versions. Also, a Document is composed of Sections, and each Section can have 0 or many Commands (such as links or buttons), Figures, or Tables.

Focusing the investigation on the Document class, version control is a system requirement. Versions can be defined as a list of objects in the first document object. This can be implemented as a private field in Java.

In order to specify a contract for users of this class, developers may introduce invariants over Document objects. A plausible invariant is to avoid states in which a document appears more than once in the list of versions. Following the DBC approach, the invariant is visible to other objects, so it can be specified with a JML public invariant. As long as versions is a private field, JML offers a modifier that allows the field to appear in public invariants called spec_public, as shown in the next fragment.

The contract for Document is syntactically correct and provides the desired constraint. However, careful analysis raises a number of issues with encapsulation.

As contracts are part of the public interface, clients will use them as a basis for development. In this case, clients rely on implementation details for the class, as the ArrayList field is visible. The contract relies on a private field when using the Document class. This scenario may cause classes to be harder to change, without affecting other classes.

Alternative designs can be applied to avoid encapsulation issues, with the same practical issues. The JML language allows developers to hide the internal details of a class from a contract and its clients. Model fields can be used for this purpose, representing a more abstract view of class data, as they can be freely viewed by clients. The implementation for the model field must be provided by concrete, possibly private fields. The represents clause allows for the expression of functional abstractions between a model and concrete fields. Model field types can be defined as immutable objects provided by the JML models API [8], which provides classes that emulate mathematical objects (including sets, bags, and sequences). These types are appropriate for abstract fields. In this example, the JMLEqualsSet class is used, which implements a set of values.

A concrete definition for this model field must be provided by the class developer. Here, a JMLEqualsSet object is built from the elements in the concrete _versions list. The following represents clause illustrates this approach, with a model method. Model methods provide a useful abstraction for procedures and functions that will only be used within JML contracts. In this case, the method copies every element from the concrete list to the Fig. 1. Online document editing system. mathematical set, so the model field can be evaluated.

In this particular scenario, the method may be overkill, with a very operational way of filling the mathematical set. It would be hard to write and maintain such code for numerous methods. This clause can be refactored to a better solution by using methods from the JML models API itself (the getVersions method).

Regarding method contracts, in the class Section, the beginEdition method locks the section for editing by request by a given author. The preconditions state that the section is unlocked, and the requesting author is included as an author for the given document (which cannot be null). As a postcondition, the contract guarantees that the section is locked after the call.

The repetitive use of fields in the specification can be observed, even though the correct behavior is provided. As creating a model field for each concrete field clutters the class, an alternative can be found for better encapsulating internal details. A good option is using a public getter method (and if one does not exist, it could be created).

In this example, several correct contract parts can be considerably improved for DBC contexts. These “bad smells” are catalogued in this work, so that efforts towards effective DBC development can take advantage of tool support for detecting these smells, and refactorings can then be more effectively employed.

In this section, a catalog of bad smells in contracts that result from DBC development is provided. As shown in the example, smells are not necessarily hazardous, but they show evidence of possible errors and hard-to-change programs. For a more concise and uniform explanation of bad smells and for ease of identification, a specific format for smell descriptions was adopted. The format used for the catalog was inspired by code smells from Wake's book on refactoring [9]. Smells are described with the following properties.

Brief Description: Description emphasizing the problems behind the smell. Symptoms: Clear signs of the described bad smells in contracts and code. Example: Example of the bad smell, using the system described in Section Ⅲ. Causes: Likely ways of having this smell present in the program. What to do: Ideas on how to refactor the program for eliminating or minimizing the impact of the smell (although this is not the focus in this paper). Example Solution: A possible refactored program. Payoff: Advantages in avoiding these smells in terms of general quality of DBC development. Contraindications: Situation in which removing the smell may not be desirable.

Focused was centered on JML as a contract language, so smells are in principle specific to particular JML constructs. Still, they are likely to appear in similar constructs in other contract languages (JML, Eiffel, Spec# [10], among others). Six smells are described in detail: Open Doors Field Obsession, Illogical Contracts, Complexity Magnetism, Long Specs, and Specification Overkill. The set of DBC smells catalogued so far are presented in Table 1.

1) Brief Description

Contracts that expose private data, threatening encapsulation.

2) Symptoms

Indication is given with direct access to private or protected fields (or methods) in public contracts. In JML, it is made explicit with the spec_public or spec_protected modifiers. The forall operator represents a universal quantifier, with three components separated by semicolons: variable declaration, variable delimitation, and Boolean expression with the predicate.

3) Example

4) Causes

Developers need a way to specify which components of internal data must be modified in method contracts or invariants that have visibility that is less restricted than data. Also, this can be caused by a lack of abstraction when specifying methods.

5) What To Do

In cases where fields must be used to indicate state changes and contracts, a model field can be created, representing a hidden concrete field. The contracts must then be changed to use the model field, replacing accesses to the concrete field. However, if many fields are used in contracts, developers should consider using query methods instead (see Section Ⅳ-B). Regarding methods, model methods can be used, in which code delegates the call to concrete methods.

6) Solution to the Example

7) Payoff

Encapsulation is promoted, even in the presence of contracts. Removing this smell tends to bring abstraction to contracts, which is highly desirable in DBC.

8) Contraindications

Excess model fields tend to increase the complexity of contracts. In this case, query methods should be a better option. In some fields, however, query methods might not be usable due to some encapsulation requirement in the application. In this case, the contracts should be revised, as they could possibly not expose these particular fields.

1) Brief Description

There are an excessive number of direct field accesses in contracts, making these contracts more sensitive to changes in internal data.

2) Symptoms

Excess direct access to several fields from a class in contracts.

3) Example

For the setSections method, the contract includes precondition and postcondition and includes the JML assignable clause, which indicate frame conditions (variables that may possibly be assigned values). The invariant refers to fields and sections.

4) Causes

In general, this smell happens when developers avoid using methods, perhaps fearing long specifications. This can also happen regardless of concrete or model fields.

5) What To Do

Mainly, solutions must include the use of query (accessor) methods. In Eiffel, for instance, field accesses automatically behave as query methods. JML does not offer this feature, since it would demand changes in the semantics of the programming language (Java).

6) Solution to the Example

7) Payoff

Besides adding abstraction to contracts, this solution usually makes the contract easier to understand.

8) Contraindications

The contract can get considerably long if too many fields are accessed. In this scenario, contracts can be rewritten with improvements by using auxiliary model methods (see Section Ⅳ-C).

1) Brief Description

Contracts defining predicates with logics that become too hard to understand.

2) Symptoms

The bad smell Illogical Contracts is identified by long specifications where a chain of Boolean predicates is presented. Long and chained Boolean predicates are hard to read and understand, especially when universal quantifications are used.

3) Example

In the Document class, there may be an invariant stating that the sections for older versions of a document must be present in the later versions. In JML, this must be written as two universal quantifications.

4) Causes

Some complex specifications may be required. This might be more common in JML, as it follows Java syntax with extensions, which makes Boolean predicates verbose. Abstraction in this scenario is a challenge.

5) What To Do

Declaration of JML-pure Boolean methods that represent predicates. In JML, pure methods are required to have no side effects. The methods are used in contracts as auxiliary predicates. In this context, naming is important for improving readability.

6) Solution to the Example

In JML, auxiliary predicates can be declared as model methods.

7) Payoff

The solution helps raising abstraction in contracts, making them easier to read and edit.

8) Contraindications

In some situations, it may be necessary to create too many methods, which can make the specification longer than the original. Therefore, it is sensible to revise the contracts in order to find better ways to rewrite complex statements (which is not always possible). In addition, if predicates become substantially complex due to the application domain, separation and comments in natural language can be used, especially if the contracts will not be subject to tool-assisted verification. For instance, JML allows for predicates in natural language, although they are not considered for reasoning.

1) Brief Description

Model fields with complex definitions in represents clauses.

2) Symptoms

When using abstract model fields, the represents clause may become very complex. This scenario hinders readability and maintainability, especially for class implementers (clients should not have access to represents).

3) Example

In this case, the versionsSet model field has a complex definition, which is encapsulated in a model method. This method copies each element of the concrete ArrayList to the abstract set.

4) Causes

This situation arises depending on how hard it is to abstract from concrete data. Also, the complexity of specific data structures is critical (for example, collection manipulation from Java).

5) What To Do

For simple collections, the JML model API offers methods like convertFrom. The mathematical toolkit of the language should support this solution. In cases that result in complex model methods that abstract away details from internal data, other auxiliary methods can be extracted (analogous to the Extract Method refactoring [1]).

6) Solution to the Example

7) Payoff

Contracts become easier to write and understand by implementers. Abstraction in general is higher. Despite this example, a variation of this smell can happen in the opposite situation: a one-line definition of represents can become too complex. In this case, the model method should be included.

1) Brief Description

Unnecessary heavyweight style in DBC applications, covering every possible behavior for methods.

2) Symptoms

In JML, developers may use two styles of contracts (specification cases): heavyweight or lightweight. For the first style, in contrast to the latter, JML expects that developers only omit parts of the specification when the default is appropriate, specifying behavior completely. This is indicated by the clauses normal_behavior and exceptional_behavior. An excess of heavyweight contracts obstructs good DBC development, decreasing abstraction and readability.

3) Example

In the contract, the also keyword indicates the complementarity of specification cases. The signals_only and signals constructs define the Java exceptions possibly thrown by the method in exceptional behavior.

4) Causes

Sometimes, it is required that specifications be replicated, with the intention of specifying complex contracts. Also, developers may wish to document every situation in which exceptions are thrown.

5) What To Do

In DBC, lightweight contracts are much more desirable, as both clients and implementers should often refer to contracts as documentation. In this scenario, exceptional behaviors should be removed, omitting exceptional situations that are not relevant for implementing the program. Also, the normal_behavior clause can be removed.

6) Solution to the Example

More importantly, better readability and maintainability of contracts. In avoiding heavyweight specifications in DBC, another benefit arises in that developers eliminate the risk of introducing specification mistakes by accidently defining overlapping specification cases (superposition of preconditions that do not make clear which one is valid for a given state).

8) Contraindications

When JML is applied in complete tool-assisted verification or test-case generation, covering all specification cases is critical. In this scenario, this is certainly not considered a bad smell.

1) Brief Description

Excess of redundant specifications.

2) Symptoms

Repeated use of redundant clauses, such as ensures_ redundantly or requires_redundantly, which means that the contract was already valid in the given context, usually for documentation purposes. Even different predicates with the same semantic are allowed.

3) Example

4) Causes

This bad smell may appear to be caused by needs for repeating specifications with the intention of explaining something complex. But, in other contexts, this can expose a lack of attention to the existing predicates.

5) What To Do

Mostly, redundant clauses can be removed, because the redundancy might show the existence of an unnecessary specification. In some cases, a good revision of predicates is enough. Also, it is better to use the simplest forms of the specifications, because if it is possible to reexplain something more simply, it is always best to use this simpler explanation in a single turn.

6) Solution to the Example

7)Payoff

The specification becomes clearer and more easily understood. Inconsistencies are avoided as redundancy is removed.

8) Contraindications

In a number of situations, the use of ensures_ redundantly is justified as a good way to explain complex contracts. In these cases, it is important to look for ways to leave contracts in the simplest form possible. There is still an alternative of removing Smell Section Ⅳ-C.