6.031
6.031 — Software Construction
Spring 2022

Reading 11: Abstraction Functions & Rep Invariants

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

Today’s reading introduces several ideas:

  • invariants
  • representation exposure
  • abstraction functions
  • representation invariants

In this reading, we study a more formal mathematical idea of what it means for a class to implement an ADT, via the notions of abstraction functions and rep invariants. These mathematical notions are eminently practical in software design. The abstraction function will give us a way to cleanly define the equality operation on an abstract data type (which we’ll discuss in more depth in a future class). The rep invariant will make it easier to catch bugs caused by a corrupted data structure.

Invariants

Resuming our discussion of what makes a good abstract data type, the final, and perhaps most important, property of a good abstract data type is that it preserves its own invariants. An invariant is a property of a program that is always true, for every possible runtime state of the program. Immutability is one crucial invariant that we’ve already encountered: once created, an immutable object should always represent the same value, for its entire lifetime. But there are many other kinds of invariants, including types of variables (i: number means that i is always a number), or relationships between variables (e.g. when i is used to loop over the indices of an array, then 0 <= i < array.length is an invariant within the body of the loop).

Saying that the ADT preserves its own invariants means that the ADT is responsible for ensuring that its own invariants hold. This is done by hiding or protecting the variables involved in the invariants (e.g., using language features like private), and allowing access only through operations with well-defined contracts.

When an ADT preserves its own invariants, reasoning about the code becomes much easier. If you can count on the fact that strings are immutable, for example, then you can rule out the possibility that a string has been mutated when you’re debugging code that uses strings – or when you’re trying to establish an invariant for another ADT that uses strings. Contrast that with a mutable string type, which can be mutated by any code that has access to it. To reason about a bug or invariant involving a mutable string, you’d have to check all the places in the code where the string might be accessible.

reading exercises

Statically-checked invariants

We’re already accustomed to declaring some useful invariants. Consider this line of code:

const names: Array<string> = ["Huey", "Dewey", "Louie"];

Which of the following are invariants expressed by this code?

(missing explanation)

Immutability

Later in this reading, we’ll see many interesting invariants. Let’s focus on immutability for now. Here’s a specific example:

/**
 * This immutable data type represents a tweet from Twitter.
 */
class Tweet {

    public author: string;
    public text: string;
    public timestamp: Date;

    /**
     * Make a Tweet.
     * @param author    Twitter user who wrote the tweet
     * @param text      text of the tweet
     * @param timestamp date/time when the tweet was sent
     */
    public constructor(author: string, text: string, timestamp: Date) {
        this.author = author;
        this.text = text;
        this.timestamp = timestamp;
    }
}

How do we guarantee that these Tweet objects are immutable – that, once a tweet is created, its author, message, and date can never be changed?

The first threat to immutability comes from the fact that clients can — in fact must — directly access its fields. So nothing’s stopping us from writing code like this:

let t: Tweet = new Tweet("justinbieber",
                    "Thanks to all those beliebers out there inspiring me every day",
                    new Date());
t.author = "rbmllr";

This is a trivial example of representation exposure, meaning that code outside the class can modify the representation directly. Rep exposure like this threatens not only invariants, but also representation independence. We can’t change the implementation of Tweet without affecting all the clients who are directly accessing those fields.

Fortunately, TypeScript gives us language mechanisms to deal with this kind of rep exposure:

class Tweet {

    private readonly author: string;
    private readonly text: string;
    private readonly timestamp: Date;

    public constructor(author: string, text: string, timestamp: Date) {
        this.author = author;
        this.text = text;
        this.timestamp = timestamp;
    }

    /**
     * @returns Twitter user who wrote the tweet
     */
    public getAuthor(): string {
        return this.author;
    }

    /**
     * @returns text of the tweet
     */
    public getText(): string {
        return this.text;
    }

    /**
     * @returns date/time when the tweet was sent
     */
    public getTimestamp(): Date {
        return this.timestamp;
    }

}

The private and public keywords indicate which fields and methods are accessible only within the class and which can be accessed from outside the class. The readonly keyword also helps by guaranteeing that the fields of this immutable type won’t be reassigned after the object is constructed.

But that’s not the end of the story: the rep is still exposed! Consider this perfectly reasonable client code that uses Tweet:

/**
 * @returns a tweet that retweets t, one hour later
 */
function retweetLater(t: Tweet): Tweet {
    const d: Date = t.getTimestamp();
    d.setHours(d.getHours()+1);
    return new Tweet("rbmllr", t.getText(), d);
}

retweetLater takes a tweet and should return another tweet with the same message (called a retweet) but sent an hour later. The retweetLater method might be part of a system that automatically echoes funny things that Twitter celebrities say.

What’s the problem here? The getTimestamp call returns a reference to the same Date object referenced by tweet t. t.timestamp and d are aliases to the same mutable object. So when that date object is mutated by d.setHours(), this affects the date in t as well, as shown in the snapshot diagram.

