Reading 6: Specifications

Specifications are the linchpin of teamwork. It’s impossible to delegate responsibility for implementing a method without a specification. The specification acts as a contract: the implementer is responsible for meeting the contract, and a client that uses the method can rely on the contract. In fact, we’ll see that like real legal contracts, specifications place demands on both parties: when the specification has a precondition, the client has responsibilities too.

In this reading we’ll look at the role played by specifications of methods. We’ll discuss what preconditions and postconditions are, and what they mean for the implementer and the client of a method. We’ll also talk about how to use exceptions, an important language feature found in Java, Python, and many other modern languages, which allows us to make a method’s interface safer from bugs and easier to understand.

Before we dive into the structure and meaning of specifications…

And keep making progress on Java by completing these categories in the Java Tutor:

Suppose you are working on a program containing this method, which finds the index of an integer in an array:

static int find(int[] arr, int val) {
    for (int i = 0; i < arr.length; i++) {
        if (arr[i] == val) return i;
    }
    return -1;
}

This find method has many clients in the program (places where the method is called). Now you’ve realized that frequently in this program, when find is called with a large array, the value it finds is likely to be either close to the start of the array (which is very fast to find), or close to the end (which is very slow, because it requires checking almost the entire array). So you have the clever idea to speed things up by searching from both ends of the array at the same time:

static int find(int[] arr, int val) {
    for (int i = 0, j = arr.length-1; i <= j; i++, j--) {
        if (arr[i] == val) return i;
        if (arr[j] == val) return j;
    }
    return -1;
}

Is it safe to replace find with this new implementation? Can we make this change without introducing bugs? To determine behavioral equivalence, our question is whether we could substitute one implementation for the other.

Not only do these implementations have different performance characteristics, they actually have different behavior. If val happens to appear more than once in the array, the original find always returns the lowest index at which it occurs. But the new find might return the lowest index or the highest index, whichever it finds first.

But when val occurs at exactly one index of the array, the two implementations behave the same: they both return that index. It may be that the clients never rely on the behavior outside of that case. Whenever they call the method, they will be passing in an array with exactly one element matching val. For such clients, these two versions of find are the same, and we could switch from one implementation to the other without issue.

The notion of behavioral equivalence is in the eye of the beholder — that is, the client. In order to make it possible to substitute one implementation for another, and to know when this is acceptable, we need a specification that states exactly what the client depends on.

In this case, a specification that would allow these two implementations to be behaviorally equivalent might be:

static int find(int[] arr, int val)

static int find(int[] a, int val) {
    for (int i = 0; i < a.length; i++) {
        if (a[i] == val) return i;
    }
    return a.length;
}

static int find(int[] a, int val) {
    for (int i = a.length - 1 ; i >= 0; i--) {
        if (a[i] == val) return i;
    }
    return -1;
}

Our find example showed how a specification can help make a program both ready for change and safe from bugs. Many of the nastiest bugs in programs arise because of misunderstandings about behavior at the interface between two pieces of code. Although every programmer has specifications in mind, not all programmers write them down. As a result, different programmers on a team have different specifications in mind. When the program fails, it’s hard to determine where the error is. Precise specifications in the code let you apportion blame (to code fragments, not people!), and can spare you the agony of puzzling over where a bug fix should go.

Specifications are good for the client of a module because they help make the module easier to understand. Having a specification lets you understand what the module does without having to read the module’s code. If you’re not convinced that reading a spec is easier than reading code, compare our spec for find on the left, with its tricky implementation on the right:

static int find(int[] arr, int val)

static int find(int[] arr, int val) {
    for (int i = 0, j = arr.length-1; i <= j; i++, j--) {
        if (arr[i] == val) return i;
        if (arr[j] == val) return j;
    }
    return -1;
}

Specifications are good for the implementer of a method because they give the implementer freedom to change the implementation without telling clients. Specifications can make code faster, too. We’ll see that a specification can rule out certain states in which a method might be called. This restriction on the inputs might allow the implementer to skip an expensive check that is no longer necessary and use a more efficient implementation.

The contract acts as a firewall between client and implementer. It shields the client from the details of the workings of the module: as a client, you don’t need to read the source code of the procedure if you have its specification. And it shields the implementer from the details of the usage of the module: as an implementer, you don’t have to ask every client how they plan to use the module. This firewall results in decoupling, allowing the code of the module and the code of a client to be changed independently, so long as the changes respect the specification — each obeying its obligation.

