Design-by-Contract (DBC)  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 (
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 (
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  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
The model modifier introduces specification-only fields, which are also called
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  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.
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
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 . 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# , among others). Six smells are described in detail:
Contracts that expose private data, threatening encapsulation.
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.
Catalog of Design-by-Contract smells
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.
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.
Encapsulation is promoted, even in the presence of contracts. Removing this smell tends to bring abstraction to contracts, which is highly desirable in DBC.
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.
There are an excessive number of direct field accesses in contracts, making these contracts more sensitive to changes in internal data.
Excess direct access to several fields from a class in contracts.
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.
In general, this smell happens when developers avoid using methods, perhaps fearing long specifications. This can also happen regardless of concrete or model fields.
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).
Besides adding abstraction to contracts, this solution usually makes the contract easier to understand.
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).
Contracts defining predicates with logics that become too hard to understand.
The bad smell
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.
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.
Declaration of JML-pure Boolean methods that represent predicates. In JML,
In JML, auxiliary predicates can be declared as model methods.
The solution helps raising abstraction in contracts, making them easier to read and edit.
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.
Model fields with complex definitions in represents clauses.
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).
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.
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).
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 ).
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.
Unnecessary heavyweight style in DBC applications, covering every possible behavior for methods.
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.
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.
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.
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.
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).
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.
Excess of redundant specifications.
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.
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.
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.
The specification becomes clearer and more easily understood. Inconsistencies are avoided as redundancy is removed.
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.