Chapter 2 — Contracts and Specifications

“Write the contract first. Then the contract is what you have to be right about, instead of the code.” — Bertrand Meyer (paraphrased)

“And the LORD said to Moses, ‘Write these words, for in accordance with these words I have made a covenant with you and with Israel.’” — Exodus 34:27

Why This Matters

Last week you read code. This week you write something before code: the contract the code is going to honor.

A senior engineer does not open an empty file and start typing methods. A senior engineer opens an empty file and starts typing method signatures, parameter constraints, return guarantees, and conditions that must hold before and after the method runs. The body of the method is the last thing written, because by the time the contract is firm, the body almost writes itself.

This is the practice of specification-driven design, and it is the single largest skill gap between a junior and a senior programmer. It is also — preview of Phase 2 — exactly the skill that makes you good at directing AI. A vague prompt produces vague code. A precise prompt, with a real specification, produces code that often works on the first try. The prompt and the spec are the same artifact. You will see this in Chapter 10. For now, you are training the spec muscle so the prompt muscle has something to grow on top of.

The Christian student already lives inside a tradition that takes promise-keeping seriously. The covenant theology of Reformation Lutheranism is precisely about a God who binds himself by promise — and then keeps the promise He made, regardless of the cost. The Augsburg Confession (1530) is what happens when a community decides to write the covenant down in such precise terms that a five-hundred-years-later reader can still tell who’s keeping faith with it and who isn’t. A specification is a covenant in software form. Same shape. Smaller stakes.

A program with no specification is a program nobody can verify. A specification with no program is a promise nobody has tried to keep. Both halves matter. This chapter is the first half. Chapter 4 (testing) is the verification. Together they are how the senior engineer trusts code at all.

2.1 — What Is a Specification?

A specification is a promise about behavior. Concretely, for a method, the specification answers four questions:

1. What does the method do? One sentence. (The purpose.)
2. What must be true before the method is called? The preconditions.
3. What is guaranteed to be true after the method returns? The postconditions.
4. What is guaranteed to remain true throughout, regardless? The invariants.

A method without a specification is a black hole. You can call it. You don’t know what it does. You don’t know what it requires. You don’t know what it promises.

A method with a specification is a contract. The caller agrees to satisfy the preconditions. The method agrees to deliver the postconditions. Both sides are bound. If the caller violates the precondition, the method’s behavior is undefined — that’s the caller’s bug. If the method violates the postcondition while the caller did their part, the method has a bug.

This is not a Java idea. It is a programming idea. Eiffel made it explicit with Design by Contract in the late 1980s. Bertrand Meyer wrote a book about it. Java borrows the vocabulary and writes the contracts in Javadoc comments.

Coach’s Note — A contract is not a wish. A contract is enforceable. By the end of this chapter, every contract you write will be paired with tests (Chapter 4) and runtime assertions (Chapter 3) that actually check the contract. The spec without enforcement is a polite suggestion.

2.2 — A Specification, Written Down

Here is a method with no specification. Read it. Try to use it. Notice what you cannot tell from the signature alone. (download FindExample.java — both versions, with a main you can run.)

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

Questions a caller has:

• What if arr is null?
• What if arr is empty?
• What if the target appears more than once — does this return the first, last, or any?
• What does the -1 mean? Is -1 “not found” or is it a valid index in some encoding?

You can read the body and infer the answers. But the contract is what should tell you, not the body. The contract is what lets a caller use the method without reading the body.

Here is the same method with a proper Javadoc specification:

/**
 * Returns the index of the first occurrence of the given target in the array.
 *
 * @param arr    the array to search; must not be null
 * @param target the value to search for
 * @return the smallest index {@code i} such that {@code arr[i] == target},
 *         or {@code -1} if no such index exists
 * @throws NullPointerException if {@code arr} is null
 */
public int find(int[] arr, int target) {
    for (int i = 0; i < arr.length; i++) {
        if (arr[i] == target) return i;
    }
    return -1;
}

Now the caller knows everything. They know arr cannot be null (precondition). They know they will get the first occurrence, not just any (postcondition). They know -1 is the sentinel for “not found.” They know violating the precondition causes a NullPointerException. The body is now an implementation detail. The contract is the truth.

That is what this chapter trains.

2.3 — Javadoc Syntax (The Subset You Actually Need)

Javadoc is the standard Java mechanism for embedding documentation directly in source files. The compiler ignores it. The javadoc tool turns it into the HTML you saw at docs.oracle.com when you read the standard library last week.

A Javadoc comment is a block comment that starts with /** (two asterisks, not one) and ends with */. It sits immediately before the class, method, or field it describes.

/**
 * One-line summary sentence ending with a period.
 *
 * Longer description, possibly multiple paragraphs.
 *
 * @param  paramName   description of this parameter
 * @return             description of the return value
 * @throws ExceptionType   under what circumstances
 */

