Chapter 5. Self-conscious code: Reliability through monitoring

This chapter covers

• Writing method specifications in contract form
• Enforcing contracts at runtime
• Using assertions
• Checking class invariants as a lightweight alternative to postconditions

Software reliability refers to the extent to which the system performs as expected, in a variety of operating conditions. In this chapter, we’ll explore the main coding techniques you can use to prevent or expose unexpected program behaviors. But first, let’s discuss how you can define the expected behavior of a piece of software, aka its specification. In line with the structure of this book, I’ll focus on the behavior of a single class, such as Container. A popular way to organize specifications of OO programs and classes therein is through the design-by-contract methodology.

5.1. Design by contract

In ordinary language, a contract is an agreement in which each party accepts obligations in exchange for some benefits. In fact, what’s an obligation for one party is the benefit of another. For example, a phone plan is a contract between a carrier and the phone owner. The carrier is obliged to render the phone service, and the owner is obliged to pay for it, so each party benefits from the other party’s obligations.

The design-by-contract methodology suggests attaching contracts to software artifacts, particularly individual methods. A method contract comprises a precondition, a postcondition, and possibly a penalty.

5.1.1. Pre- and postconditions

The precondition states the requirements for the method to correctly function. It talks about the legal values for the parameters and about the current state of this object (for an instance method). For example, the precondition of a square-root method might state that its argument should be non-negative.

It’s the caller’s responsibility to respect the precondition of the method being called. In the analogy with an ordinary contract, the precondition is an obligation for the caller and a benefit for the callee. The method itself can either passively assume that the precondition holds or actively check whether it holds, and react accordingly.

The precondition should include only properties that are under the full control of the caller. For example, a method that takes a file name as an argument and opens that file can’t list among its preconditions that the file exists, because the caller can’t be 100% sure that it does. (Another process can erase that file at any time.) The method can still throw an exception in that case, but that exception will be of the checked variety, forcing the caller to handle it.

Conversely, the postcondition states the effect of the method and describes its return value and all the changes performed on the state of any object. In most well-designed classes, changes should be limited to the current object, but this isn’t always the case. For example, the connectTo method in our running example must modify multiple containers to achieve its intended effect.

The postcondition also should specify what happens when the caller violates a precondition: this is referred to as a penalty. In Java, the typical penalty consists of throwing an unchecked exception. Figure 5.1 is a graphical depiction of the contract for an instance method.

Figure 5.1. The high-level structure of a contract for an instance method. All consequences of a method besides its return value are called side effects.

Pop Quiz 1

What’s wrong with throwing a checked exception as a penalty?

For example, here’s the contract for the next method of the java.util.Iterator interface:

1. Precondition— This iterator hasn’t reached the end. Equivalently, a call to has Next would return true.
2. Postcondition— It returns the next item in the iteration and advances the iterator by one position.
3. Penalty— If the precondition is violated, the method throws NoSuchElement Exception (an unchecked exception).

Calling next when the iterator has already reached the end violates the precondition and is an error on the side of the client. (The error is outside the next method.) Conversely, an implementation of next that doesn’t advance the iterator to the next item is violating the postcondition. In this case, the error lies inside the method itself.

Figure 5.2 depicts the detailed data dependencies involving various parts of the contract. The precondition dictates the legal values for the arguments and for the state of this object before the call. That’s why two arrows are coming into the “precondition” box. For example, the precondition of Iterator::next mentions only the state of the iterator because that method takes no arguments.

Figure 5.2. Detailed structure of a contract for an instance method. Solid arrows represent data dependencies pertaining to the contract (what the contract talks about). Dashed arrows are standard runtime interactions that occur regardless of the contract (what actually happens at runtime).

Because the postcondition describes all the changes that the method brings about, it may refer to the following data:

• The return value (as the main effect of the method)
• Both the old and new state of this object: the old state as an input that can influence the behavior of the method, and the new state as another effect of the method
• The value of the arguments, as inputs
• Other side effects that globally available objects or static methods produce, such as a call to System.out.println

Figure 5.2 omits the last case and depicts the others as incoming arrows into the “post-condition” box. For example, the postcondition of Iterator::next refers explicitly to the return value, and implicitly to both the old and new state of the iterator, when it says that “it returns the next item and advances the iterator by one position.”

5.1.2. Invariants

Besides method contracts, classes can have associated invariants. An invariant is a condition, regarding the class fields, that’s always true, except while an object is undergoing change due to a method of the class.

Invariants are static consistency rules: they refer to the state of the objects at a single instant in time. On the other hand, postconditions are dynamic consistency rules because they compare the state of the object(s) before and after a method call.

As the name implies, invariants must hold both before and after a method is called. Accordingly, in figure 5.2, invariants have incoming arrows from the old and new state of the object.

The initial state of each object, which a constructor establishes, must satisfy the invariants, and all public methods are responsible for preserving their validity. Private methods don’t have this obligation because their role is to support public methods. As a result, when a private instance method runs, it’s typically within the context of some ongoing public instance method that invoked it, either directly or indirectly. Because the current object may be undergoing change, the private method may find it in an intermediate state that violates an invariant, and may also leave it in an inconsistent state. It’s only at the end of the public method that the state of the object must be consistent again, and invariants must be restored.

5.1.3. Correctness and robustness

You can refine software reliability into two qualities: correctness and robustness. The difference between them lies in the type of environment you assume for your system. When evaluating correctness, you imagine your system in a nominal environment, that is, an environment satisfying the system expectations. In such a friendly context, method preconditions are honored, external inputs arrive in a timely manner and in the right format, and all resources that the system needs are available. If the system is correct, it will behave according to plan in all friendly environments.

In principle, correctness is a Boolean property: either it holds or it doesn’t. Partial correctness doesn’t make a lot of sense. However, it’s usually impractical to devise perfectly formal and complete specifications, and as soon as specifications become blurry, so does correctness. In the little controlled world of the container example, we’ll put forward clear specifications and make sure the class is correct with respect to them. Then, we’ll explore techniques that maximize our confidence in its correctness. Those techniques will be useful in real-world scenarios when you don’t have months to spend over a single class, as I had when writing this book.

On the other hand, robustness refers to system behavior under exceptional or unanticipated environments. Typical cases include the host machine running out of memory or disk space, external inputs being in the wrong format or outside the legal range, methods being called in breach of their preconditions, and so on. A robust system is expected to react gracefully in such situations, where the appropriate definition of grace is highly dependent on the context.

For example, if a crucial resource is unavailable, the program might try to wait a little and request it again, a couple of times, before giving up and terminating. If the problem persists, and, more generally, whenever termination is the only way out, the program should clearly inform the user about the nature of the problem. In addition, it should strive to minimize data loss so the user can later resume their task as smoothly as possible.

Pop Quiz 2

If a program prints some output on paper, what’s a graceful reaction to the printer being out of paper?

Figure 5.3 summarizes the relationships between the two software qualities that constitute reliability, the various types of specifications I discussed earlier, and the three coding techniques you’ll use in this chapter and the next.

Figure 5.3. Relationship between reliability attributes, contract-based specifications, and coding techniques

Correctness is defined with respect to a contract, comprising pre- and postconditions, and optionally to a set of class invariants. The penalty is not directly related to correctness because it only springs into action when the caller violates a precondition. As such, it’s a robustness issue.

