6.031
6.031 — Software Construction
Fall 2021

Reading 6: Specifications

Software in 6.031

Safe from bugsEasy to understandReady for change
Correct today and correct in the unknown future. Communicating clearly with future programmers, including future you. Designed to accommodate change without rewriting.

Objectives

  • Understand preconditions and postconditions in function specifications, and be able to write correct specifications
  • Be able to write tests against a specification
  • Understand how to use exceptions

Introduction

Specifications are the linchpin of teamwork. It’s impossible to delegate responsibility for implementing a function without a specification. The specification acts as a contract: the implementer is responsible for meeting the contract, and a client that uses the function 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 functions. We’ll discuss what preconditions and postconditions are, and what they mean for the implementer and the client of a function. We’ll also talk about how to use exceptions, an important language feature found not only in TypeScript, but also Python, Java, and many other modern languages, which allows us to make a function’s interface safer from bugs and easier to understand.

TypeScript Tutor exercises

Keep making progress on TypeScript by completing these categories in TypeScript Tutor:

Behavioral equivalence

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

function find(arr:Array<number>, val:number):number {
    for (let i = 0; i < arr.length; i++) {
        if (arr[i] === val) return i;
    }
    return -1;
}

This find function has many clients in the program (places where the function 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:

function find(arr:Array<number>, val:number):number {
    for (let 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 input/output 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 function, 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:

find(arr:Array<number>, val:number):number
requires:
val occurs exactly once in arr
effects:
returns index i such that arr[i] = val

reading exercises

Something’s missing

There’s a strange difference between the implementations and specification of find above. Both implementations end with return -1, but the spec never mentions -1 at all! Why?

(missing explanation)

Order matters

The find spec we just showed will let you make this implementation change safely – but only if that spec existed at the right time! Which ordering of the steps below is safest from bugs?

C: other people write clients using find
I1: you write the original forward-search find implementation
I2: you write the new forward-and-back find implementation
S: you write the spec for find shown above
T: you write a test suite for find

(missing explanation)

Behave nicely

Consider these two implementations of find, which differ not only in the direction they search through the array, but also in what they return if the search fails:

function find(arr:Array<number>, val:number):number {
    for (let i = 0; i < arr.length; i++) {
        if (arr[i] === val) return i;
    }
    return arr.length;
}
function find(arr:Array<number>, val:number):number {
    for (let i = arr.length - 1; i >= 0; i--) {
        if (arr[i] === val) return i;
    }
    return -1;
}

As we said above, suppose clients only care about calling the find function when they know val occurs exactly once in arr.

(missing explanation)

Best behavior

Now let’s change the spec.

Suppose clients now care that the find function should:

  • (if val is in arr) return some index i such that arr[i] === val
  • (otherwise) return some integer j such that j is not a valid array index.

(missing explanation)

Why specifications?

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:

find(arr:Array<number>, val:number):number
requires:
val occurs exactly once in arr
effects:
returns index i such that arr[i] = val
function find(arr:Array<number>, val:number):number {
    for (let 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 function 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 function 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 module 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.

Specification structure

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

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

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

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

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

The postcondition is an obligation on the implementer of the function. It includes the parts that TypeScript can statically check, notably the return type. 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 function is invoked, assuming the precondition was true before.

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

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

reading exercises

Logical implication

Here’s the spec we’ve been looking at:

find(arr:Array<number>, val:number):number
requires:
val occurs exactly once in arr
effects:
returns index i such that arr[i] = val

(missing explanation)

Logical implementation

(missing explanation)

Specifications in TypeScript

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.

TypeScript does not go quite so far, but its static type declarations are effectively part of the precondition and postcondition of a function, 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 function, and generally depends on human beings to check it and guarantee it.

A common convention, originally designed for Java but now also used by TypeScript and JavaScript, is to put a documentation comment before the function, in which parameters are described by @param clauses and results are described by @returns clauses. You should put the preconditions into @param where possible, and postconditions into @returns. So a specification like this:

find(arr:Array<number>, val:number):number
requires:
val occurs exactly once in arr
effects:
returns index i such that arr[i] = val

… might be rendered in TypeDoc 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
 * @returns index i such that arr[i] = val
 */
function find(arr:Array<number>, val:number):number

Documenting your specifications using this TypeDoc format allows Visual Studio Code to show you (and clients of your code) useful information, and allows you to generate HTML documentation automatically.

reading exercises

TypeDoc

Given this spec:

isPalindrome(word:string):boolean
requires:
word contains only alphanumeric characters
effects:
returns true if and only if word is a palindrome

Here is a flawed attempt to write the spec in TypeDoc:

/*
 * 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
 * @returns boolean
 */

(missing explanation)

Concise TypeDoc specs

For this spec written in TypeDoc:

/**
 * 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
 * @returns 'X' or 'O', or 'tie' if the board is a tie
 */
function endGame(board:Array<Array<'X'|'O'>>):'X'|'O'|'tie'

Identify the information contributed by each line of the spec, starting with the function signature:

(missing explanation)

(missing explanation)

(missing explanation)

(missing explanation)

Back to Python

For this spec written as a Python docstring (example adapted from a 6.0001 Hangman game):

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

Identify the information contributed by each line of the spec:

(missing explanation)

(missing explanation)

(missing explanation)

(missing explanation)

What a specification may talk about

A specification of a function can talk about the parameters and return value of the function, but it should never talk about local variables of the function or private fields of the function’s class. You should consider the implementation invisible to the reader of the spec. It’s behind the firewall as far as clients are concerned.

The source code of the function may even be unavailable to the reader of your spec, because the TypeDoc tool extracts just the spec comments from your code and renders them as HTML.

Avoid null

Many languages allow a variable to take on the special value like None or null, which means that the variable doesn’t point to an object. By default, TypeScript behaves this way, so that any variable can be null regardless of the variable’s type:

This is an unfortunate hole in the static type system, because null is not truly a legal string value. You can’t call any methods or use any properties with this reference:

word.toLowerCase() // throws TypeError
word.length        // throws TypeError

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: accessing length throws a TypeError.

Also note that an array might be non-null but contain null as a value:

let words = [ null ];

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

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

When TypeScript has strict null checking enabled (which is the 6.031 configuration), the static type checker guarantees this:

let word:string = null;  // compile error when strict null checking is on

If a function allows null or undefined values in a parameter or return value, it needs to explicitly declare null in the type (e.g. string|null). But this should be done sparingly. Avoid null.

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.)

Include emptiness

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 array [ ], 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 Nonelen(None) and None + "a" both produce errors.

The same idea translates to TypeScript. The null reference is not a valid string, or array, or map, or any other object. But the empty string "" is a valid string value, and the empty array [ ] is a valid array value.

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

reading exercises

Vacuous statements

Consider a function whose type signature is:

computeSomething(array:Array<string>):string

Which of the following preconditions on array would allow calling computeSomething([])?

(missing explanation)

Which of the following preconditions on array would allow calling computeSomething([""])?

(missing explanation)

Which of the following preconditions on array would allow calling computeSomething([null])?

(missing explanation)

Testing and specifications

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:

find(arr:Array<number>, val:number):number
requires:
val occurs in arr
effects:
returns index i such that arr[i] = 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:

let array = [7, 7, 7];
let i = find(array, 7);
assert.strictEqual(i, 0);  // bad test case: assumes too much, more than the postcondition promises
assert.strictEqual(array[i], 7);  // 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

Recall the search engine example from Testing with these functions:

/** 
 * @returns the contents of the file
 */
function load(filename:string):string { ... }

/** 
 * @returns the words in string s, in the order they appear, 
 *         where a word is a contiguous sequence of 
 *         non-whitespace and non-punctuation characters 
 */
function extract(s:string):Array<string> { ... }

/**
 * @returns an index mapping a word to the set of filenames
 *         containing that word, for all files in the input set 
 */
function index(filenames:Set<string>):Map<string, Set<string>>  { 
    ...
    for (let file of files) {
        let doc = load(file);
        let words = extract(doc);
        ...
    }
    ...
} 

We talked then about unit testing, the idea that we should write tests of each module of our program in isolation. A good unit test is focused on just a single specification. Our tests will nearly always rely on the specs of JavaScript library functions, but a unit test for one function we’ve written shouldn’t fail if a different function fails to satisfy its spec. As we saw in the example, a test for extract() shouldn’t fail if load() doesn’t satisfy its postcondition.

Good integration tests, tests that use a combination of modules, will make sure that our different functions have compatible specifications: callers and implementers of different functions are passing and returning values as the other expects. Integration tests cannot replace systematically-designed unit tests. From the example, if we only ever test extract by calling index, we will only test it on a potentially small part of its input space: inputs that are possible outputs of load. In doing so, we’ve left a place for bugs to hide, ready to jump out when we use extract for a different purpose elsewhere in our program, or when load starts returning documents written in a new format, etc.

reading exercises

gcd 1

Alice writes the following code:

function gcd(a:number, b:number):number {
    if (a > b) {
        return gcd(a-b, b);
    } else if (b > a) {
        return gcd(a, b-a);
    }
    return a;
}

Bob writes the following test:

it("tests gcd", function() {
    assert.strictEqual(gcd(24, 54), 6);
});

The test passes! But where’s the spec?

Alice should write a > 0 in the precondition of gcd

Alice should write b > 0 in the precondition of gcd

Alice should write gcd(a, b) > 0 in the precondition of gcd

Alice should write a and b are integers in the precondition of gcd

(missing explanation)

gcd 2

If Alice adds a > 0 to the precondition, Bob should test negative values of a

(missing explanation)

If Alice does not add a > 0 to the precondition, Bob should test negative values of a

(missing explanation)

Specifications for mutating functions

We discussed mutable vs. immutable objects in an earlier reading (Basic TypeScript). 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 function that mutates an object:

addAll(array1:Array<string>, array2:Array<string>):boolean
requires:
array1 and array2 are not the same object
effects:
modifies array1 by adding the elements of array2 to the end of it, and returns true if array1 changed as a result of call

First, look at the postcondition. It gives two constraints: the first telling us how array1 is modified, and the second telling us how the return value is determined.



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

If array1 and array2 are the same array, 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 array 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.

Here is another example of a mutating function:

sort(array:Array<string>):void
requires:
nothing
effects:
puts array in sorted order, i.e. array[i]array[j] for all 0 ≤ i < j < array.length

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

toLowerCase(array:Array<string>):Array<string>
requires:
nothing
effects:
returns a new array t, same length as array, where t[i] = array[i].toLowerCase()

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 “array is not modified”, but in the absence of a postcondition describing mutation, we demand no mutation of the inputs.

Exceptions

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

Since an exception is a possible output from a method, it may have to be described in the postcondition for the method. An exception can be documented with a @throws clause in the documentation comment. This section discusses when to include an exception in a specification, and when not to.

Exceptions for signaling bugs

You’ve probably already seen some exceptions in your Python or TypeScript programming so far. For example, in Python:

  • IndexError is thrown when an array index array[i] is outside the valid range for the array array
  • KeyError is thrown when a dictionary lookup dict[key] finds no matching key
  • TypeError is thrown for a variety of dynamic type errors, such as trying to call a method on None

TypeScript also has TypeError for dynamic type errors, but most dynamic errors are signaled with a generic Error class.

These kinds of exceptions generally indicate bugs – in either the client or the implementation – and the information displayed when the exception is thrown can help you find and fix the bug.

Exceptions that signal bugs are not part of the postcondition of a method, so they should not appear in @throws. For example, TypeError normally should never be mentioned in a spec. The types of the arguments are part of the precondition, which means that a valid implementation is free to throw TypeError without any warning if those types are violated (for example, if a client manages to pass a null value). So this spec, for example, never mentions TypeError:

/**
 * @param array array of strings to convert to lower case
 * @returns new array t, same length as array, 
 *         where t[i] is array[i] converted to lowercase for all valid indices i
 */
function toLowerCase(array:Array<string>):Array<string>

Exceptions for anticipated failures

Exceptions are not just for signaling bugs. They can be used to signal anticipated sources of failure, in such a way that the caller can catch them and respond to them. Exceptions that signal anticipated failures should be documented with a @throws clause, specifying the conditions under which that failure occurs. For example:

/**
 * Compute the integer square root.
 * @param x integer value to take square root of
 * @returns square root of x
 * @throws NotPerfectSquareError if x is not a perfect square
 */
function integerSquareRoot(x:number):number
/**
 * Pops a value from this queue.
 * @returns next value in the queue, and removes the value from the queue
 * @throws EmptyQueueError if this queue is empty
 */
function pop():number

reading exercises

Throw all the things!

Examine this code for analyzing some Thing objects:

const allTheThings: Set<Thing> = new Set();

function analyzeEverything():void {
    analyzeThings();
}

function analyzeThings():void {
    try {
        for (const t of allTheThings) {
            analyzeOneThing(t);
        }
    } catch (e) {
        return;
    }
}

function analyzeOneThing(t:Thing) {
    // ...
    // ... maybe throw new AnalysisError()
    // ...
}

(missing explanation)

Summary

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

reading exercises

Scrabble 1

Suppose we’re working on the function below…

/**
 * @param tiles     a string of 7 uppercase letters.
 * @param crossings contains only uppercase letters, without duplicates.
 * @returns an array of words where each word can be made by taking
 *         letters from tiles and at most 1 letter from crossings.
 */
function scrabble(tiles:string, crossings:string):Array<string> {
    if (tiles.length !== 7) { throw new Error("tiles must have length 7"); }
    return [ ];
}

(missing explanation)

(missing explanation)

Scrabble 2

(missing explanation)

(missing explanation)

A specification acts as a crucial firewall between the implementer of a module and its client. It makes separate development possible: the client is free to write code that uses the module without seeing its source code, and the implementer is free to write the code that implements the module 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.