The tags you will actually use this semester:

Worth noting: the first sentence of a Javadoc (everything up to the first period followed by whitespace) is treated specially — it appears in summary lists in the generated docs. So make it a real, complete, useful sentence.

The fully-specified mean method below is worth studying as a template (download MeanExample.java).

/**
 * Computes the average of the array. Returns NaN if the array is empty.
 *
 * The average is calculated as the sum of all elements divided by the count.
 * Overflow is not detected; callers with very large arrays of large values
 * should consider {@link Math#fma} or a wider accumulator.
 *
 * @param values the array of values; must not be null
 * @return the arithmetic mean, or {@code Double.NaN} if {@code values.length == 0}
 * @throws NullPointerException if {@code values} is null
 */
public static double mean(double[] values) {
    if (values.length == 0) return Double.NaN;
    double total = 0;
    for (double v : values) total += v;
    return total / values.length;
}

Coach’s Note — The Javadoc syntax is small. The discipline is what’s hard. Writing @param values the values to average is not a spec — it’s a restatement of the parameter name. Writing @param values the array of values; must not be null is a spec, because it adds a constraint nobody could infer from the name. The spec is the part that adds information.

2.4 — Preconditions, Postconditions, Invariants

These three words come up over and over. Get them precise now.

Precondition

What must be true before the method is called for the method to do its job. The caller’s responsibility.

Examples in Java:

• arr must not be null.
• index must satisfy 0 <= index < size().
• capacity must be positive.
• The list must not be empty.

If the caller violates a precondition, the method’s behavior is undefined in the language sense. The method may throw, may return garbage, may corrupt state. The contract gives no guarantees. That’s the caller’s problem.

In practice, well-written Java methods convert “undefined behavior” into a specific, recognizable exception — usually NullPointerException, IllegalArgumentException, or IndexOutOfBoundsException. That’s the fail fast discipline (Chapter 3 will go deep on this).

Postcondition

What is guaranteed to be true after the method returns. The method’s responsibility, conditional on the caller having satisfied the preconditions.

Examples:

• The return value is the smallest index where the target was found, or -1 if it wasn’t found.
• The list’s size has increased by exactly one.
• The map’s value for the given key is the value just passed in.

A postcondition is a promise the method keeps. The caller can rely on it without reading the body.

Invariant

What must always be true about the object, before and after every method call. The class’s responsibility.

Examples (for a BankAccount class):

• balance >= 0 (or balance >= -overdraftLimit).
• owner != null after construction.
• The sum of all deposits minus the sum of all withdrawals equals the current balance.

Invariants are the rules the object maintains about its own state. Methods are allowed to break the invariant momentarily inside their body (e.g., during a transfer, the source account is briefly debited before the destination is credited) — but the invariant must be restored before the method returns.

The Lutheran apologetic frame fits well here: a covenant is a standing promise. It holds before and after every interaction. An invariant in software is the same kind of standing promise — no matter what method is called, this thing remains true about this object.

Coach’s Note — When you’re stuck designing a class, write the invariants first. The invariants tell you what the methods are even allowed to do. A method that breaks an invariant is, by definition, a bug. Once the invariants are written, the methods almost design themselves.

2.5 — Method Signatures as Contracts

Before you write any prose in Javadoc, the signature itself is part of the contract. Every piece of the signature is a promise.

public boolean isOpen()

• public — “any caller may invoke this.” (Access modifier is a contract.)
• boolean — “I will return exactly one of true or false. I will not throw a checked exception. I will not modify your boolean reference because there isn’t one.” (Return type is a contract.)
• isOpen — “this is a boolean accessor; I do not modify state.” (Name is a contract by convention.)
• () — “I require no arguments.” (Empty parameter list is a contract.)

When you write a method signature, you are making four promises before you’ve written a word of prose. The Javadoc fills in the prose. The signature alone, well-named, communicates a great deal.

A signature that lies — getName() that mutates state, isReady() that returns void and “indicates readiness via a side channel” — is the senior engineer’s least favorite kind of code. Don’t write it.

2.6 — A Worked Spec: EventLog

Let’s specify a small class together, the way you would for Project 2 — and the way you’d hand the spec to an AI in Phase 2.

Problem: A class that tracks events. Each event has a category (a string), a message (a string), and a timestamp (milliseconds since epoch, captured at the moment the event is added). Callers can add events, get all events of a given category in the order they were added, and get the total count.

Step 1: The class header

/**
 * An append-only log of events, each tagged with a category and timestamp.
 *
 * <p>Events are stored in insertion order. The log is not thread-safe.
 * Callers requiring concurrent access must provide external synchronization.
 *
 * <p>Categories are case-sensitive. Lookups by category return events
 * whose category equals the given string under {@link String#equals}.
 *
 * <p>This class maintains the invariant that {@link #count()} equals the
 * total number of successful {@link #add} calls since construction.
 */