Three coding techniques help implement and enforce contracts:

• Plain if-based checks make sure the caller is invoking a method in the proper way, obeying its preconditions, and issue a corresponding penalty otherwise.
• Java assert statements are useful to keep postconditions and invariants in check, particularly in safety-critical software.
• Finally, tests increase your confidence in the reliability of your software, mostly by checking postconditions and triggering penalties.

In this chapter and the next, I’ll delve into the best practices regarding each of these techniques. For the moment, notice that the first two are monitoring techniques, active during regular operation of your software. Testing instead is performed before operation and separately from it.

5.1.4. Checking contracts

Many programming errors have to do with violating method preconditions. To expose these problems as early as possible, methods should check their preconditions at runtime and throw a suitable exception if they’re not met. This is sometimes called defensive programming. Two standard exception classes are commonly used for this purpose:

• IllegalArgumentException—The value of an argument violates the precondition.
• IllegalStateException—The current state of this object is incompatible with the instance method being called or with the value of the arguments. For example, attempting to read from a file that already has been closed might throw this exception.

Assertions represent a related but more specific checking mechanism. An assertion is a statement of the following form:

assert condition : "Error message!";

When executed, the line evaluates the Boolean condition and throws an Assertion Error if the condition is false. The error message string is passed into the exception being thrown and will be printed out if the exception isn’t caught. In other words, the assertion is quite similar to the following statement:

  if (!condition) {
     throw new AssertionError("Error message!");
  }

At this point, an assertion looks like a shorter version (aka syntactic sugar) of a regular if-based check. However, one crucial feature distinguishes the two: by default, the JVM does not execute assertions. You have to explicitly activate them with the “-ea”command-line option or via the corresponding IDE setting. When you have assertions turned off, the program doesn’t incur the performance overhead due to evaluating the corresponding Boolean conditions.

A standard if-based check is always executed, but if an assertion performs that check instead, you’ll be able to turn it on or off at each execution. The usual practice is to turn on assertions during development and then revert to the default “off” state for production. It seems that assertions win all the way: they’re more succinct, and you have more control over them. Should you use them for all runtime error checking? It turns out that in some cases the flexibility that comes with assertions becomes a liability. In those cases, you want some checks to stay in place at all times, even during production.

Design by contract provides simple guidelines for identifying which checks should always be on:

• Precondition checks on public methods should always be on, so you should use regular if-based checks for them.
• All other checks should be on only during development. These include postcondition and invariant checks, and precondition checks on nonpublic methods. Use assertions there.

The rationale is the following. Precondition violations are due to the caller not respecting the method contract. On the other hand, a postcondition or invariant violation is due to an issue within the class itself. Consider the following key assumption:

Development and testing ensure that each single class is free from internal issues.

By an internal issue, I mean a bug that manifests itself even if the class clients respect all the rules that the contracts put forward. For the moment, take this assumption at face value; I’ll discuss its plausibility in a second. If the previous assumption holds, the only way the program can misbehave is by a class misusing another class. In a properly encapsulated system, this can happen only via public methods. Hence, to expose these bugs, precondition checks on public methods are sufficient, and you should leave them on. Notice that checking preconditions at runtime doesn’t fix the problem, it merely exposes it as early as possible during the execution so you can more accurately characterize the root cause.

How reasonable is the no-internal-issue assumption? That ultimately depends on the quality and intensity of the development process. The higher the quality and intensity, the more likely the assumption is to hold. By quality of the development process, I mean whether the developers follow the industry’s best practices. Intensity (or effort) refers to the number of people and amount of time used to develop, and especially test, each class. For example, you can only expect small classes to be entirely free from internal issues. For good reason, writing small classes is one of the sacred best practices in OOP.

5.1.5. The broader picture

Figure 5.4 puts the techniques presented in this chapter and the next into a wider perspective. This book focuses on programming styles and techniques that even a single programmer can employ in their daily activities. Beyond that, at least two more types of intervention can contribute to software quality in general, and to reliability in particular.

Figure 5.4. A broad view on quality-enhancing techniques.

First, there’s human oversight: having a fellow developer look at your code and evaluate it according to company standards. You can arrange this in periodic reviews or sometimes as a continuous interaction between two colleagues, a practice known as pair programming.

Then, some software tools can automatically check a variety of code properties, enriching the scrutiny that the compiler already performs. You can divide such tools roughly into three categories, from the most basic to the most advanced:

• Style checkers— These tools only perform relatively superficial checks targeting readability and uniformity (discussed in chapter 7). In turn, those qualities also indirectly benefit reliability and maintainability. Example feature: Check that the indentation is correct and uniform (same number of extra spaces for each nesting level) Example tool: CheckStyle^[1]

  ¹

  As of this writing, available at https://checkstyle.sourceforge.io.

• Static analyzers— These tools are capable of performing a semantic analysis similar to the compiler’s type-checking phase. Style checkers and static analyzers are also known as linters. Example feature: Checks whether an anonymous class contains an uncallable method (a method that doesn’t override another method and that other methods of that class don’t use) Example tools: SpotBugs,^[2] SonarQube^[3]

  ²

  As of this writing, available at https://spotbugs.github.io.

  ³

  As of this writing, available at www.sonarqube.org.

• Formal verifiers— These tools, mostly born out of academic research, understand a program at a deeper level than the typical compiler. That is, they can simulate the execution of the program on entire sets of values, a process known as symbolic execution. Example feature: Check whether an integer variable can ever become negative^[4]

  ⁴

  Technically, this property is undecidable. A formal verifier will attempt to prove or disprove it, but it’s not guaranteed to succeed.

  Example tool: KeY^[5]

  ⁵

  As of this writing, available at www.key-project.org.

It’s usually up to your organization to choose the set of quality practices and tools it deems appropriate to the task at hand. What’s suitable for developing a videogame is vastly different from what a military or healthcare client demands. Now, let’s go back to our usual perspective, focused on how to improve the reliability of a single unit of code, even before your fellow programmers or tools of choice have a chance to look at it.

5.2. Designing containers by contract

You’re ready to apply the design-by-contract guidelines to water containers and their Reference implementation. But first, let’s figure out the contracts for the container methods, summarized in table 5.1. I didn’t include the constructor in the table because its contract simply states that it creates an empty container.

Table 5.1. Contracts for the methods of Container

As you can see from table 5.1, the contracts are just a structured way to present the expected behavior of a method, explicitly distinguishing the assumptions from the guarantees. Compared to the method descriptions I provided in chapter 1, these contracts add the description of the preconditions and the corresponding penalties:

• connectTo requires its argument to be non-null and is expected to throw Null PointerException (NPE) otherwise
• addWater, when used with a negative argument, say – x, requires the total amount of water in the containers connected to this one to be at least x, or else it will throw IllegalArgumentException (IAE).

Those are two standard classes of exceptions, both of which are unchecked and subclasses of RuntimeException.

The precondition requiring an argument to be non-null is extremely common, as is the confusion about which type of exception is the most appropriate in this case. The sidebar sheds some light on the issue.

  public static Object requireNonNull(Object x)
  public static Object requireNonNull(Object x, String message)