Abstractly speaking, a specification of a method has several parts:

• a method signature, giving the name, parameter types, return type, and exceptions thrown
• a requires clause, describing additional restrictions on the parameters
• an effects clause, describing the return value, exceptions, and other effects of the method

Taken together, these parts form the precondition and the postcondition of the method.

The precondition is an obligation on the client (the caller of the method). It is a condition over the state in which the method is invoked. One aspect of the precondition is the number and types of the parameters in the method signature. Additional conditions are written down in the requires clause, for example:

• narrowing a parameter type (e.g. x >= 0 to say that an int parameter x must actually be a nonnegative int)
• interactions between parameters (e.g., val occurs exactly once in arr)

The postcondition is an obligation on the implementer of the method. It includes the parts that Java can statically check: the return type and declared checked exceptions. Additional conditions are written down in the effects clause, including:

• how the return value relates to the inputs
• which exceptions are thrown, and when
• whether and how objects are mutated

In general, the postcondition is a condition on the state of the program after the method is invoked, assuming the precondition was true before.

The overall structure is a logical implication: if the precondition holds when the method is called, then the postcondition must hold when the method completes.

If the precondition does not hold when the method is called, the implementation is not bound by the postcondition. It is free to do anything, including never returning, throwing an exception, returning arbitrary results, making arbitrary mutations, etc.

static int find(int[] arr, int val)

Some languages (notably Eiffel) incorporate preconditions and postconditions as a fundamental part of the language, as expressions that the runtime system (or even the compiler) can automatically check to enforce the contracts between clients and implementers.

Java does not go quite so far, but its static type declarations are effectively part of the precondition and postcondition of a method, a part that is automatically checked and enforced by the compiler. The rest of the contract — the parts that we can’t write as types — must be described in a comment preceding the method, and generally depends on human beings to check it and guarantee it.

Java has a convention for documentation comments, in which parameters are described by @param clauses and results are described by @return clauses. You should put the preconditions into @param where possible, and postconditions into @return. So a specification like this:

static int find(int[] arr, int val)

… might be rendered in Java like this:

/**
 * Find a value in an array.
 * @param arr array to search, requires that val occurs exactly once
 *            in arr
 * @param val value to search for
 * @return index i such that arr[i] = val
 */
static int find(int[] arr, int val)

The Java API documentation is produced from Javadoc comments in the Java standard library source code. Documenting your specifications in Javadoc allows Eclipse to show you (and clients of your code) useful information, and allows you to produce HTML documentation in the same format as the Java API docs.

static boolean isPalindrome(String word)

/*
 * Check if a word is a palindrome.
 * A palindrome is a sequence of characters
 * that reads the same forwards and backwards.
 * @param String word
 * @requires word contains only alphanumeric characters
 * @effects returns true if and only if word is a palindrome
 * @return boolean
 */

/**
 * Find the winner of a standard 3x3 tic-tac-toe game.
 * @param board   a completely-full board of 'X' or 'O', in row-major order
 * @return 'X' or 'O'
 * @throws TieException if the board is a tie
 */
static String endGame(char[][] board) throws TieException

def guess(secret_word, letters_guessed):
    '''
    secret_word: string, the word the user is guessing
    letters_guessed: list (of letters), which letters have been guessed so far
    returns: string, secret_word with not-yet-guessed letters replaced by underscores (_)
    '''

What a specification may talk about

In Java, references to objects and arrays can also take on the special value null, which means that the reference doesn’t point to an object. Null values are an unfortunate hole in Java’s type system.

Primitives cannot be null:

int size = null;     // illegal
double depth = null; // illegal

and the compiler will reject such attempts with static errors.

On the other hand, we can assign null to any non-primitive variable:

String name = null;
int[] points = null;

and the compiler happily accepts this code at compile time. But you’ll get errors at runtime because you can’t call any methods or use any fields with one of these references:

name.length()   // throws NullPointerException  
points.length   // throws NullPointerException

Note, in particular, that null is not the same as an empty string "" or an empty array. On an empty string or empty array, you can call methods and access fields. The length of an empty array or an empty string is 0. The length of a string variable that points to null isn’t anything: calling length() throws a NullPointer­Exception.

Also note that arrays of non-primitives and collections like List might be non-null but contain null as a value:

String[] names = new String[] { null };
List<Double> sizes = new ArrayList<>();
sizes.add(null);

