Specifications and Abstract Data Types: The Contracts Beneath the Code

Hook #

Every method you have ever written has a specification. Most of the time it lives only in your head, or half-written in a comment, or implied by the test that happens to exist. This course starts by dragging that specification into the light and treating it as a first-class engineering artifact — because the difference between code that other people (and future-you) can build on and code that quietly rots is almost entirely a question of whether its contracts are explicit. A specification is a promise: given these preconditions, I guarantee these postconditions. An abstract data type is that same idea scaled up to a whole object: here is what this type means and what it guarantees, and here — hidden behind a wall — is how it actually pulls it off. Get the contracts right and you can change the implementation freely, reason about correctness locally, and hand the code to a stranger. Get them wrong or leave them implicit, and every change becomes a game of "what will this break?"

What you'll be able to do by the end of this lesson #

• State a method's contract precisely as preconditions (what the caller must guarantee) and postconditions (what the method guarantees in return), and explain why a violated precondition is the caller's bug, not the method's.
• Explain an abstract data type as the separation of what a type means (its abstract value) from how it is represented (its fields), and why that wall is what makes code changeable.
• Define a representation invariant (the condition every valid instance must satisfy) and an abstraction function (the mapping from the concrete representation up to the abstract value it stands for).
• Recognize why a stronger precondition or a weaker postcondition makes a spec easier to implement but harder to use, and vice versa — the central trade-off of interface design.

A quick try before we start #

Write, in one sentence each, the precondition and postcondition of Array#[] (indexing into an array). Then ask: what happens in Ruby if you index out of bounds? (nil, not a crash.) Now Array#fetch? (It raises IndexError.) Same abstract operation, two different contracts: [] has a weak precondition (any index is legal) and absorbs the out-of-range case into its postcondition (returns nil); fetch has a stronger implied contract and fails loudly. Neither is "correct" — they are two points on the same design axis, and Ruby ships both on purpose. Noticing that a single operation can carry different contracts, and that the choice is a design decision, is the whole mindset of this lesson.

Why this matters here #

This is the foundational lesson of Software Construction because everything else in the course is downstream of it. Testing (the next two lessons) is meaningless without a spec — a test checks behavior against a contract; with no contract, a test just pins whatever the code happens to do today. Debugging is the search for where reality diverged from the spec. Refactoring is changing the implementation while preserving the contract — which you can only do safely if the contract is written down. Even concurrency correctness comes down to invariants that must hold across threads. Specifications and ADTs are not one topic among many; they are the substrate the other topics stand on.

For a working engineer, the payoff is concrete and daily. Every service object, every gem method, every API endpoint is an abstract data type or a specified operation whether you name it or not. The reason a well-designed library feels good to use is that its contracts are clear and stable; the reason a tangled internal service is miserable is that its "contract" is "read the implementation and hope." Learning to see and state contracts explicitly is what lets you build the deep, stable interfaces that everything else depends on — and it is the difference between code that is a foundation and code that is a liability.

The engineer's lens #

The first and most load-bearing idea is that a specification is a wall that decouples the caller from the implementer, and the entire value of the wall is that neither side has to know the other's business. The caller programs against the promise (preconditions → postconditions) and never looks at the implementation; the implementer is free to do anything at all as long as the promise is kept. This is why you can upgrade a library across a major version and your code still works — the maintainers preserved the contract even as they rewrote everything behind it. It is also why "just read the code to see what it does" is an anti-pattern dressed as diligence: if you depend on behavior that isn't in the spec, you have coupled yourself to an accident of the current implementation, and you will break the day it changes. The discipline the great libraries teach — the ones you actually enjoy depending on — is that they specify a little less than they implement, deliberately, so they keep room to evolve. When you write a public method, the question is not only "what does this do?" but "what am I willing to promise forever, and what am I keeping unpromised so I can change it later?"