Next, consider class invariants. Ideally, invariants should exactly describe what object states are consistent with the contracts. In more detail, they should tell us which values for the fields we can obtain after a series of legal operations. For Reference, this leads to the following invariants:

Consider how these invariants relate to the contracts in table 5.1. Invariant I1 is intuitively obvious: a container can’t include a negative amount of water. The precondition of addWater is in charge of defending this invariant against external attacks, that is, attempts to decrease water levels below zero. Invariants I2 and I3 are a consequence of our policy regarding groups of containers: they all start with a single container, then they’re merged pairwise. The constructor establishes these invariants, and the connectTo method must preserve them by correctly merging groups. Finally, invariant I4 states the relationship between groups and amounts. It’s the responsibility of addWater and connectTo to maintain it, as expressed by their postconditions.

It’s an interesting exercise to verify that the four invariants, I1–I4, are complete, in the sense that you can build any pool of containers satisfying them from scratch by a legal sequence of constructor and method calls. Moreover, removing any one of the four invariants voids this property.^[6]

⁶

For example, if you remove invariant I1, you admit an isolated container holding a negative amount of water. You can’t obtain that scenario with a legal sequence of constructor and method calls.

Pop Quiz 3

Is this a valid invariant for the Container class: “Passing zero to addWater leaves all containers unchanged”?

Now that we’ve clearly laid out the contracts and invariants, you can use them to harden Reference for correctness and robustness. The path for preconditions and postconditions is pretty clear: we’ll check them at the beginning and end of their method, using if-based checks or assertions, according to the guidelines I presented earlier. Regarding invariants, we need to address the issue of when to check them, that is, how often and at which program points. Recall that invariants are supposed to hold at the beginning and end of each (public) method. At one extreme, we might check all invariants at all of those moments. At the other extreme, we might skip all invariant checking because properly checking pre- and postcondition automatically ensures that invariants hold. The weakness of the latter approach lays in the word properly. Indeed, in the following section, we’ll implement a version of Container where each method carefully checks its pre- and postconditions, and you’ll witness how tricky and expensive it is to perform these checks thoroughly. Then, in section 5.4, we’ll replace postconditions with invariants, which are generally easier to check.

All versions of Container in this chapter are based on the same fields as Reference, repeated here for convenience:

public class Container {
   private Set<Container> group;  1 Containers connected to this one
   private double amount;         2 Amount of water in this container

5.3. Containers that check their contracts    [Contracts]

In this section, we’ll develop a version of Container whose methods check both their precondition and their postcondition at each invocation.

5.3.1. Checking the contract of addWater

Let’s start with the addWater method. You’ve already seen its contract in table 5.1, but I’ll repeat it here for convenience:

• Precondition— If the argument is negative, there’s enough water in the group.
• Postcondition— Distributes water equally to all containers in the group.
• Penalty— Throws an IllegalArgumentException.

The method has a simple precondition that you can check using a standard if statement, according to the guidelines I discussed earlier.

You should check the postcondition using assertions so that you can easily turn those checks off in production. So far, I’ve expressed the postcondition of addWater in rather vague terms. What does it mean to equally distribute the added water? Clearly, at the end of the method, all containers in the group must have the same amount of water. However, that’s not the end of the story. The total amount in the whole group should be equal to the old total amount, plus the newly added water. To check this property, you have to store some information at the beginning of the method. Then you use it at the end to compare the way the object state was supposed to change with the way it actually changed.

This situation suggests structuring the method into the following four steps:

1. Check the precondition with a plain if.
2. Store the current group amount in some temporary variable so you can check the postcondition later.
3. Perform the actual water-adding operation.
4. Check the postcondition using the data you stored in step 2.

Moreover, keep in mind the following design objective: when assertions are turned off, you want all the time and space overhead of checking postconditions to go away. Consistent with that objective, you should only perform steps 2 and 4 when assertions are enabled. That’s easy for step 4: just invoke postAddWater as the condition of an assertion. Step 2 is trickier because it’s not naturally expressed as an assertion. To turn it into an assertion, you can wrap the assignment into a dummy comparison (see listing 5.1) that’s always true. In this case, you can assert that the old group amount is positive. With this trick, the only residual overhead, even when assertions are disabled, is the allocation of the oldTotal variable on the stack.^[7]

⁷

If you don’t like the dummy assert trick, an alternative is to set a flag to true if assertions are enabled (how? see pop quiz 4), and use regular ifs to skip certain operations when assertions are disabled.

Pop Quiz 4

How do you set a Boolean flag to true only if assertions are enabled?

The following listing shows a possible implementation that delegates steps 2 and 4 to two novel support methods.

Listing 5.1. Contracts: Method addWater

   public void addWater(double amount) {
      double amountPerContainer = amount / group.size();
      if (this.amount + amountPerContainer < 0) {  1 Checks the precondition
         throw new IllegalArgumentException(
                   "Not enough water to match the addWater request.");
      }
      double oldTotal = 0;  2.0 Saves the postcondition data
      assert (oldTotal = groupAmount()) >= 0;  2.1 Dummy assert

      for (Container c: group) {  3 The actual update
         c.amount += amountPerContainer;
      }
      assert postAddWater(oldTotal, amount) :  4 Checks the postcondition
                   "addWater failed its postcondition!";
   }

The implementation of addWater in listing 5.1 delegates two tasks to new support methods: groupAmount computes the total amount of water in a group of containers; postAddWater is responsible for checking the postcondition of addWater. The code for groupAmount is trivial, simply adding up the values of all amount fields in the current group, as shown in the following listing.

Listing 5.2. Contracts: Support method groupAmount

   private double groupAmount() {  1 Returns the total amount in the group
      double total = 0;
      for (Container c: group) { total += c.amount; }
      return total;
   }

The method postAddWater, in turn, splits its task into two parts: first it checks that all containers in the current group hold the same amount of water; then it verifies that the total amount in the group is equal to the old amount plus the newly added amount. (The following version of postAddWater is tentative—a better version follows.)

Listing 5.3. Contracts: Tentative version of support method postAddWater

   private boolean postAddWater(double oldTotal, double addedAmount) {
      return isGroupBalanced() &&
             groupAmount() == oldTotal + addedAmount;  1 Exact comparison
                                                         of doubles
   }