Tweet’s immutability invariant has been broken. The problem is that Tweet leaked out a reference to a mutable object that its immutability depended on. We exposed the rep, in such a way that Tweet can no longer guarantee that its objects are immutable. Perfectly reasonable client code created a subtle bug.

We can patch this kind of rep exposure by using defensive copying: making a copy of a mutable object to avoid leaking out references to the rep. Here’s the code:

public getTimestamp(): Date {
    return new Date(this.timestamp.getTime());
}

Mutable types often have a copy constructor that allows you to make a new instance that duplicates the value of an existing instance. In this case, Date’s copy constructor uses the timestamp value, measured in milliseconds since January 1, 1970. As another example, Map’s copy constructor takes an array of key-value pairs, which can be extracted from the map you want to copy by calling entries().

So we’ve done some defensive copying in the return value of getTimestamp. But we’re not done yet! There’s still rep exposure. Consider this (again perfectly reasonable) client code:

/**
 * @returns an array of 24 inspiring tweets, one per hour today
 */
function tweetEveryHourToday(): Array<Tweet> {
    const array: Array<Tweet> = [];
    const date: Date = new Date();
    for (let i = 0; i < 24; i++) {
        date.setHours(i);
        array.push(new Tweet("rbmllr", "keep it up! you can do it", date));
    }
    return array;
}

This code intends to advance a single Date object through the 24 hours of a day, creating a tweet for every hour. But notice that the constructor of Tweet saves the reference that was passed in, so all 24 Tweet objects end up with the same time, as shown in this snapshot diagram.

Again, the immutability of Tweet has been violated. We can fix this problem, too, by using judicious defensive copying, this time in the constructor:

public constructor(author: string, text: string, timestamp: Date) {
    this.author = author;
    this.text = text;
    this.timestamp = new Date(timestamp.getTime());
}

In general, you should carefully inspect the argument types and return types of all your ADT operations. If any of the types are mutable, make sure your implementation doesn’t return direct references to its representation. Returning a reference to a mutable rep object causes rep exposure.

You may object that this seems wasteful. Why make all these copies of dates? Why can’t we just solve this problem by a carefully written specification, like this?

/**
 * Make a Tweet.
 * @param author    Twitter user who wrote the tweet
 * @param text      text of the tweet
 * @param timestamp date/time when the tweet was sent. Caller must never
 *                   mutate this Date object again!
 */