These nulls are likely to cause errors as soon as someone tries to use the contents of the collection.

Null values are troublesome and unsafe, so much so that most methods simply avoid them entirely. As a general convention, null values are disallowed in parameters and return values unless the spec explicitly says otherwise. So every method has a precondition on the object and array types in its parameters that they be non-null – including elements of collections like arrays, sets, lists, and maps. Every method that can return object or array types implicitly has a postcondition that their values are non-null, again including elements of collection types.

If a method allows null values in a parameter, it needs to explicitly state it, or if it might return a null value in a result, it should explicitly state it. But these are in general not good ideas. Avoid null.

There are extensions to Java that allow you to forbid null directly in the type declaration, e.g.:

static boolean addAll(@NonNull List<T> list1, @NonNull List<T> list2)

where it can be checked automatically at compile time or runtime.

Google has their own discussion of null in Guava, the company’s core Java libraries. The project explains:

Careless use of null can cause a staggering variety of bugs. Studying the Google code base, we found that something like 95% of collections weren’t supposed to have any null values in them, and having those fail fast* rather than silently accept null would have been helpful to developers.

Additionally, null is unpleasantly ambiguous. It’s rarely obvious what a null return value is supposed to mean — for example, Map.get(key) can return null either because the value in the map is null, or the value is not in the map. Null can mean failure, can mean success, can mean almost anything. Using something other than null makes your meaning clear.*

(*Boldface added for emphasis.)

If you avoid using null, there is still sometimes a need for a parameter or return value to indicate that a value is missing. For example, what should Map.get(key) return when the key is not found in the map? One good tool for this problem is Optional<T>. You can think of Optional<T> like a very constrained List<T> of length at most 1. It either contains just one element of type T, or it is empty. The isPresent() method tests whether or not it is empty, and get() and getOrElse() unpack the value if present. The key advantage of Optional<T> is that it can be used sparingly, only in places where it’s sensible for the spec to allow for a missing value, and it clearly expresses the intention of the spec in those cases.

public static String none() {
    return null;          // (1)
}

public static void main(String[] args) {
    String a = none();    // (2)
    String b = null;      // (3)
    if (a.length() > 0) { // (4)
        b = a;            // (5)
    }
    return b;             // (6)
}

Make sure to understand the difference between null and emptiness.

Recall that in Python, None is not the same as the empty string "", the empty list [ ], or the empty dictionary { }. These empty objects like these are valid objects that simply happen to contain no elements. But you can use them with all the usual operations allowed by the type. For example, len("") returns 0, and "" + "a" returns "a". That’s not true of None – len(None) and None + "a" both produce errors.

The same idea translates to Java. The null reference is not a valid string, or list, or map, or any other object. But the empty string "" is a valid String value, and the empty list List.of() is a valid list value.

The upshot of this is that empty values are always allowed as parameter or return values, unless a spec explicitly disallows them.

String computeSomething(List<String> list)

In testing, we talk about black box tests that are chosen with only the specification in mind, and glass box tests that are chosen with knowledge of the actual implementation (Testing). But it’s important to note that even glass box tests must follow the specification. Your implementation may provide stronger guarantees than the specification calls for, or it may have specific behavior where the specification is undefined. But your test cases should not count on that behavior. Test cases must be correct, obeying the contract just like every other client.

For example, suppose you are testing this specification of find, slightly different from the one we’ve used so far:

static int find(int[] arr, int val)

This spec has a strong precondition in the sense that val is required to be found; and it has a fairly weak postcondition in the sense that if val appears more than once in the array, this specification says nothing about which particular index of val is returned. Even if you implemented find so that it always returns the lowest index, your test case can’t assume that specific behavior:

int[] array = new int[] { 7, 7, 7 };
int i = find(array, 7);
assertEquals(0, i);  // bad test case: assumes too much, more than the postcondition promises
assertEquals(7, array[i]);  // correct

Similarly, even if you implemented find so that it (sensibly) throws an exception when val isn’t found, instead of returning some arbitrary misleading index, your test case can’t assume that behavior, because it can’t call find() in a way that violates the precondition.

So what does glass box testing mean, if it can’t go beyond the spec? It means you are trying to find new test cases that exercise different parts of the implementation, but still checking those test cases in an implementation-independent way, following the spec.

Testing units

/** 
 * @return the contents of the file
 */
public static String load(File file) { ... }