   private boolean isGroupBalanced() {  2 Checks that all the group
      for (Container x: group) {          shares the same amount
         if (x.amount != amount) return false;
      }
      return true;
   }

As you can see, checking the postcondition requires more lines of code than the original nonhardened method! The sheer number of lines may lead you to surmise that you’re more likely to make a mistake in coding the postcondition check than in writing the original method. Is there a point to this effort? If the check ends up simply repeating the same calculations that the method performed, the effort is clearly pointless. However, if you can find a different, and hopefully simpler, way to check that the outcome is correct, then the two different algorithms are checking each other. Even a mistake in the postcondition routine is an opportunity to refine your understanding of the class at hand.

Now you run this version of addWater on a simple example, with assertions on, and. . . it breaks! The VM reports failure in the postcondition of addWater. Here’s the code fragment that generates the assertion failure—can you spot the problem?

Container a = new Container(), b = new Container(), c = new Container();
a.connectTo(b);
b.connectTo(c);
a.addWater(0.9);

The problem lies with the comparison between two double values in postAddWater (listing 5.3). If you don’t use floating-point numbers on a regular basis, it’s easy to forget that they don’t behave like ideal real numbers. As a result, sometimes (a/b) * b comes out different from a.

For example, the number 0.9 is not exactly representable in base 2. Its binary expansion is periodic, so it will be stored in an approximate way. When you divide it by 3 and add it to the three containers, more approximations are performed. In the end, when you sum back the amounts from each container in the group, the total comes out slightly different than expected. Summarizing, you’re computing the amount of water in the group in two different ways, and then comparing them using ==. Because of approximations, the two sides won’t be exactly equal. Detailed calculations are beyond the scope of this book but within the reach of the resources listed in the Further reading section at the end of this chapter. Suffice it to say, in the current situation you get the following values after the call to addWater:

This suggests that you should almost always do floating-point comparisons with some tolerance for error. How much tolerance depends on the range of numbers you expect to handle. In this case, say the unit for liquids is liters (gallons would work just fine), and our containers will handle tens or hundreds of liters. In this scenario, it’s safe to assume you’re not interested in single drops of water, so it’s reasonable to employ a tolerance of, say, 0.0001 = 10^–4 liters—roughly equal to the amount of water in a drop. You end up with the following improved version of postAddWater.

Listing 5.4. Contracts: support methods postAddWater and almostEqual

   private boolean postAddWater(double oldTotal, double addedAmount) {
      return isGroupBalanced() &&
            almostEqual(groupAmount(), oldTotal + addedAmount);
   }

   private static boolean almostEqual(double x, double y) {
      final double EPSILON = 1E-4;  1 Tolerance for rounding errors
      return Math.abs(x-y) < EPSILON;
   }

Pop Quiz 5

What happens if you pass “not-a-number” (Double.NAN) to addWater?

5.3.2. Checking the contract of connectTo

Next, let’s examine the connectTo method and its contract:

• Precondition— Argument is not null
• Postcondition— Merges the two groups of containers and redistributes water
• Penalty— Throws NullPointerException

This kind of precondition is so common that the JDK provides a standard way to handle it with the Objects.requireNonNull(arg,msg) static method. As I explained earlier, that method throws an NPE with a custom message if arg is null, otherwise returning arg itself.

Properly checking the postcondition, in contrast, poses significant challenges. Start by translating the postcondition into a list of practical checks to be performed on the instance fields. Call G the set of containers that this.group points to at the end of connectTo(other). The postcondition requires that the following properties hold:

1. G is not null, and its elements are all the containers that belonged to the two old groups of this and other.
2. All containers in G must point back to G via their group reference.
3. All containers in G must have the same amount value, equal to the total amount in the two old groups divided by the number of containers in G.

To check property 1, you need to store the old groups of this and other before the merge, that is, at the beginning of connectTo. The method could modify those groups, so you need to store a copy of those sets. Property 2 doesn’t need any information beforehand; to verify it, it’s sufficient to iterate over all containers in G and check that their group field points back to G. Finally, checking property 3 requires you to know the value of the amount fields before the merge, or at least the sum of those values over all containers connected to this or other. Summarizing, you need to store the following information, as it stands before the merge:

• A copy of the groups of this and other
• The total amounts of water in those groups

Introduce a nested class ConnectPostData to keep this information together, as shown in the following listing.

Listing 5.5. Contracts: Nested class ConnectPostData

   private static class ConnectPostData {  1 Stores data needed to check
      Set<Container> group1, group2;         the postcondition
      double amount1, amount2;
   }

You can now draft the code for connectTo, following the same four-step structure as addWater. As before, you should try to keep the overhead to a minimum when you have assertions disabled. In listing 5.6, the only overhead that sticks even when you have assertions disabled is the allocation of the postData local variable (in the fifth line). You achieve this effect by embedding the call to saveConnectPostData into a dummy assert statement that always succeeds (in the sixth line).

The code that actually makes the connection is the same as for Reference, so I’ve omitted it from the following listing for readability.

Listing 5.6. Contracts: Method connectTo (abridged)

   public void connectTo(Container other) {
      Objects.requireNonNull(other,        1 Checks the precondition
              "Cannot connect to a null container.");
      if (group==other.group) return;

      ConnectPostData postData = null;  2 Prepares the postcondition data
      assert (postData = saveConnectPostData(other)) != null;  3 Dummy assert

      ...  4 The actual operation goes here (same as Reference)

      assert postConnect(postData) :  5 Checks the postcondition
             "connectTo failed its postcondition!";
   }

Methods saveConnectPostData and postConnect, respectively, store the needed information and use that information to check whether the postcondition holds. They are shown in the following listing.

Listing 5.7. Contracts: Methods saveConnectPostData and postConnect

   private ConnectPostData saveConnectPostData(Container other) {
      ConnectPostData data = new ConnectPostData();
      data.group1 = new HashSet<>(group);  1 Shallow copy
      data.group2 = new HashSet<>(other.group);
      data.amount1 = amount;
      data.amount2 = other.amount;
      return data;
   }
   private boolean postConnect(ConnectPostData postData) {
      return areGroupMembersCorrect(postData)
          && isGroupAmountCorrect(postData)
          && isGroupBalanced()
          && isGroupConsistent();
   }

In the name of readability, the postConnect method delegates its task to four different methods, whose roles I’ve summarized in table 5.2.

You’ve already seen the code for isGroupBalanced earlier (listing 5.3). Let’s have a quick look at the code to check whether the old groups were properly merged (listing 5.8). It first checks that the new group contains all the members from the two old groups (second and third lines). To make sure that the new group doesn’t contain any extra members,^[8] it checks that the size of the new group is equal to the sum of the sizes of the two old groups (fourth line).

⁸

It may be argued that the size check is redundant. Indeed, if all containers respect the invariants before the call to connectTo, there’s no way for connectTo to reach any other container that’s not in one of the two groups being merged. Even a faulty implementation can produce a smaller new group but not a larger one.

Table 5.2. The four methods used to check the postcondition of connectTo

Listing 5.8. Contracts: Support method areGroupMembersCorrect