public constructor(author: string, text: string, timestamp: Date) {

This approach is sometimes taken when there isn’t any other reasonable alternative – for example, when the mutable object is too large to copy efficiently. But the cost in your ability to reason about the program, and your ability to avoid bugs, is enormous. In the absence of compelling arguments to the contrary, it’s almost always worth it for an abstract data type to guarantee its own invariants, and preventing rep exposure is essential to that.

An even better solution is to prefer immutable types. If Date were an immutable type, then we would have ended this section after talking about public and private. No further rep exposure would have been possible.

reading exercises

Rep exposure

Consider the following problematic data type:

      /** Represents an immutable right triangle. */
      class RightTriangle {
/*A*/     private sides: Array<number>;

/*B*/     public readonly hypotenuse: number;

          /**
           * Make a right triangle.
           * @param legA, legB  the two legs of the triangle
           * @param hypotenuse  the hypotenuse of the triangle,
*C*        *           requires hypotenuse^2 = legA^2 + legB^2
           *           (within the error tolerance of double arithmetic)
           */
          public constructor(legA: number, legB: number, hypotenuse: number) {
/*D*/         this.sides = [ legA, legB ];
/*D*/         this.hypotenuse = hypotenuse;
          }

          /**
           * Get the two sides of the right triangle.
           * @returns two-element array with the triangle's side lengths
           */
          public getAllSides(): Array<number> {
/*E*/         return this.sides;
          }

          /**
           * @param factor to multiply the sides by
           * @returns a triangle made from this triangle by
           * multiplying all side lengths by factor.
           */
          public scale(factor: number): RightTriangle {
              return new RightTriangle(this.sides[0]*factor, this.sides[1]*factor, this.hypotenuse*factor);
          }

          /**
           * @returns a regular triangle made from this triangle.
           * A regular right triangle is one in which
           * both legs have the same length.
           */
          public regularize(): RightTriangle {
              const bigLeg: number = Math.max(this.sides[0], this.sides[1]);
              return new RightTriangle(bigLeg, bigLeg, this.hypotenuse);
          }

      }

(missing explanation)

(missing explanation)

(missing explanation)

(missing explanation)

(missing explanation)

Sign here

Suppose you want to build a version of TypeScript where users can choose to only use classes that have been cryptographically signed by identities they trust. You want each class to manage its own array of signatures, so you provide the operation:

public getSigners(): Array<Identity>

and implement it by simply returning a reference to your private Array<Identity> field of identities whose signatures you’ve all checked and validated.

Which bugs do you have?

(missing explanation)

Rep invariant and abstraction function

We now take a deeper look at the theory underlying abstract data types. This theory is not only elegant and interesting in its own right; it also has immediate practical application to the design and implementation of abstract types. If you understand the theory deeply, you’ll be able to build better abstract types, and will be less likely to fall into subtle traps.

In thinking about an abstract type, it helps to consider the relationship between two spaces of values.

The space of abstract values consists of the values that the type is designed to support, from the client’s point of view. For example, an abstract type for unbounded integers, like TypeScript’s BigInt, would have the mathematical integers as its abstract value space.

The space of representation values (or rep values for short) consists of the objects that actually implement the abstract values. For example, a BigInt value might be implemented using an array of digits, represented as number values. The rep space would then be the set of all such arrays.

In simple cases, an abstract type will be implemented as a single object, but more commonly a small network of objects is needed. For example, a rep value for Array might possibly be a linked list, a group of objects linked together by next and previous pointers. So a rep value is not necessarily a single object, but often something rather complicated.

Now of course the implementer of the abstract type must be interested in the representation values, since it is the implementer’s job to achieve the illusion of the abstract value space using the rep value space.

Suppose, for example, that we choose to use a string to represent a set of characters:

class CharSet {
    private s: string;
    ...
}
the abstract space and rep space of CharSet

Then the rep space R contains strings, and the abstract space A is mathematical sets of characters. We can show the two value spaces graphically, with an arrow from a rep value to the abstract value it represents. There are several things to note about this picture:

  • Every abstract value is mapped to by some rep value. The purpose of implementing the abstract type is to support operations on abstract values. Presumably, then, we will need to be able to create and manipulate all possible abstract values, and they must therefore be representable.
  • Some abstract values are mapped to by more than one rep value. This happens because the representation isn’t a tight encoding. There’s more than one way to represent an unordered set of characters as a string.
  • Not all rep values are mapped. In this case, the string “abbc” is not mapped, because we have decided that the rep string should not contain duplicates. This will allow us to terminate the remove method when we hit the first instance of a particular character, since we know there can be at most one.

In practice, we can only illustrate a few elements of the two spaces and their relationships; the graph as a whole is infinite. So we describe it by giving two things:

1. An abstraction function that maps rep values to the abstract values they represent:

AF : R → A

The arrows in the diagram show the abstraction function. In the terminology of functions, the properties we discussed above can be expressed by saying that the function is surjective (also called onto), not necessarily injective (one-to-one) and therefore not necessarily bijective, and often partial.

2. A rep invariant that maps rep values to booleans:

RI : R → boolean

For a rep value r, RI(r) is true if and only if r is mapped by AF. In other words, RI tells us whether a given rep value is well-formed. Alternatively, you can think of RI as a set: it’s the subset of rep values on which AF is defined.

the abstract space and rep space of CharSet using the NoRepeatsRep

For example, the diagram at the right showing a rep for CharSet that forbids repeated characters, RI(“a”) = true, RI(“ac”) = true, and RI(“acb”) = true, but RI(“aa”) = false and RI(“abbc”) = false. Rep values that obey the rep invariant are shown in the green part of the R space, and must map to an abstract value in the A space. Rep values that violate the rep invariant are shown in the red zone, and have no equivalent abstract value in the A space.

Both the rep invariant and the abstraction function should be documented in the code, right next to the declaration of the rep itself:

class CharSet {
    private s: string;
    // Rep invariant:
    //   s contains no repeated characters
    // Abstraction function:
    //   AF(s) = {s[i] | 0 <= i < s.length}
    ...
}

A common confusion about abstraction functions and rep invariants is that they are determined by the choice of rep and abstract value spaces, or even by the abstract value space alone. If this were the case, they would be of little use, since they would be saying something redundant that’s already available elsewhere.

The abstract value space alone doesn’t determine AF or RI: there can be several representations for the same abstract type. A set of characters could equally be represented as a string, as above, or as a bit vector, with one bit for each possible character. Clearly we need two different abstraction functions to map these two different rep value spaces.

It’s less obvious why the choice of both spaces doesn’t determine AF and RI. The key point is that defining a type for the rep, and thus choosing the values for the space of rep values, does not determine which of the rep values will be deemed to be legal, and of those that are legal, how they will be interpreted. Rather than deciding, as we did above, that the strings have no duplicates, we could instead allow duplicates, but at the same time require that the characters be sorted, appearing in nondecreasing order. This would allow us to perform a binary search on the string and thus check membership in logarithmic rather than linear time. Same rep value space – different rep invariant:

the abstract space and rep space of CharSet using the SortedRep
class CharSet {
    private s: string;
    // Rep invariant:
    //   s[0] <= s[1] <= ... <= s[s.length-1]
    // Abstraction function:
    //   AF(s) = {s[i] | 0 <= i < s.length}
    ...
}

Even with the same type for the rep value space and the same rep invariant, we might still interpret the rep differently by using different abstraction functions. Suppose the rep invariant admits any string of characters. Then we could define the abstraction function, as above, to interpret the array’s elements as the elements of the set. But there’s no a priori reason to let the rep decide the interpretation. Perhaps we’ll interpret consecutive pairs of characters as subranges, so that the string rep "acgg" is interpreted as two range pairs, [a-c] and [g-g], and therefore represents the set {a,b,c,g}. Here’s what the AF and RI would look like for that representation:

the abstract space and rep space of CharSet using the SortedRangeRep
class CharSet {
    private String s;
    // Rep invariant:
    //   s.length is even
    //   s[0] <= s[1] <= ... <= s[s.length-1]
    // Abstraction function:
    //   AF(s) = union of { c | s[2i] <= c <= s[2i+1] }
    //           for all 0 <= i < s.length/2
    ...
}

The essential point is that implementing an abstract type means not only choosing the two spaces – the abstract value space for the specification and the rep value space for the implementation – but also deciding which rep values are legal, and how to interpret them as abstract values.

It’s critically important to write down these assumptions in your code, as we’ve done above, so that future programmers (and your future self) are aware of what the representation actually means. Why? What happens if different implementers disagree about the meaning of the rep?

You can look at example code for three different CharSet implementations.

reading exercises

Exploring a rep

Consider the last rep for CharSet proposed above:

class CharSet {
    private s: string;
    // Rep invariant:
    //   s.length is even
    //   s[0] <= s[1] <= ... <= s[s.length-1]
    // Abstraction function:
    //   AF(s) = union of { c | s[2i] <= c <= s[2i+1] }
    //           for all 0 <= i < s.length/2
    ...
}

(missing explanation)

(missing explanation)

(missing explanation)

Who knows what?

(missing explanation)

(missing explanation)

Rep invariant pieces

Suppose C is an abstract data type whose representation has two string fields:

class C {
    private s: string;
    private t: string;
    ...
}

(missing explanation)

Trying to implement without an AF/RI

Suppose Louis Reasoner has created CharSet with the following rep:

class CharSet {
    private s: string;
    ...
}

But Louis unfortunately neglects to write down the abstraction function (AF) and rep invariant (RI). Here are four possible AF/RI pairs that might have been what Louis had in mind. All of them were also mentioned in the reading above.

SortedRep:

// AF(s) = {s[i] | 0 <= i < s.length}
// RI: s[0] < s[1] < ... < s[s.length-1]

SortedRangeRep:

// AF(s) = union of { c | s[2i] <= c <= s[2i+1] }
//         for all 0 <= i < s.length/2
// RI: s.length is even, and s[0] <= s[1] <= ... <= s[s.length-1]

NoRepeatsRep:

// AF(s) = {s[i] | 0 <= i < s.length}
// RI: s contains no character more than once

AnyRep:

// AF(s) = {s[i] | 0 <= i < s.length}
// RI: true

Louis has three teammates helping him implement CharSet, each working on a different operation: add(), remove(), and contains(). Each teammate might have their own idea about what the AF/RI should be.

/**
 * Modifies this set by adding c to the set.
 * @param c character to add; required to be one-character string.
 */
public add(c: string): void {
    s = s + c;
}

(missing explanation)

Trying to implement without an AF/RI #2
/**
 * Modifies this set by removing c, if found.
 * If c is not found in the set, has no effect.
 * @param c character to remove; required to be one-character string.
 */
public remove(c: string): void {
    const position = s.indexOf(c);
    if (position >= 0) {
        s = s.substring(0, position) + s.substring(position+1, s.length);
    }
}

(missing explanation)

Trying to implement without an AF/RI #3
/**
 * Test for membership.
 * @param c a one-character string.
 * @returns true iff this set contains c
 */
public contains(c: string): boolean {
    for (let i = 0; i < this.s.length; i += 2) {
        const low: string = this.s.charAt(i);
        const high: string = this.s.charAt(i+1);
        if (low <= c && c <= high) {
            return true;
        }
    }
    return false;
}

(missing explanation)

the abstraction function and rep invariant of RatNum

Example: rational numbers

Here’s an example of an abstract data type for arbitrary-precision rational numbers, implemented using BigInt in the rep. Look closely at its rep invariant and abstraction function. It would be completely reasonable to design another implementation of this same ADT with a more permissive RI. With such a change, some operations might become more expensive to perform, and others cheaper.

class RatNum {

    private readonly numerator: bigint;
    private readonly denominator: bigint;

    // Rep invariant:
    //   denominator > 0
    //   numerator/denominator is in reduced form,
    //       i.e. gcd(|numerator|,denominator) = 1

    // Abstraction function:
    //   AF(numerator, denominator) = numerator/denominator

    /**
     * Make a new RatNum = (n / d).
     * @param n numerator
     * @param d denominator
     * @throws Error if d = 0
     */
    public constructor(n: bigint, d: bigint) {
        // reduce ratio to lowest terms
        const g = gcd(BigInt(n), BigInt(d));
        const reducedNumerator = n / g;
        const reducedDenominator = d / g;

        // make denominator positive
        if (d < 0n) {
            this.numerator = -reducedNumerator;
            this.denominator = -reducedDenominator;
        } else if (d > 0n) {
            this.numerator = reducedNumerator;
            this.denominator = reducedDenominator;
        } else {
            throw new Error('denominator is zero');
        }
        this.checkRep();
    }

}

reading exercises

RatNum

Looking at the code above, and the abstraction function diagram next to it, which line of the rep is most responsible for each of these features of the abstraction function diagram?

(numerator=1, denominator=-2) appears in the red zone of R

(missing explanation)

(numerator=2, denominator=4) appears in the red zone of R

(missing explanation)

an arrow goes from (numerator=-1, denominator=2) to -1/2

(missing explanation)

Checking the rep invariant

The rep invariant isn’t just a neat mathematical idea. If your implementation asserts the rep invariant at run time, then you can catch bugs early. Here’s a method for RatNum that tests its rep invariant:

// Check that the rep invariant is true
private checkRep(): void {
    assert(this.denominator > 0n);
    assert(gcd(abs(this.numerator), this.denominator) === 1n);
}

(Note that bigint literals are integers suffixed with n.)

You should certainly call checkRep() to assert the rep invariant at the end of every operation that creates or mutates the rep – in other words, creators, producers, and mutators. Look back at the RatNum code above, and you’ll see that it calls checkRep() at the end of the constructor.

Observer methods don’t normally need to call checkRep(), but it’s good defensive practice to do so anyway. Why? Calling checkRep() in every method, including observers, means you’ll be more likely to catch rep invariant violations caused by rep exposure.

Why is checkRep private? Who should be responsible for checking and enforcing a rep invariant – clients, or the implementation itself?

reading exercises

Checking the rep invariant

(missing explanation)

No null values in the rep

Recall from the Specifications reading that null and undefined values are troublesome and unsafe, so much so that we try to remove them from our programming entirely. Preconditions and postconditions implicitly require that objects be non-null. Turning on strict null-checking in TypeScript enforces this with static type checking.

We extend that prohibition to the reps of abstract data types. The rep invariant implicitly includes x !== null and x !== undefined for every reference x in the rep, including references inside arrays, maps, etc. So if your rep is:

class CharSet {
    s: string;
}

then its rep invariant automatically includes s !== null && s !== undefined, and you don’t need to state that in a rep invariant comment. And if you have strict null checking enabled (which is the 6.031 TypeScript configuration), the static type checker guarantees it.

If some field in the rep is allowed to be null, then its type should say so explicitly. A union type like string|undefined is an example of how to do that. But think twice before designing a rep like this, because allowing null and undefined to leak into your code leads to headaches down the road.

reading exercises

Null check?

Consider this rep for some ADT named Thing:

class Thing {
    private i: number;
    private s: string;
    ...
}

The rep is accompanied by one of the rep invariants below. For each proposed rep invariant, translate it into a minimum set of assertions that you would need to place into checkRep() to check that rep invariant.

Assume that strict null-checking is enabled.

// Rep invariant:
//    i is positive

private void checkRep() {
}

(missing explanation)

// Rep invariant:
//    the length of s is even

private void checkRep() {
}

(missing explanation)

Beneficent mutation

Recall that a type is immutable if and only if a value of the type never changes after being created. With our new understanding of the abstract space A and rep space R, we can refine this definition: the abstract value should never change. But the implementation is free to mutate a rep value as long as it continues to map to the same abstract value, so that the change is invisible to the client. This kind of change is called beneficent mutation.

Here’s a simple example using an alternative rep for the RatNum type we saw earlier. This rep has a weaker rep invariant that doesn’t require the numerator and denominator to be stored in lowest terms:

class RatNum {

    private numerator: bigint;
    private denominator: bigint;

    // Rep invariant:
    //   denominator != 0

    // Abstraction function:
    //   AF(numerator, denominator) = numerator/denominator

    /**
     * Make a new RatNum = (n / d).
     * @param n numerator
     * @param d denominator
     * @throws Error if d = 0
     */
    public constructor(n: bigint, d: bigint) {
        if (d === 0n) throw new Error("denominator is zero");
        this.numerator = n;
        this.denominator = d;
        checkRep();
    }

    ...
}

This weaker rep invariant allows a sequence of RatNum arithmetic operations to simply omit reducing the result to lowest terms. But when it’s time to display a result to a human, we first simplify it:

    /**
     * @returns a string representation of this rational number
     */
    public toString(): string {
        const g = gcd(this.numerator, this.denominator);
        this.numerator /= g;
        this.denominator /= g;
        if (this.denominator < 0n) {
            this.numerator = -this.numerator;
            this.denominator = -this.denominator;
        }
        checkRep();
        return (this.denominator > 1n) ? (this.numerator + "/" + this.denominator)
                                 : (this.numerator + "");
    }

Notice that this toString implementation reassigns the private fields numerator and denominator, mutating the representation – even though it is an observer method on an immutable type! But, crucially, the mutation doesn’t change the abstract value. Dividing both numerator and denominator by the same common factor, or multiplying both by -1, has no effect on the result of the abstraction function, AF(numerator, denominator) = numerator/denominator. Another way of thinking about it is that the AF is a many-to-one function, and the rep value has changed to another that still maps to the same abstract value. So the mutation is harmless, or beneficent.

We’ll see other examples of beneficent mutation in future readings. This kind of implementer freedom often permits performance improvements like caching, data structure rebalancing, and lazy cleanup.

Documenting the AF, RI, and safety from rep exposure

It’s good practice to document the abstraction function and rep invariant in the class, using comments right where the private fields of the rep are declared. We’ve been doing that above.

When you describe the rep invariant and abstraction function, you must be precise.

It is not enough for the RI to be a generic statement like “all fields are valid.” The job of the rep invariant is to explain precisely what makes the field values valid or not.

As a function, if we take the documented RI and substitute in actual field values, legal or not, we should obtain a boolean result. Note that if we’re tempted to refer to the abstract value in our RI, we’ve put the cart before the horse: illegal rep values don’t have an abstract value, and we need to reject them in the RI by talking about the rep values alone.

It is not enough for the AF to offer a generic explanation like “represents a set of characters.” The job of the abstraction function is to define precisely how the concrete field values are interpreted.

As a function, if we take the documented AF and substitute in actual legal field values, we should obtain out a complete description of the single abstract value they represent. For example, for the CharSet abstraction function AF(s) = {s[i] | 0 <= i < s.length}, we can substitute a specific (legal) rep value like s="abbc", and get:
AF("abbc") = { "abbc"[i] | 0 <= i < "abbc".length } = { 'a', 'b', 'c' }.

But if we instead had a vague and ill-defined abstraction function like AF(s) = a set of characters, then substituting for s would not affect the righthand side at all. This definition does not say precisely which abstract set of characters corresponds to the rep value s="abbc".

Another piece of documentation that 6.031 asks you to write is a rep exposure safety argument. This is a comment that examines each part of the rep, looks at the code that handles that part of the rep (particularly with respect to parameters and return values from clients, because that is where rep exposure occurs), and presents a reason why the code doesn’t expose the rep.

Here’s an example of Tweet with its rep invariant, abstraction function, and safety from rep exposure fully documented:

// Immutable type representing a tweet.
class Tweet {

    private readonly author: string;
    private readonly text: string;
    private readonly timestamp: Date;

    // Rep invariant:
    //   author is a Twitter username (a nonempty string of letters, digits, underscores)
    //   text.length <= 280
    // Abstraction function:
    //   AF(author, text, timestamp) = a tweet posted by author, with content text,
    //                                 at time timestamp
    // Safety from rep exposure:
    //   All fields are private;
    //   author and text are Strings, so are guaranteed immutable;
    //   timestamp is a mutable Date, so Tweet() constructor and getTimestamp()
    //        make defensive copies to avoid sharing the rep's Date object with clients.

    // Operations (specs and method bodies omitted to save space)
    public constructor(author: string, text: string, timestamp: Date) { ... }
    public getAuthor(): string { ... }
    public getText(): string { ... }
    public getTimestamp(): Date { ... }
}

Notice that we don’t have any explicit rep invariant conditions on timestamp (aside from the conventional assumption that timestamp is not null, which we have for all object references). But we still need to include timestamp in the rep exposure safety argument, because the immutability property of the whole type depends on all the fields remaining unchanged.

Compare the argument above with an example of a broken argument involving mutable Date objects.

Here are the arguments for RatNum.

// Immutable type representing a rational number.
class RatNum {
    private readonly numerator: bigint;
    private readonly denominator: bigint;

    // Rep invariant:
    //   denominator > 0
    //   numerator/denominator is in reduced form, i.e. gcd(|numerator|,denominator) = 1
    // Abstraction function:
    //   AF(numerator, denominator) = numerator/denominator
    // Safety from rep exposure:
    //   All fields are private, and all types in the rep are immutable.

    // Operations (specs and method bodies omitted to save space)
    public constructor(n: bigint, d: bigint) { ... }
    ...
}

Notice that an immutable rep is particularly easy to argue for safety from rep exposure.

You can look at the full code for RatNum.

reading exercises

Arguing against rep exposure

Consider the following ADT:

// Mutable type representing Twitter users' followers.
class FollowGraph {
    private readonly followersOf: Map<string,Set<string>>;

    // Rep invariant:
    //    all strings in followersOf are Twitter usernames
    //           (i.e., nonempty strings of letters, digits, underscores)
    //    no user follows themselves, i.e. x is not in followersOf.get(x)
    // Abstraction function:
    //    AF(followersOf) = the follower graph where Twitter user x is followed by user y
    //                      if and only if followersOf.get(x).has(y)
    // Safety from rep exposure:
    //    All fields are private, and ..???..

    // Operations (specs and method bodies omitted to save space)
    public constructor() { ... }
    public addFollower(user: string, follower: string): void { ... }
    public removeFollower(user: string, follower: string): void { ... }
    public getFollowers(user: string): Set<string> { ... }
}

For each statement below: assuming the omitted method bodies are consistent with the statement, can we use the statement in place of ..???.. to make a complete and persuasive safety-from-rep-exposure comment?

1. “Strings are immutable.”

(missing explanation)

2.followersOf is a mutable Map containing mutable Set objects, but getFollowers() makes a defensive copy of the Set it returns, and all other parameters and return values are immutable string or void.”

(missing explanation)

3. “This class is mutable, so rep exposure isn’t an issue.”

(missing explanation)

4.followersOf is a mutable Map, but it is never passed or returned from an operation.”

(missing explanation)

5.FollowGraph() does not expose the rep; addFollower() does not expose the rep; removeFollower() does not expose the rep; getFollowers() does not expose the rep.”

(missing explanation)

6.string is immutable. The Set type in the rep is mutable, and the same type is returned by getFollowers(), but that return value is a fresh defensive copy, not a reference to any set stored in the rep. The Map type in the rep is mutable, but that type is never passed or returned from an operation.”

(missing explanation)

What an ADT specification may talk about

Since we’ve just discussed where to document the rep invariant and abstraction function, now is a good moment to update our notion of what a specification may talk about.

The specification of an abstract type T – which consists of the specs of its operations – should only talk about things that are visible to the client. This includes parameters, return values, and exceptions thrown by its operations. Whenever the spec needs to refer to a value of type T, it should describe the value as an abstract value, i.e. mathematical values in the abstract space A.

The spec should not talk about details of the representation, or elements of the rep space R. It should consider the rep itself (the private fields) invisible to the client, just as method bodies and their local variables are considered invisible. That’s why we write the rep invariant and abstraction function as ordinary comments within the body of the class, rather than TypeDoc comments above the class. Writing them as TypeDoc comments would commit to them as public parts of the type’s specification, which would interfere with rep independence and information hiding.

ADT invariants replace preconditions

Now let’s bring a lot of pieces together. An enormous advantage of a well-designed abstract data type is that it encapsulates and enforces properties that we would otherwise have to stipulate in a precondition. For example, instead of a spec like this, with an elaborate precondition:

/**
 * @param set1 is a sorted set of characters with no repeats
 * @param set2 is likewise
 * @returns characters that appear in one set but not the other,
 *  in sorted order with no repeats
 */
static exclusiveOr(set1: string, set2: string): string;

We might instead use an ADT that captures the desired property:

/**
 * @returns characters that appear in one set but not the other
 */
static exclusiveOr(set1: SortedCharSet, set2: SortedCharSet): SortedCharSet;

This hits all our targets:

  • it’s safer from bugs, because the required condition (sorted with no repeats) can be enforced in exactly one place, the SortedCharSet type, and because static checking comes into play, preventing values that don’t satisfy this condition from being used at all, with an error at compile-time.

  • it’s easier to understand, because it’s much simpler, and the name SortedCharSet conveys what the programmer needs to know.

  • it’s more ready for change, because the representation of SortedCharSet can now be changed without changing exclusiveOr or any of its clients.

Many of the places where we used preconditions on the early problem sets in this course would have benefited from a custom ADT instead.

reading exercises

Encapsulating preconditions in ADTs

Consider this function:

/**
 * Find tweets written by a particular user.
 *
 * @param tweets an array of tweets with distinct timestamps, not modified by this function.
 * @param username Twitter username (a nonempty sequence of letters, digits, and underscores)
 * @returns all and only the tweets in the array whose author is username,
 *         in the same order as in the input array.
 */
function writtenBy(tweets: Array<Tweet>, username: string): Array<Tweet> { ... }

(missing explanation)

How to establish invariants

An invariant is a property that is true for the entire program – which in the case of an invariant about an object, reduces to the entire lifetime of the object.

To make an invariant hold, we need to:

  • make the invariant true in the initial state of the object; and
  • ensure that all changes to the object keep the invariant true.

Translating this in terms of the types of ADT operations, this means:

  • creators and producers must establish the invariant for new object instances; and
  • mutators, observers, and producers must preserve the invariant for existing object instances.

The risk of rep exposure makes the situation more complicated. If the rep is exposed, then the object might be changed anywhere in the program, not just in the ADT’s operations, and we can’t guarantee that the invariant still holds after those arbitrary changes.

So the full rule for proving invariants is as follows:

If an invariant of an abstract data type is

  1. established by creators and producers;
  2. preserved by mutators, observers, and producers; and
  3. no representation exposure occurs,

then the invariant is true of all instances of the abstract data type.

This rule applies structural induction over the abstract data type.

reading exercises

Structural induction

Recall this data type from the first exercise in this reading, now with a different rep (and new bugs):

/** Represents an immutable right triangle. */
class RightTriangle {
    private sides: number[];

    // Rep invariant:
    //   sides.length = 3
    //   sides[i] > 0 for all i
    //   sides[0]^2 + sides[1]^2 = sides[2]^2 (within the error tolerance of double arithmetic)

    // Abstraction function:
    //   AF(sides) = the right triangle with legs sides[0] and sides[1], and hypotenuse sides[2]


    /**
     * Make a right triangle.
     * @param legA, legB  the two legs of the triangle, must be positive
     * @param hypotenuse  the hypotenuse of the triangle, also positive,
     *           requires hypotenuse^2 = legA^2 + legB^2
     *           (within the error tolerance of double arithmetic)
     */
    public constructor(legA: number, legB: number, hypotenuse: number) {
        this.sides = new Array<number>(legA, legB, hypotenuse);
    }

    /**
     * Get all the sides of the triangle.
     * @returns three-element array with the triangle's side lengths
     */
    public getAllSides(): Array<number> {
        return this.sides;
    }

    /**
     * @returns length of the triangle's hypotenuse
     */
    public getHypotenuse(): number {
        return this.sides[2];
    }

    /**
     * @param factor to multiply the sides by, must be >0
     * @returns a triangle made from this triangle by
     * multiplying all side lengths by factor.
     */
    public scale(factor: number): RightTriangle {
        return new RightTriangle(this.sides[0]*factor, this.sides[1]*factor, this.sides[2]*factor);
    }

    /**
     * @returns a regular triangle made from this triangle.
     * A regular right triangle is one in which
     * both legs have the same length.
     */
    public regularize(): RightTriangle {
        const bigLeg: number = Math.max(this.sides[0], this.sides[1]);
        return new RightTriangle(bigLeg, bigLeg, this.sides[2]);
    }

}

This data type has an important invariant: the relationship between the legs and hypotenuse, as stated in the Pythagorean theorem.

(missing explanation)

(missing explanation)

(missing explanation)

(missing explanation)

(missing explanation)

Recipes for programming

Abstract data types are at the heart of software construction for correctness, clarity, and changeability.

Recall the test-first programming approach for:

Writing a method

  1. Spec. Write the spec, including the method signature (name, argument types, return types, exceptions), and the precondition and the postcondition as a documentation comment.
  2. Test. Create systematic test cases and put them in test file so you can run them automatically.
    1. You may have to go back and change your spec when you start to write test cases. Just the process of writing test cases puts pressure on your spec, because you’re thinking about how a client would call the method. So steps 1 and 2 iterate until you’ve got a better spec and some good test cases.
    2. Make sure at least some of your tests are failing at first. A test suite that passes all tests even when you haven’t implemented the method is not a good test suite for finding bugs.
  3. Implement. Write the body of the method. You’re done when the tests are all passing.
    1. Implementing the method puts pressure on both the tests and the specs, and you may find bugs that you have to go back and fix. So finishing the method may require changing the implementation, the tests, and the specs, and bouncing back and forth among them.

Let’s broaden this to a recipe for:

Writing an abstract data type

  1. Spec. Write specs for the operations of the data type, including method signatures, preconditions, and postconditions.
  2. Test. Write test cases for the ADT’s operations.
    1. Again, this puts pressure on the spec. You may discover that you need operations you hadn’t anticipated, so you’ll have to add them to the spec.
  3. Implement. For an ADT, this part expands to:
    1. Choose rep. Write down the private fields of a class (or, as we’ll see in future readings, choose and define a different kind of rep). Write down the rep invariant and abstraction function as a comment.
    2. Assert rep invariant. Implement a checkRep() method that enforces the rep invariant. This is critically important if the rep invariant is nontrivial, because it will catch bugs much earlier.
    3. Implement operations. Write the method bodies of the operations, making sure to call checkRep() in them. You’re done when the tests are all passing.

And let’s broaden it further to a recipe for:

Writing a program

(consisting of ADTs and functions)

  1. Choose data types. Decide which ones will be mutable and which immutable.
  2. Choose functions. Write your top-level main function and break it down into smaller steps.
  3. Spec. Spec out the ADTs and functions. Keep the ADT operations simple and few at first. Only add complex operations as you need them.
  4. Test. Write test cases for each unit (ADT or function).
  5. Implement simply first. Choose simple, brute-force representations. The point here is to put pressure on the specs and the tests, and try to pull your whole program together as soon as possible. Make the whole program work correctly first. Skip the advanced features for now. Skip performance optimization. Skip corner cases. Keep a to-do list of what you have to revisit.
  6. Iterate. Now that it’s all working, make it work better. Reimplement, optimize, redesign if necessary.

Summary

  • An invariant is a property that is always true of an ADT object instance, for the lifetime of the object.
  • A good ADT preserves its own invariants. Invariants must be established by creators and producers, and preserved by observers and mutators.
  • The rep invariant specifies legal values of the representation, and should be checked at runtime with checkRep().
  • The abstraction function maps a concrete representation to the abstract value it represents.
  • Representation exposure threatens both representation independence and invariant preservation.
  • An invariant should be documented, by comments or even better by assertions like checkRep(), otherwise the invariant is not safe from bugs.

The topics of today’s reading connect to our three properties of good software as follows:

  • Safe from bugs. A good ADT preserves its own invariants, so that those invariants are less vulnerable to bugs in the ADT’s clients, and violations of the invariants can be more easily isolated within the implementation of the ADT itself. Stating the rep invariant explicitly, and checking it at runtime with checkRep(), catches misunderstandings and bugs earlier, rather than continuing on with a corrupt data structure.

  • Easy to understand. Rep invariants and abstraction functions explicate the meaning of a data type’s representation, and how it relates to its abstraction.

  • Ready for change. Abstract data types separate the abstraction from the concrete representation, which makes it possible to change the representation without having to change client code.