/**
 * @return the words in string s, in the order they appear, 
 *         where a word is a contiguous sequence of 
 *         non-whitespace and non-punctuation characters
 */
public static List<String> extract(String s) { ... }

/**
 * @return an index mapping a word to the set of files
 *         containing that word, for all files in the input set
 */
public static Map<String, Set<File>> index(Set<File> files) { 
    ... calls load() and extract() ...
} 

public static int gcd(int a, int b) {
    if (a > b) {
        return gcd(a-b, b);
    } else if (b > a) {
        return gcd(a, b-a);
    }
    return a;
}

@Test public void gcdTest() {
    assertEquals(6, gcd(24, 54));
}

We discussed mutable vs. immutable objects in an earlier reading (Basic Java). But our specification examples thus far haven’t illustrated how to describe side-effects — changes to mutable objects — in the postcondition.

So here’s a specification that describes a method that mutates an object:

static boolean addAll(List<T> list1, List<T> list2)

We’ve taken this, slightly simplified, from the Java List interface. First, look at the postcondition. It gives two constraints: the first telling us how list1 is modified, and the second telling us how the return value is determined.

---

---

Second, look at the precondition. It tells us that list1 cannot be the same object as list2. The behavior of the method if you attempt to add the elements of a list to itself is undefined. You can easily imagine why the implementer of the method would want to impose this constraint: it’s not likely to rule out any useful applications of the method, and it makes it easier to implement. The specification allows a simple implementation in which you take an element from list2 and add it to list1, then go on to the next element of list2 until you get to the end.

If list1 and list2 are the same list, this simple algorithm will not terminate, as shown in the sequence of snapshot diagrams on the right — or practically speaking it will throw a memory error when the list object has grown so large that it consumes all available memory. Either outcome, infinite loop or crash, is permitted by the specification because of its precondition.

Remember also the implicit precondition that list1 and list2 must be valid objects, rather than null. We omit saying this because it’s virtually always required of object references.

Here is another example of a mutating method:

static void sort(List<String> list)

And an example of a method that does not mutate its argument:

static List<String> toLowerCase(List<String> list)

Just as null is implicitly disallowed unless stated otherwise, programmers also assume that mutation is disallowed unless stated otherwise. The spec of to­Lower­Case could explicitly state as an effect that “list is not modified”, but in the absence of a postcondition describing mutation, we demand no mutation of the inputs.

Now that we’re writing specifications and thinking about how clients will use our methods, let’s discuss how to handle exceptional cases in a way that is safe from bugs and easy to understand.

A method’s signature — its name, parameter types, return type — is a core part of its specification, and the signature may also include exceptions that the method may trigger.

Exceptions for signaling bugs

Exceptions for special results

class BirthdayBook {
    LocalDate lookup(String name) { ... }
}