   private boolean areGroupMembersCorrect(ConnectPostData postData) {
      return group.containsAll(postData.group1)
          && group.containsAll(postData.group2)
          && group.size() == postData.group1.size() +
                             postData.group2.size();
   }

5.4. Containers that check their invariants    [Invariants]

The previous section shows how complicated it may be to properly check postconditions. A handy alternative is to periodically verify invariants instead. Recall the invariants I established for Reference earlier in this chapter:

If the class is correct and its clients use it in the right way (that is, while respecting the preconditions of all methods), all postconditions and invariants will hold. A programming error in a method may trigger a postcondition violation. In turn, a postcondition violation may cause an invariant to fail. Assuming that preconditions are respected, a postcondition violation precedes and causes any invariant violation. On the other hand, a postcondition violation doesn’t necessarily show up as an invariant violation.

For example, assume that addWater contained the following error: when asked to add x liters of water, it adds only liters instead. Because the method leaves all objects in a legal state, this implementation would pass all invariant checks. That’s because invariants are static consistency rules that only look at the current state of the object(s). On the other hand, it would miserably fail the postcondition verification that Contracts performs.

To summarize, checking postconditions, as we did in the previous section, is generally safer but more expensive. Conversely, checking invariants is easier but also somewhat riskier: some programming errors that a postcondition check may catch might pass the invariant audit.

When are you supposed to check invariants? As I said, in principle you could check them at the beginning and end of all methods, and at the end of all constructors. This is a standard, albeit drastic, solution that you can apply in all contexts. On the other hand, you may want to be a little more subtle, and avoid unnecessary checks, by focusing on those methods that could actually break an invariant.

Assume that you trust the constructor to initially establish all invariants. The constructor from Reference is so simple that you can easily count on that. Which methods can break invariants? Invariants are properties of objects’ states, so only methods that modify the value of the fields can potentially break an invariant.

Let’s examine the three public methods of Reference:

• getAmount is clearly a read-only method, and therefore it can’t break any invariant.
• addWater modifies the amount field, so it could in principle break invariants I1 and I4 of all the containers it touches.
• Finally, connectTo is the most critical method, because it modifies both fields of many containers. If improperly coded, it could break all invariants for many containers.

Table 5.3 summarizes these observations.

Table 5.3. What each method modifies and which invariants it could break

One way to avoid unnecessary work is to check an invariant only at the end of the methods that could break it. We’ll implement these checks using assertions, essentially treating invariants as postconditions of those methods. This simplification is safe, in the sense that you’re still able to attribute an invariant violation to the method that caused it. Indeed, since the state of our objects starts in an invariant-abiding condition and is properly encapsulated (that is, private), only public methods can be responsible for tarnishing it. As soon as one public method messes up, you’ll witness the error as an assertion failure coming from that method.

According to table 5.3, we can focus on methods connectTo and addWater. Both of these methods modify the state of multiple objects, so we should check the invariants of all the objects they touch. This is particularly cumbersome for method connectTo: according to its contract, an invocation like a.connectTo(b) is supposed to modify the state of all containers that, at the start of the method, are connected to either a or b. However, at the point when we plan to check the invariants, that is, at the end of the method, we don’t know which containers were previously connected to either a or b, unless we implicitly trust the correctness of the method itself.

5.4.1. Checking the invariants in connectTo

As I illustrated in the previous discussion, when it comes to checking the invariants at the end of connectTo, you have two options:

1. At the beginning of the method, store (a copy of) the current groups of this and other so that you can then properly check the invariants on all relevant objects.
2. Only check the state of the objects belonging to the single group obtained at the end of the method.

Option 1 is safer, but it resembles the heavy work you ended up doing in the previous section to check the postcondition of connectTo. I advise you to pursue option 2, instead, which is more practical and gives partial trust to the method. It assumes that it correctly merges the two preexisting groups into a single one, and it checks all the other properties that the invariants cover.

You should end up with something akin to the following listing, where the invariant-checking task is delegated to a private support method. I’m omitting the central part of connectTo, as it’s exactly the same as in Reference.

Listing 5.9. Invariants: Method connectTo (abridged) and its support method

   public void connectTo(Container other) {
      Objects.requireNonNull(other,        1 Checks the precondition
                             "Cannot connect to a null container.");

      ...   2 The actual operation goes here (same as Reference)

      assert invariantsArePreservedByConnectTo(other) :
             "connectTo broke an invariant!";       3 Checks the invariants
   }

   private boolean invariantsArePreservedByConnectTo(Container other) {
      return group == other.group &&
             isGroupNonNegative() &&
             isGroupBalanced() &&
             isGroupConsistent();
   }

By choosing option 2, you don’t have to save the state of any object at the beginning of connectTo. You can just check the precondition (in the second line), perform the connection operation (same as Reference), and finally check the (simplified) invariants (in the assert line).

Three more support methods are involved in checking the invariants. You’ve already seen an implementation of isGroupBalanced in the previous section. You can see now that it’s checking invariant I4. The other two invariant-checking methods are detailed in the following listing.

Listing 5.10. Invariants: Two invariant-checking support methods

   private boolean isGroupNonNegative() {  1 Checks invariant I1
      for (Container x: group) {
         if (x.amount < 0) return false;
      }
      return true;
   }
   private boolean isGroupConsistent() {  2 Checks invariants I2, I3
      for (Container x: group) {
         if (x.group != group) return false;
      }
      return true;
   }

To see that we aren’t catching all invariant violations, consider the scenario in figure 5.5. On the left side (Before), three containers are connected into two groups: a is isolated, whereas b and c are connected. We don’t care about water amounts in this example; assume they’re equal in all containers. This state of affairs satisfies all invariants.

Figure 5.5. The situation before and after a faulty a.connectTo(b) operation. The checks in Invariants don’t catch this type of fault. Water amounts are omitted as unimportant.

Now, imagine that a faulty implementation of a.connectTo(b) brings about the situation on the right side (After). Instead of joining all of the containers in a single group, that implementation updates the group of a to include a and b, and container b now points to its new group. Meanwhile, container c and its group are left untouched. As a consequence, container c still “believes” it belongs to a group including b and c.

This fault breaks invariant I2 because b belongs to two different groups, but Invariants doesn’t detect the problem. Indeed, by choosing option 2 that I described earlier, you’ll check only that the two containers being connected (a and b) point to the same group and that the group field of all containers in that group actually points to that group (method isGroupConsistent).

The fault in figure 5.5 would be detected if we chose option 1 instead of option 2. Also, Contracts would detect it as a postcondition violation.

5.4.2. Checking the invariants in addWater

The implementation of addWater follows the same scheme as connectTo. As I discussed earlier and summarized in table 5.3, it’s enough to check the validity of invariants I1 and I4 because they’re the only ones that addWater could possibly invalidate.

As you can see in the following listing, invariant verification is delegated to a private support method that invokes two other methods that you’ve already encountered in the previous sections.

Listing 5.11. Invariants: Method addWater and its support method

   public void addWater(double amount) {
      double amountPerContainer = amount / group.size();

      if (this.amount + amountPerContainer < 0) {  1 Checks the precondition
         throw new IllegalArgumentException(
            "Not enough water to match the addWater request.");
      }
      for (Container c: group) {
         c.amount += amountPerContainer;
      }
      assert invariantsArePreservedByAddWater() :  2 Checks the invariants
             "addWater broke an invariant!";
   }