public class EventLog {

The class header documents:

• What the class is.
• Insertion-order guarantee (a postcondition of add).
• Thread-safety policy (a precondition the caller must respect across calls).
• Case-sensitivity of categories (a postcondition of lookups).
• The headline invariant of the class.

Step 2: The constructor

/**
 * Constructs an empty event log.
 *
 * @implSpec The log starts with {@code count() == 0}.
 */
public EventLog() {
    this.events = new ArrayList<>();
}

A constructor’s contract is usually short — the postcondition is “a valid object exists with the documented initial state.” The @implSpec tag (Java 8+) calls out an implementation detail that callers can rely on.

Step 3: The add method

/**
 * Adds an event with the given category and message to the log.
 *
 * <p>The event's timestamp is captured as the current value of
 * {@link System#currentTimeMillis()} at the moment of the call.
 *
 * @param category the event's category; must not be {@code null}
 * @param message  the event's message; must not be {@code null}
 * @throws NullPointerException if {@code category} or {@code message} is null
 * @implSpec After return, {@code count()} has increased by one and the
 *           newly added event is the last in {@link #getByCategory} for
 *           the given category.
 */
public void add(String category, String message) { /* ... */ }

Notice:

• Two preconditions, both explicit (non-null).
• The timestamp behavior is part of the contract — callers know it’s captured at call time, not at log construction.
• An @implSpec documenting two postconditions.

Step 4: The lookup

/**
 * Returns the events in the given category, in insertion order.
 *
 * @param category the category to filter by; must not be {@code null}
 * @return an unmodifiable list of events with the matching category;
 *         empty if no events match
 * @throws NullPointerException if {@code category} is null
 */
public List<Event> getByCategory(String category) { /* ... */ }

The unmodifiable guarantee is a postcondition that protects the class’s invariant. If callers could mutate the returned list, they could violate the “insertion order” invariant from the class header. The return type is List<Event>; the documentation tells the caller the list is unmodifiable. The implementation will use Collections.unmodifiableList(...) to enforce it.

Step 5: The count

/**
 * Returns the number of events currently in the log.
 *
 * @return the count, always {@code >= 0}
 */
public int count() { /* ... */ }

Short and complete. The >= 0 is a postcondition that follows trivially from the constructor + add contracts, but stating it explicitly is good hygiene — a caller never needs to wonder.

What we did

We wrote no implementation. We wrote only the contract. And yet — anyone could now read this spec and write the implementation. Anyone could write the test suite. Anyone could review the implementation against the spec. The spec is the real artifact. The implementation is a verifiable consequence.

That is the move.

Coach’s Note — Notice how much of the spec was actually the same kind of careful reading you did in Chapter 1, but in reverse. You’re writing what a careful reader would want to be told. If Chapter 1 made you a good reader, Chapter 2 is asking you to write for that reader. Same skill, opposite direction.

2.7 — Spec Before Code: The Workflow

The discipline of this week:

1. Read the problem statement. What is the class for?
2. Write the class-level Javadoc. What does it do? What invariants does it maintain? What’s the thread-safety policy?
3. Write every method signature with its complete Javadoc. Preconditions, postconditions, exceptions, return semantics. No method bodies yet.
4. Read your spec out loud. Imagine handing it to a colleague (or to an AI). Does it answer every question they would have?
5. Now write the implementations.
6. Now write the tests (Chapter 4’s topic — but you can do this in Project 2’s Medium tier already).
7. Read your code against your spec. Does every postcondition hold? Does every precondition get enforced? Did you break an invariant somewhere?

In practice, you will iterate. Writing the spec will reveal that the problem statement was ambiguous. Writing the implementation will reveal that the spec was incomplete. Writing the tests will reveal that the spec was wrong. Each iteration tightens the contract.

The order matters because each step constrains the next. Spec-first design is cheap to revise — changing a Javadoc comment costs nothing. Implementation-first design is expensive to revise — rewriting code costs time. Get the cheap revisions out of the way first.

2.8 — Covenant Theology, Compactly

The chapter’s apologetic frame: what does it mean to make a promise and keep it?

A covenant in the biblical sense is not a contract between equals — it is a binding promise, usually initiated by God, in which the terms are specified, the parties are named, and the consequences of faithfulness and infidelity are made explicit. The Old Testament covenants (Noahic, Abrahamic, Mosaic, Davidic) and the New Covenant in Christ are each a worked example of “promise written down precisely enough that a thousand years from now we can still tell who’s keeping it.”

The Lutheran confessional tradition takes this seriously. The Augsburg Confession, presented in 1530, was an attempt to write down — in language a Holy Roman Emperor’s court could read — exactly what the evangelical churches confessed. It is precise speech under pressure. The Lutheran fathers were not philosophers writing for the academy; they were pastors trying to leave a durable record their grandchildren’s grandchildren could still rely on. The Formula of Concord (1577) is a second pass at the same exercise, sharpened by another fifty years of controversy.

A specification is the same kind of artifact. A method’s Javadoc is a promise the implementer makes to every caller, present and future, that the method behaves the way the doc says. When the implementer keeps the promise — when the body actually does what the spec says — the caller can build on the method without fear. When the implementer breaks the promise, the dependent code breaks too, often in places far from the original method, often months later. The cost compounds.

A team that takes specifications seriously is a team that takes promises seriously. The connection is not metaphor. It is a continuation of the same human discipline — say what you mean, mean what you say, do what you said — applied to code.

Coach’s Note — I am not trying to make Javadoc holy. I am trying to make you take it as seriously as the people who wrote the Augsburg Confession took precise speech under pressure. That seriousness is the muscle. The Java syntax is just the gym equipment you train it on.

2.9 — Common Bugs (Spec Edition)

These are the bugs your specifications introduce.

Bug: The Javadoc describes parameter x but the method is actually named value. What happened: You renamed the parameter and didn’t update the Javadoc. Fix: Use your IDE’s “extract parameter” / “rename” refactoring, which updates Javadoc automatically. Or: re-read the Javadoc after every signature change.

Bug: The Javadoc says @throws IllegalArgumentException but the body throws NullPointerException. What happened: The spec and the implementation drifted. Fix: Decide which is right. Update the other. Add a test that triggers the throw and verifies the type — this is Chapter 4’s job, but you can already see why tests catch this class of bug.

Bug: A precondition like “must not be null” is documented but not enforced in the body. What happened: You wrote the spec but trusted callers to follow it. They didn’t. Fix: Add Objects.requireNonNull(arg, "arg") at the top of the method. The runtime check is one line; it converts a “mysterious NullPointerException later” into a “clean exception with a useful message immediately.” (Chapter 3.)

Bug: A postcondition like “returns an unmodifiable list” is documented but the body returns the internal list directly. What happened: Spec says one thing, code does another. Caller mutates the list. Class’s invariant breaks. Bug appears in a completely unrelated method weeks later. Fix: return Collections.unmodifiableList(events);. Match the spec.

Bug: The Javadoc summary sentence is “Adds.” — one word. What happened: Lazy. The generated docs now show a method whose summary is just the word “Adds.” Fix: Write the sentence. “Adds an event with the given category and message to the log.” Treat the first sentence as the headline that will be skimmed.

Bug: Two methods on the same class document slightly different preconditions for the same parameter (one says “must not be null,” the other says nothing). What happened: Inconsistency. The reader can’t tell which behavior they should rely on. Fix: Pick a policy and apply it everywhere. Either both forbid null (consistent), or one accepts null with documented behavior (e.g., “if null, returns empty list”).

2.10 — Reps

Open the exercises. The reps this week are spec-writing reps. You will:

• Read a function and write its Javadoc from the body.
• Read a Javadoc and write the function from the spec.
• Spot Javadocs that lie.
• Write specs for unusual cases — null inputs, empty inputs, very large inputs.

Every rep is AI-off. The spec muscle has to live in your hands before Phase 2 can put it to work.

2.11 — This Week’s Project

You’re ready for Project 2 — Spec Before Code, in Project 2.

You will pick one of three small classes to specify and build. The Normal tier asks you to write the complete Javadoc spec first, then the implementation. The Medium tier asks you to add a test for every contract claim. The Hard tier asks you to refactor the implementation to be more elegant without changing the spec or the tests — the proof that a real spec is implementation-independent.

This is the project that, if you do it well, gives you the skill you will use in Phase 2 to write prompts that actually work. Don’t shortcut it.

2.12 — Coach’s Final Word for Week 2

Last week you read. This week you wrote — but you wrote promises, not code. You wrote the contract that the code is going to have to keep.

Three more weeks of Phase 1 to go before the midterm, and each one is going to compound on this one. Chapter 3 teaches you how to enforce the contracts you wrote this week. Chapter 4 teaches you how to verify the contracts you wrote this week. Chapter 5 teaches you how to debug when the contract is being violated and you don’t know where. All three of those chapters assume you have the spec in your hands first.

If you find yourself starting Chapter 3 without a spec for the code you’re about to refactor — go back to this chapter and write one. The spec is the artifact every subsequent week depends on.

See you on Monday.

Up next: Read the exercises and run every rep. Then open Project 2 and write your first specification. After that, Chapter 3 — exception handling.