LocalDate lookup(String name) throws NotFoundException {
    ...
    if ( ...not found... )
        throw new NotFoundException();
    ...

BirthdayBook birthdays = ...
try {
    LocalDate birthdate = birthdays.lookup("Alyssa");
    // we know Alyssa's birthday
} catch (NotFoundException nfe) {
    // her birthday was not in the birthday book
}

try {
    LocalDate birthdate = birthdays.lookup("Elliot");
}
System.out.println("done");

try {
    LocalDate birthdate = birthdays.lookup("Elliot");
} catch (NotFoundException nfe) {
    birthdate = LocalDate.now();
}
System.out.println("done");

try {
    LocalDate birthdate = birthdays.lookup("Elliot");
} catch (Exception NotFoundException) {
}
System.out.println("done");

try {
    LocalDate birthdate = birthdays.lookup("Elliot");
} catch (NotFoundException nfe) {
    throw new DateTimeException("Missing reference birthday", nfe);
}
System.out.println("done");

We’ve seen two different purposes for exceptions: special results and bug detection. As a general rule, you’ll want to use checked exceptions to signal special results, and unchecked exceptions to signal bugs.

Some terminology: checked exceptions are called that because they are checked by the compiler:

• If a method might throw a checked exception, the possibility must be declared in its signature. Not­Found­Exception would be a checked exception, and that’s why the signature ends with throws Not­Found­Exception.
• If a method calls another method that may throw a checked exception, it must either handle it, or declare the exception itself, since if it isn’t caught locally it will be propagated up to callers.

So if you call BirthdayBook’s lookup method and forget to handle the Not­Found­Exception, the compiler will reject your code. This is very useful, because it ensures that exceptions that are expected to occur will be handled.

Unchecked exceptions, in contrast, are used to signal bugs. These exceptions are not expected to be handled by the code except perhaps at the top level. We wouldn’t want every method up the call chain to have to declare that it (might) throw all the kinds of bug-related exceptions that can happen at lower call levels: index out of bounds, null values, illegal arguments, assertion failures, etc.

As a result, for an unchecked exception the compiler will not check for try-catch or a throws declaration. Java still allows you to write a throws clause for an unchecked exception as part of a method signature, but this has no effect, and is thus a bit funny, and we don’t recommend doing it.

All exceptions may have a message associated with them. If not provided in the constructor (e.g., as described for Runtime­Exception), the reference to the message string is null. This can result in confusing stack traces that start, for example:

birthday.NotFoundException: null
at birthday.BirthdayBook.lookup(BirthdayBook.java:42)

The “null” is misleading: in this case, it tells you the NotFoundException had no message string, not that a null value was responsible for the exception.

Exception hierarchy

To understand how Java decides whether an exception is checked or unchecked, let’s look at the class hierarchy for Java exceptions.

Exception is the normal base class of checked exceptions. The compiler applies static checking to methods using these exceptions. A checked exception must either be caught or declared when it’s possible for it to be thrown.

However, RuntimeException and its subclasses are unchecked exceptions. RuntimeException and its subclasses don’t have to be declared in the throws clause of a method that throws them, and doesn’t have to be caught or declared by a caller of such a method.

In addition, Error and its subclasses are unchecked exceptions. This part of the hierarchy is reserved for errors produced by the Java runtime system, such as StackOverflow­Error and OutOfMemory­Error. For some reason Assertion­Error also extends Error, even though it indicates a bug in user code, not in the runtime. Errors should be considered unrecoverable, and should not be caught by your code.

When you define your own exceptions, you should either subclass Exception (to make it a checked exception) or RuntimeException (to make it unchecked). Don’t subclass Error, because these kinds of exceptions are reserved by Java itself.

When you catch an exception with a try-catch statement, you should catch the most specific exception class possible. If you are expecting a FileNotFoundException, that’s what your catch statement should use. Catching a broad class of exceptions, like Exception or RuntimeException or Error, is not safe from bugs or ready for change, because it catches every possible subclass of these exceptions, which may interfere with static checking and hide bugs.

One of the confusing aspects of the Java exception hierarchy is that RuntimeException is itself a subclass of Exception. So the whole Exception family includes both checked exceptions (its direct descendents) and unchecked exceptions (the RuntimeException branch of the family) But Error is not a subclass of Exception, so all the unchecked Error-like exceptions are outside the Exception family.

reading exercises

Get to the point

Suppose we’re building a robot and we want to specify the function

public static List<Point> findPath(Point initial, Point goal)

which is responsible for path-finding: determining a sequence of Points that the robot should move through to navigate from initial to goal, past any obstacles that might be in the way.

In the postcondition, we say that findPath will search for paths only up to a bounded length (set elsewhere), and that it will throw an exception if it fails to find one.

Which of these would we choose?

throws a checked NoPathException(missing answer)

throws an unchecked NoPathException(missing answer)

throws a checked PathNotFoundException(missing answer)

throws an unchecked PathNotFoundException(missing answer)

(missing explanation)

check explain

Don’t point that thing at me

When we define our exception for findPath, which will we choose as our superclass?

Exception(missing answer)

Error(missing answer)

RuntimeException(missing answer)

(missing explanation)

check explain

Gotta catch ‘em all

Louis Reasoner doesn’t like checked exceptions. Whenever the Java compiler tells him to catch a checked exception, he simply wraps the entire body of the code he’s writing with a try-catch block. Here’s an example of how he might use the findPath method that we’ve just designed an exception for:

public void driveRobotAround() {
    try {
        ... // Louis's code

        path = findPath(initial, goal); // this method throws a checked PathNotFoundException

        ... // more of Louis's code

    } catch (Exception e) { // Louis makes the compiler happy
        return;
    }
}

How does his approach behave in the following situations?

findPath() throws a PathNotFoundException because too many obstacles are blocking the path. (PathNotFoundException is a subclass of Exception.)

this exception is a checked exception(missing answer)

this exception is an unchecked exception(missing answer)

the exception is caught by Louis’s catch clause(missing answer)

the exception is not caught(missing answer)

the exception’s stack trace is displayed so that the problem can be debugged(missing answer)

the exception is quietly ignored(missing answer)

(missing explanation)

findPath() throws an IndexOutOfBoundsException because its code for creating the point list is buggy. (IndexOutOfBoundsException is a subclass of RuntimeException, which is a subclass of Exception.)

this exception is a checked exception(missing answer)

this exception is an unchecked exception(missing answer)

the exception is caught by Louis’s catch clause(missing answer)

the exception is not caught(missing answer)

the exception’s stack trace is displayed so that the problem can be debugged(missing answer)

the exception is quietly ignored(missing answer)

(missing explanation)

findPath() throws a MemoryError because it has an infinite loop that eventually fills up memory with Point objects. (MemoryError is a subclass of Error.)

this exception is a checked exception(missing answer)

this exception is an unchecked exception(missing answer)

the exception is caught by Louis’s catch clause(missing answer)

the exception is not caught(missing answer)

the exception’s stack trace is displayed so that the problem can be debugged(missing answer)

the exception is quietly ignored(missing answer)

(missing explanation)

Part of Louis’s own code in this method throws a NullPointerException because it tries to call a method on a null reference. (NullPointerException is a subclass of RuntimeException, which is a subclass of Exception.)

this exception is a checked exception(missing answer)

this exception is an unchecked exception(missing answer)

the exception is caught by Louis’s catch clause(missing answer)

the exception is not caught(missing answer)

the exception’s stack trace is displayed so that the problem can be debugged(missing answer)

the exception is quietly ignored(missing answer)

(missing explanation)

check explain

Catch me if you can

Alyssa Hacker has a much more precise way of dealing with checked exceptions. She catches the specific exception class that the method throws, with the narrowest try-catch block possible. Here is how she calls findPath():

public void driveRobotAround() {
    ... // Alyssa's code

    try {
        path = findPath(initial, goal); // this method throws a checked PathNotFoundException
    } catch (PathNotFoundException e) { // so catch it specifically, right here
        // see questions below
    }

    ... // more of Alyssa's code
}

Which of the following exceptions would Alyssa’s catch clause catch, if findPath() happened to throw it?

IOException(missing answer)

MemoryError(missing answer)

NullPointerException(missing answer)

PathNotFoundException(missing answer)

RuntimeException(missing answer)

(missing explanation)

Which of the following lines of code might be good to include in Alyssa’s catch clause?

e.printStackTrace();(missing answer)

return;(missing answer)

throw new RobotStuckException();(missing answer)

(missing explanation)

check explain

How to declare exceptions in a specification

/**
 * @param list list of strings to convert to lower case
 * @return new list list' where list'[i] is list[i] converted to lowercase
 */
static List<String> toLowerCase(List<String> list)

static Set<Thing> allTheThings;

static void analyzeEverything() {
    analyzeThings();
}

static void analyzeThings() {
    try {
        for (Thing t : allTheThings) {
            analyzeOneThing(t);
        }
    } catch (AnalysisException ae) {
        return;
    }
}

static void analyzeOneThing(Thing t) throws AnalysisException {
    // ...
    // ... maybe go past the end of a list
    // ...
}

Before we wrap up, check your understanding with one last example:

// Requires: tiles has length 7 & contains only uppercase letters.
//           crossings contains only uppercase letters, without duplicates.
// Effects: Returns a list of words where each word can be made by taking
//          letters from tiles and at most 1 letter from crossings.
public static List<String> scrabble(String tiles, String crossings) {
    if (tiles.length() != 7) { throw new RuntimeException(); }
    return new ArrayList<>();
}

A specification acts as a crucial firewall between the implementer of a procedure and its client. It makes separate development possible: the client is free to write code that uses the procedure without seeing its source code, and the implementer is free to write the code that implements the procedure without knowing how it will be used.

Let’s review how specifications help with the main goals of this course:

• Safe from bugs. A good specification clearly documents the mutual assumptions that a client and implementer are relying on. Bugs often come from disagreements at the interfaces, and the presence of a specification reduces that. Using machine-checked language features in your spec, like static typing and exceptions rather than just a human-readable comment, can reduce bugs still more.

• Easy to understand. A short, simple spec is easier to understand than the implementation itself, and saves other people from having to read the code.

• Ready for change. Specs establish contracts between different parts of your code, allowing those parts to change independently as long as they continue to satisfy the requirements of the contract.