   private boolean invariantsArePreservedByAddWater() {
      return isGroupNonNegative() && isGroupBalanced();
   }

5.5. And now for something completely different

Let’s apply the techniques from this chapter to a different, drier example (no water involved). Consider a class BoundedSet<T>, representing a bounded-size set that keeps track of the order of insertion of its elements. In detail, a BoundedSet has a fixed maximum size, called its capacity, established at construction time. The class offers the following methods:

• void add(T elem)—Adds the specified element to this bounded set. If this addition brings the set size beyond its capacity, this method removes from the set the oldest element (the one that was inserted first). The addition of an element that already belongs to the set renews it (that is, it makes the element the newest one in the set).
• boolean contains(T elem)—Returns true if this bounded set contains the specified element.

This type of functionality is common when a program needs to remember a small number of frequently used items, as in a cache. Concrete examples include the Open Recent menu entry of many programs or the Recently Used Programs feature of the Windows Start menu.

5.5.1. The contracts

The first step toward a reliable implementation involves stating the method contracts in more detail, clearly distinguishing preconditions and postconditions. In this particular case, there’s very little to add to the informal descriptions of the methods because those two methods have no preconditions: you can invoke them at any time with any argument (except null). You obtain the following contract for add:

• Precondition— Argument is not null.
• Postcondition— Adds the specified element to this bounded set. If this addition brings the set size beyond its capacity, this method removes from the set the oldest element (the one that was inserted first). The addition of an element that already belongs to the set renews it (that is, it makes the element the newest one in the set).
• Penalty— Throws NullPointerException.

For contains, you may want to explicitly say in the postcondition that this method doesn’t modify its set:

• Precondition— Argument is not null.
• Postcondition— Returns true if this bounded set contains the specified element. It doesn’t modify this bounded set.
• Penalty— Throws NullPointerException.

5.5.2. A baseline implementation

Before actively checking these contracts, start with a plain implementation of Bounded Set. In this way, you’ll see more clearly the costs associated with those checks. First, choose the internal representation for a bounded set. A linked list is a handy choice because it allows you to keep the elements sorted by insertion time and efficiently remove the oldest element with the dedicated method removeFirst. However, this doesn’t mean that insertion in a bounded set will occur in constant time. To renew an element that’s already present, you need to scan the list, remove the element from its current position, and then add it to the front of the list, which takes linear time.

You get the following basic structure for the class:

public class BoundedSet<T> {
   private final LinkedList<T> data;
   private final int capacity;

   public BoundedSet(int capacity) {  1 Constructor
      this.data = new LinkedList<>();
      this.capacity = capacity;
   }

Next come the two methods. As you can see, the linked list allows you to write a very simple implementation, in exchange for limited performance (one of the typical trade-offs filling this book).

   public void add(T elem) {
      if (elem==null) {
         throw new NullPointerException();
      }
      data.remove(elem);   1 Removes elem if it’s already there
      if (data.size() == capacity) {
         data.removeFirst();  2 If full, removes the oldest
      }
      data.addLast(elem);  3 Adds elem as the newest
   }
   public boolean contains(T elem) {
      return data.contains(elem);
   }

5.5.3. Checking the contracts

As we’ve done with water containers, let’s design a hardened implementation of Bounded Set whose methods actively check their contracts.

Focus on the postcondition of add, which is the most interesting part of both contracts. Since add is supposed to modify the state of the bounded set in a specific and substantial way, the hardened add method needs to start by making a copy of the current state of the bounded set. At the end of add, a private support method will compare the current state of this bounded set with the copy made at the beginning of add and check that it’s been modified according to the contract.

The modern suggested way to provide copy capability to a class is through a copy constructor,^[9] that is, a constructor accepting another object of the same class. You can easily achieve that for BoundedSet:

⁹

Check out item 13 in Effective Java to learn why that’s preferred over the clone method for new classes.

   public BoundedSet(BoundedSet<T> other) {  1 Copy constructor
      data = new LinkedList<>(other.data);
      capacity = other.capacity;
   }

As I’ve discussed with regard to water containers, you should make sure that you only execute everything connected to the postcondition check, including the initial copy, when assertions are enabled. As before, you can achieve this objective by wrapping the initial copy in a dummy assert statement.

   public void add(T elem) {
      BoundedSet<T> copy = null;
      assert (copy = new BoundedSet<>(this)) != null;  1 Dummy assert

      ...  2 The actual operation goes here.

      assert postAdd(copy, elem) :  3 Checks the postcondition
             "add failed its postcondition!";
   }

Finally, the following code shows the private support method responsible for actually checking the postcondition. It first checks that the newly added element sits at the front of the current list. Then, it makes a copy of the current list so it can remove the newest element from both the current and old lists. At that point, it compares the position of all other elements before and after the call to add—they should be the same. You can handily delegate this check to the equals method of the lists.

   private boolean postAdd(BoundedSet<T> oldSet, T newElement) {
      if (!data.getLast().equals(newElement)) {  1 newElement must be at the front.
         return false;
      }
       2 Removes newElement from both old and new
      List<T> copyOfCurrent = new ArrayList<>(data);
      copyOfCurrent.remove(newElement);
      oldSet.data.remove(newElement);
      if (oldSet.data.size()==capacity) {  3 If it was full, drop the oldest.
         oldSet.data.removeFirst();
      }
       4 All remaining objects should be the same, in the same order.
      return oldSet.data.equals(copyOfCurrent);
   }

As with water containers, checking the postcondition takes more effort than the add operation that you’re scrutinizing, both at coding time and at runtime. This confirms that you should reserve such checks for special circumstances, such as in safety-critical software or for particularly tricky routines.

5.5.4. Checking the invariants

Recall that an invariant is a static consistency property on the fields of a class that should hold at all times, except when an object is undergoing change because of a method. Given the chosen representation for bounded sets (the fields data and capacity), only two consistency properties characterize a valid bounded set:

Any list and any integer satisfying these two invariants are sound, and you could, in fact, obtain them by a legal sequence of operations on an initially empty bounded set. You should check these invariants in a private support method, like the following:

   private boolean checkInvariants() {
      if (data.size() > capacity)  1 Invariant I1
         return false;
       2 Invariant I2 follows.
      Set<T> elements = new HashSet<>();
      for (T element: data) {
         if (!elements.add(element))  3 If add returns false, this element is a duplicate.
            return false;
      }
      return true;
   }

Once again, focus on the add method. The method contains is a trivial one-liner that can’t spoil the state of the object.

A hardened add, instead, can check the invariants at the end of each call. As usual, put such a check in an assert statement so you can easily turn on and off all reliability enhancements together (but remember, they’ll be off by default).