The second lens is the pair that makes an ADT rigorous: the representation invariant and the abstraction function. The rep invariant is the answer to "what does a valid instance of this type look like?" — for a sorted set backed by an array, it might be "the array is sorted and has no duplicates." Every public method must preserve it: assume it on entry, restore it before returning. The abstraction function is the answer to "what abstract value does this concrete representation stand for?" — it maps the array [1, 3, 7] up to the abstract set {1, 3, 7}. These two ideas are quietly the most powerful correctness tool in the course, because they let you reason locally: to trust the whole type, you only need to check that each method preserves the rep invariant, one method at a time — you never have to hold the entire object's history in your head. This is exactly the move a Rails engineer makes without naming it. An ActiveRecord model's validations are a representation invariant ("an order always has a positive total and a customer"); the difference is that Rails checks the invariant at the database boundary rather than proving each method preserves it, which is why you can still wedge a model into an invalid in-memory state between assignment and save. Seeing that validates is a rep-invariant enforcement mechanism — and seeing where its enforcement has gaps — is the kind of X-ray vision this lesson gives you into a framework you already use.

The third, subtler lens is the trade-off geometry of a specification: a spec can be made stronger or weaker, and the direction has opposite consequences for the two sides of the wall. Strengthen the precondition (demand more of the caller — "the array must already be sorted") and you make the method easier to implement but harder and more dangerous to call. Weaken the postcondition (promise less — "returns the elements in some order") and you make the method easier to implement and safer to change, but less useful. The best interfaces are not the ones that promise the most; they are the ones that promise exactly enough and no more — strong enough to be useful, weak enough to leave the implementer room. This is the same instinct as Ousterhout's "deep module": the ideal is a simple, undemanding interface (weak preconditions, so it is safe to call) that hides genuinely significant complexity (a strong postcondition, delivered by hard work inside). When you catch yourself writing a method that demands the caller pre-arrange the world just so, you are pushing complexity out through the interface onto everyone who calls you — the opposite of a deep module, and a smell worth heeding.

What to focus on in the resources #

• The MIT 6.1020 specification and ADT readings — this is the primary text. Read for the vocabulary and the reasoning discipline: precondition/postcondition, rep invariant, abstraction function, and the "spec strength" trade-off. The examples are in Java; ignore the syntax and absorb the concepts — they are language-independent.
• The "spec strength" trade-off. Make sure you can explain why a stronger precondition is easier to implement but worse to depend on. This is the single most transferable idea for interface design.
• Ousterhout's deep vs. shallow modules (A Philosophy of Software Design). Read this as the design framing of the same wall: a deep module hides significant complexity behind a simple interface. Map it onto ADTs — a good ADT is a deep module.
• Skip on first pass: formal notation for specs (Hoare triples, JML-style annotations) and exhaustive rep-invariant checking machinery. Get the conceptual wall and the trade-off geometry; the formalism is a later, optional refinement.

Explain it back #

Explain to a colleague why "you can change the implementation as long as you preserve the contract" is the entire point of a specification — and what a representation invariant buys you. A strong answer: a spec is a wall (preconditions → postconditions) that lets the caller depend on a promise rather than on the implementation, so the implementer can rewrite everything behind the wall freely as long as the promise holds — that is what makes code changeable and libraries upgradable. A representation invariant ("what a valid instance looks like") lets you reason about correctness locally: check that each method preserves it, one at a time, and you can trust the whole type without holding its entire history in your head. Bonus: explain the spec-strength trade-off (a stronger precondition is easier to implement but harder and more dangerous to call) and connect it to Ousterhout's deep module (simple interface, hidden complexity).

Where this connects #

Backward: The ADT idea builds directly on the algebraic data types and pattern matching from the Programming Languages course (an ADT is the object-oriented cousin of a sum/product type — data plus the operations that respect its invariants). The very notion of a specified operation goes back to algorithm correctness and termination from the algorithms course: an algorithm is a spec (input → output) plus a procedure that provably meets it.

Forward: The next lesson, testing as engineering, is impossible without this one — a test checks behavior against a contract, so you must have a contract first. Property-based testing (lesson 3) tests the postcondition directly across thousands of generated inputs. Systematic debugging and refactoring (lesson 4) are, respectively, "find where reality broke the spec" and "change the code while preserving the spec." And the correctness-in-practice lesson (immutability, thread safety) is about keeping invariants intact under conditions — concurrency — that make them hardest to hold.