   public void add(T elem) {
      ...  1 The actual operation goes here.

      assert checkInvariants() : "add broke an invariant!";
   }

Some potential bugs in add might pass unnoticed by the invariant check but be flagged by the more thorough postcondition check from the previous section. For example, imagine if add removed the oldest element even when the bounded set wasn’t full. The invariant check wouldn’t notice the problem because this defect doesn’t bring the bounded set into an inconsistent state. More precisely, the state of affairs after add is not inconsistent in itself. It’s just inconsistent with respect to the history of that object, but invariants don’t care about history. The postcondition, on the other hand, would catch this defect by comparing the state of the bounded set before and after the add operation.

5.6. Real-world use cases

Refactoring addWater to enforce the design-by-contract principles was not an easy job. In fact, it was necessary to write more code to implement precondition and postcondition checks than to perform the actual business logic. The key question is: Is it worth the trouble? Here are some real-world use cases for you to consider:

• Let’s say you’re working for a small startup that a bank has hired to develop software for handling ATM transactions. Deadlines are pushing very hard, as the bank has grown substantially and needs to replace its legacy transaction-handling software, which can’t handle the expansion of the retail network. To meet the deadlines, the software leader in your team makes a catastrophic decision: focus on the business logic to be able to deliver a solution fast. Luckily, banks don’t trust anyone. They have their own team of software testers who put everything under the microscope before deploying to production. It turns out that the elegantly crafted software your team has developed suffers from a minor bug: it’s possible to withdraw more than you actually have in your bank account—and all that embarrassment is because the software skipped a precondition check. Software fails, and often it fails catastrophically. Paying the cost of reliability during development will prevent future despair.
• You might want to take a library you’ve developed in the past and refactor it to take advantage of the features of the underlying programming language’s latest release. Or you may want to refactor the existing code to add some new features. The cost of poor design may not be obvious at the first library releases, but poor design accrues over time, and people have even come up with a term for the eventual cost of poor design: technical debt. As it accrues, technical debt might even impede future evolution of the library. Design by contract and the related programming techniques help control technical debt by promoting explicit specifications and reliability.
• When creating new software, developers often face the following dilemma: what programming language should we use? Obviously, the answer depends on many factors, and among them are the complexity of the underlying system and its reliability. It turns out that the more complicated the system design, the more difficult it is to make the system behave correctly and be robust under unexpected events. When reliability is a primary concern, one consideration is how much of a contract can your programming language express in a way that you can check at compile time. You may end up switching your programming paradigm so you can catch more defects at compile time. For example, functional programming is known to promote reliability but at the cost of a steeper learning curve and occasionally lower performance.

Let’s not fool ourselves: failure is inevitable. That’s why I defined robustness as the capability of a system to react gracefully in situations that may lead to failure, rather than a system that’s designed to avoid all possible causes of failure. Modern distributed systems are prone to failure because of their inherent nature and are thus created with this principle in mind: partial failures, inconsistencies, and reordering of messages among the nodes are impossible to control. Instead, they’re part of the design contract so you can handle them gracefully.

5.7. Applying what you learned

Exercise 1

1. Write down the contract for the method add from the java.util.Collection interface. (Yes, you can look at the Javadoc.)

2. Do the same for the method add from the java.util.HashSet class.

3. Compare the two contracts. How are they different?

Exercise 2

Implement the static method interleaveLists, defined by the following contract:

• Precondition— The method receives as arguments two Lists of the same length.
• Postcondition— The method returns a new List containing all the elements of the two lists, in an alternating fashion.
• Penalty— If at least one of the lists is null, the method throws NullPointer Exception. If the lists have different lengths, the method throws Illegal ArgumentException.

Make sure that the precondition is always checked, and the postcondition is checked only if assertions are enabled. Try to minimize the overhead when you have assertions disabled.

Exercise 3

An object of type java.math.BigInteger represents an integer of arbitrary size, internally encoded by an array of integers. Check out its source code in OpenJDK (http://mng.bz/Ye6j) and locate the following private members:

private BigInteger(int[] val)
private int parseInt(char[] source, int start, int end)

1. Write down the contract of the private constructor. Make sure to include in the precondition all assumptions that the constructor needs to terminate regularly. Does the constructor actively check its precondition?

2. Do the same for the parseInt method.

Exercise 4

The following method supposedly returns the greatest common divisor of two given integers. (Don’t worry; you don’t need to understand it.) Modify it so it checks its postcondition when assertions are enabled, and try it on 1000 pairs of integers. (You can find the following code in the eis.chapter5.exercises.Gcd class in the online repository at https://bitbucket.org/mfaella/exercisesinstyle.)

Hint: Try to check the postcondition in the simplest possible way. You shouldn’t have doubts about the correctness of the check itself.

private static int greatestCommonDivisor(int u, int v) {
   if (u == 0 || v == 0) {
      if (u == Integer.MIN_VALUE || v == Integer.MIN_VALUE) {
         throw new ArithmeticException("overflow: gcd is 2^{}31");
      }
      return Math.abs(u) + Math.abs(v);
   }
   if (Math.abs(u) == 1 || Math.abs(v) == 1) {
      return 1;
   }
   if (u > 0) { u = -u; }
   if (v > 0) { v = -v; }
   int k = 0;
   while ((u & 1) == 0 && (v & 1) == 0 && k < 31) {
      u /= 2;
      v /= 2;
      k++;
   }
   if (k == 31) {
      throw new ArithmeticException("overflow: gcd is 2^{}31");
   }
   int t = (u & 1) == 1 ? v : -(u / 2);
   do {
      while ((t & 1) == 0) { t /= 2; }
      if (t > 0) { u = -t; }
      else { v = t; }
      t = (v - u) / 2;
   } while (t != 0);
   return -u * (1 <{}< k);
}

Summary

• Software reliability starts with clear specifications.
• A standard form of specifications is in terms of method contracts and class invariants.
• You should check preconditions for public methods during all phases of the development process.
• You should check other preconditions, postconditions, and invariants only as needed, during development or in safety-critical software.
• Assertions allow you to enable or disable certain checks at any program run.

Answers to quizzes and exercises

Pop Quiz 1

Throwing a checked exception as a penalty forces the caller to deal with that exception, either by catching it or by declaring it in its throws clause. This is cumbersome because the penalty can simply be avoided by respecting the preconditions. Checked exceptions are intended for exceptional conditions that can’t be avoided because they’re outside the direct control of the caller.

Pop Quiz 2

A graceful reaction to running out of paper is to alert the user to the problem and give them the option to retry or abort the printing. In contrast, ungraceful reactions would be to crash the program or to silently ignore the print request.

Pop Quiz 3

The proposed property compares the state of an object before and after a method call. That’s the job of a postcondition, not an invariant. Invariants can only refer to the current state of an object.

Pop Quiz 4

You initialize the flag with false and then set it to true using a dummy assertion:

boolean areAssertionsEnabled = false;
assert (areAssertionsEnabled = true) == true;

Pop Quiz 5

Recall that not-a-number (NaN) is one of the special values for floating point numbers, together with plus and minus infinities. NaN is subject to special arithmetic rules. Those that concern this quiz are the following:

• NaN / n gives NaN
• NaN + n gives NaN
• NaN < n gives false
• NaN == NaN gives false (You read this right!)

Looking at the code of addWater in Contracts (listing 5.1), you can see that passing NaN as the value of the amount parameter passes the precondition check because this.amount + amountPerContainer < 0 evaluates to false. The subsequent lines set the amount field of all containers in the group to the value NaN. Finally, assuming you’ve enabled assertions, the method checks its postcondition through the method postAddWater (listing 5.4). There, NaN will fail both the isGroupBalanced() and the almostEqual() tests, and the invocation will terminate with an AssertionError.

If you have assertions disabled (as they are by default), the invocation to getAmount silently sets all containers in the group to holding NaN. These observations suggest that the contract of addWater should in fact be refined to tackle NaN and the other special values in a more reasonable way, such as by declaring them invalid through the precondition.

Exercise 1

1. The contract of an abstract method tends to be more involved than that of a concrete method. An abstract method has no implementation, so it’s basically a pure contract. Therefore, its contract needs to be clear and detailed. The situation is even more sensitive in an interface like Collection, which, being the root of the collection hierarchy, must accommodate a large variety of specializations (precisely 34, among classes and interfaces).

The Javadoc for Collection.add contains a wealth of information. Start with the qualifier “optional operation.” You can interpret it as specifying two alternative contracts for this method. First, an implementation can choose not to support insertions, like an immutable collection. In that case, it must respect the following contract:

• Precondition— No invocation is legitimate.
• Postcondition— None.
• Penalty— Throws UnsupportedOperationException.

If the class implementing Collection supports insertions, it must obey a different contract. Such a class can freely choose the precondition of add, to constrain the kind of insertions that are legitimate, but it must issue specific penalties when rejecting an insertion, as the following contract describes:

• Precondition— Implementation-defined.
• Postcondition— Ensures that this collection contains the specified element. Returns true if this collection changed as a result of the call.
• Penalty— Throws:
  • ClassCastException if the argument is invalid because of its type
  • NullPointerException if the argument is null and this collection rejects null values
  • IllegalArgumentException if the argument is invalid because of some other property
  • IllegalStateException if the argument can’t be inserted at this time

Note how this contract doesn’t specify under which conditions an insertion will change the underlying collection. That burden lies with the subclasses.

2. The class HashSet specializes the contract for add as follows:

• Precondition— None. (All arguments are legitimate.)
• Postcondition— Inserts the specified element in this collection, unless an element equal to it (according to equals) is already present. Returns true if this collection didn’t contain the specified element before the call.
• Penalty— None.

3. The contract in HashSet specifies that this collection doesn’t contain duplicate elements. Attempting to insert a duplicate is not an error: it doesn’t violate the precondition and it doesn’t raise an exception. It just leaves the collection unchanged.

Exercise 2

Here’s the code for the interleaveLists method. Note how regular if statements check the precondition, whereas the postcondition is delegated to a separate method, only invoked when assertions are enabled.

public static <T> List<T> interleaveLists(List<? extends T> a,
                                          List<? extends T> b) {
  if (a==null || b==null)
      throw new NullPointerException("Both lists must be non-null.");
  if (a.size() != b.size())
      throw new IllegalArgumentException(
                "The lists must have the same length.");

  List<T> result = new ArrayList<>();
  Iterator<? extends T> ia = a.iterator(), ib = b.iterator();
  while (ia.hasNext()) {
      result.add(ia.next());
      result.add(ib.next());
  }
  assert interleaveCheckPost(a, b, result);
  return result;
}

Here’s the code for the support method responsible for checking the postcondition:

private static boolean interleaveCheckPost(List<?> a, List<?> b,
                                           List<?> result) {
  if (result.size() != a.size() + b.size())
      return false;

  Iterator<?> ia = a.iterator(), ib = b.iterator();
  boolean odd = true;
  for (Object elem: result) {
      if ( odd && elem != ia.next()) return false;
      if (!odd && elem != ib.next()) return false;
      odd = !odd;
  }
  return true;
}

Exercise 3

First, note a few details about how these private members are documented. The official Javadoc page for BigInteger doesn’t mention any private member. That’s the default behavior for Javadoc, and you can change it using the --show-members pri vate command-line option. Still, in the source code, the constructor is equipped with a full comment in Javadoc style, whereas the method is preceded by a brief comment in free format. Apparently, the constructor is deemed important enough to warrant more detailed documentation. In chapter 7, you’ll learn more about Javadoc and documentation guidelines. Now, let’s extract the contracts from these comments and from the code.

1. Regarding the constructor, the Javadoc mentions that val should not be modified during the execution of the constructor. This property refers to multithreaded contexts, where the program may be executing other code at the same time as this constructor. As such, this requirement doesn’t exactly fit in the classic form of contract presented in this chapter, as that’s tailored to sequential programs.

On the other hand, a quick look at the constructor source code shows that the array val is also implicitly assumed to be non-null and non-empty, leading to the following contract:

• Precondition— val is non-null and non-empty.
• Postcondition— It creates the BigInteger corresponding to the integer encoded in val in two’s-complement big-endian format.
• Penalty— Throws:
  • NullPointerException if val is null
  • NumberFormatException if val is empty (length 0)

The constructor is actively checking whether the array val is empty. There’s no need to check for val being null because that case induces an NPE automatically.^[10]

¹⁰

You may still prefer to check that explicitly to clarify your intent and equip the exception with a more specific error message.

2. The comment preceding parseInt declares “Assumes start < end.” That’s one explicit precondition. Skimming through the method body, you’ll also notice that the source argument must be non-null and that start and end must be valid indices in source. Finally, every character in the specified interval of source must be a digit. You can put these observations in contract form as follows:

• Precondition— source is a non-null sequence of digit characters; start and end are valid indices for source, and start < end.
• Postcondition— Returns the integer that the digits between the two indices start and end represent.
• Penalty— Throws:
  • NullPointerException if source is null
  • NumberFormatException if any character in the specified interval is not a digit
  • ArrayIndexOutOfBoundsException if start or end is not a valid index in source

The method actively checks that each character in the interval is a digit. It omits the check for null as redundant. The only precondition explicitly stated in the documentation is not checked: invoking the method with start ≥ end doesn’t raise any exception, but, rather, returns the integer corresponding to the single character source[start].

As a side remark, this method doesn’t use any instance field, so it should be static.

Exercise 4

The code for this exercise is a slightly edited excerpt from the class Fraction^[11] from the Apache Commons project. It employs a highly non-obvious algorithm by Donald Knuth. Since the method modifies its arguments, and you need those arguments to check the postcondition, you need to store their original values in two additional variables. Then, at the end of the method, you can check the postcondition using an auxiliary method.

¹¹

The fully qualified class name is org.apache.commons.lang3.math.Fraction.

   private static int greatestCommonDivisor(int u, int v) {
      final int originalU = u, originalV = v;

        1 The original procedure goes here (modifies u and v).

      int gcd = -u * ( 1 <{}< k);
      assert isGcd(gcd, originalU, originalV) : "Wrong GCD!";
      return gcd;
   }

For the auxiliary isGcd method, I said the simplest solution is preferable. In this case, you may simply apply the definition of “greatest common divisor,” and check that

• gcd is indeed a common divisor of originalU and originalV
• every larger number is not a common divisor

   private static boolean isGcd(int gcd, int u, int v) {
        if (u \% gcd != 0 || v \% gcd != 0)   1 Checks that gcd is a common divisor
            return false;
        for (int i=gcd+1; i<=u && i<=v; i++)   2 Checks any larger number,
            if (u \% i == 0 && v \% i == 0)      up to the minimum of u and v
                return false;
        return true;
   }

This implementation of isGcd is very inefficient, being linear in the size of the smallest number between u and v. A more reasonable course of action would be to use Euclid’s classic algorithm (https://en.wikipedia.org/wiki/Euclidean_algorithm) or invoke an already implemented GCD procedure, such as the BigInteger.gcd() method from the JDK.

Further reading

• Bertrand Meyer. Object-Oriented Software Construction. Prentice Hall, 1997. This book formally introduced the design-by-contract methodology and the programming language, Eiffel, designed to support it.
• J.-M. Muller et al. Handbook of Floating-Point Arithmetic. Birkhäuser, 2010. Want to impress friends and family with your mastery of everything floating-point? Study this volume of over 500 pages. It comes with a free PhD in computer science.
• David Goldberg. “What Every Computer Scientist Should Know About Floating-Point Arithmetic.” ACM Computing Surveys, 23, 1991. At 44 pages, this article delivers its promise, but it doesn’t grant a PhD.
• Joshua Bloch. Effective Java. Addison-Wesley, 2017. The third edition of a celebrated book on Java best practices. Written by one of the designers of the Java platform.