Chapter 11. Specify First: Abstract Data Types

Learning objectives

After this chapter you should be able to:

Do unaided:

Write a complete spec for a C module: header, pre- and postconditions, invariant, ownership and lifetime rules, error convention, tests and a complexity budget.
Write unit tests from a spec before any implementation exists, including edge cases (empty, one element, wraparound, growth).
Explain the difference between a precondition violation and a reported error, and decide which each condition in a module should be.
Trace a ring-buffer queue through pushes, pops, wraparound and growth.
Explain why the ownership and lifetime section of a spec is never delegated.

May delegate:

The implementation of a stack, queue or map ADT from your own header and tests (Pair role), and extra hostile tests against your spec (Adversary role).

Opening case

A composite case, not a real student or course.

Sam has an afternoon to add an upload queue to the station's logger: when the radio link drops, readings pile up, and when it returns they go out oldest first. The station's rvec and sensor_db follow the rule set in Chapter 6 and kept in Chapter 7: a container stores copies of the readings it is given, and the caller keeps whatever it passes in.

The chapter continues from here.

The loop in this chapter

Open a step to see what it asks of you and how it plays out in the Pair phase.

PredictWhat the one-line queue prints and what ASan reports; which decisions the prompt left open; how many tests the Pair's draft fails.

Step 1 of 6 · You, no AI

What you hand in: A written prediction: the output, the memory state, the operation count, and how sure you are.

Why this step: A prediction written before the run is the only way to learn whether your model of the machine is right. A miss is the most useful result there is, because it shows exactly where the model is wrong.

The first prediction is never delegated.

Ask yourself: What will this print, what will memory look like when it ends, and how many operations will it take?

Log the prediction in your work log · Predict in every chapter · ← Predict in Chapter 10 · Predict in Chapter 12 →
WriteBy hand, a ring-buffer trace through wrap and growth (Table 11.2) and a small stack with its contract (Listing 11.2).

Step 2 of 6 · You, no AI

What you hand in: One small piece written by hand, to build the mental model.

Why this step: You can only check what you could have built. Writing a small piece yourself gives you the model you will need to judge the agent's version later.

Ask yourself: Could I write this piece again tomorrow without notes?

Browse the companion code · Write in every chapter · ← Write in Chapter 10 · Write in Chapter 12 →
Specifyrqueue.h with all seven parts, including numbered ownership rules, and test_rqueue.c, before any implementation.

Step 3 of 6 · You

What you hand in: The header or class interface, unit tests, a complexity budget and the ownership rules.

Why this step: The specification is the contract the code will be held to. Tests written first, a cost budget and ownership rules turn "looks right" into something you can check.

The ownership and lifetime section of a specification is never delegated.

Ask yourself: Who allocates, who frees, what does it cost, and what input would break it?

Prompt and specification templates · Specify in every chapter · ← Specify in Chapter 10 · Specify in Chapter 12 →
DelegateThe Pair implements rqueue.c without changing the spec; the Adversary adds tests against the spec.

Step 4 of 6 · The agent

What you hand in: The implementation from your specification, or an explanation in the Tutor phase, with the prompts and transcript saved.

Why this step: The agent does the typing; you keep the judgment. Saving the prompts and the transcript makes the delegation something you can audit afterward.

Pair Pair phase: the agent writes small units from your specification, and you audit every line.

Ask yourself: Did I hand over my specification and tests, and did I save what the agent said?

Prompt templates · Delegate in every chapter · ← Delegate in Chapter 10 · Delegate in Chapter 12 →
AuditTests under ASan and UBSan, then -DNDEBUG, then Valgrind; each failure traced to a rule; bounds against the budget; keep or rewrite.

Step 5 of 6 · You and the tools

What you hand in: The Audit Report: tests, sanitizer and Valgrind output, your own cost derivation against a timing plot, the defects found, and a keep-or-rewrite decision.

Why this step: What the agent says is testimony until an instrument confirms it. Tests, sanitizers, Valgrind and a timing plot are evidence.

The final judgment that the code is correct is never delegated.

Ask yourself: What did the sanitizer report, does the timing plot match my derivation, and would I keep this code or rewrite it?

The Audit Report template · Audit in every chapter · ← Audit in Chapter 10 · Audit in Chapter 12 →
DefendThe empty-queue rule, where each byte is freed, why push is amortized O(1), why the ownership section is yours.

Step 6 of 6 · You, live

What you hand in: A five-minute oral defense.

Why this step: If you can explain it live, you own it. The oral checks that the understanding is yours and not the agent's.

Ask yourself: Why this bound, what input breaks it, and where is this memory freed?

How the loop works · Defend in every chapter · ← Defend in Chapter 10 · Defend in Chapter 12 →

What agents get wrong here

Patterns observed in agent-written code, to test for, not guarantees. If the agent no longer makes the mistake, your job is to prove it got it right, with the same instrument.

Invented ownership ("the container takes ownership")

How to catch it Map every free to a numbered rule; a test passing stack memory under ASan

Section 11.3.1 · AddressSanitizer, Tests

Silent behavior on error, or an assert on a normal run-time event

How to catch it One test per reported error; rebuild the tests with -DNDEBUG

Section 11.3.2 · Tests

Tests that run the code without constraining it

How to catch it Run the tests against an implementation you know is broken

Section 11.3.3 · Tests

What the chapter covers

11.1 The concept, by hand
- 11.1.1 From a request to a contract
- 11.1.2 Preconditions and postconditions
- 11.1.3 Invariants
- 11.1.4 The ownership and lifetime section
- 11.1.5 Error-reporting conventions
- 11.1.6 The complexity budget
- 11.1.7 Three ADTs: stack, queue and map
- 11.1.8 The queue spec in full
- 11.1.9 Tests as specification
11.2 Predict and check
11.3 What agents get wrong here
- 11.3.1 Invented ownership
- 11.3.2 Silent behavior on error
- 11.3.3 Tests that test nothing
11.4 Working with the agent
- 11.4.1 What to hand over, and what never to hand over
- 11.4.2 The audit, run by run
11.5 Lab: The station's upload queue
11.6 Defend it

Cost thread

With initial capacity 4 and doubling, n = 1,000,000 pushes grow the buffer 18 times (at sizes 4, 8, ..., 524,288) and copy 4 + 8 + ... + 524,288 = 1,048,572 readings: fewer than 2n (Chapter 8), so push is O(1) amortized. Table 11.4 measures it with time_rq.c (in the companion repository): push n readings, pop them all, best of five runs, gcc -std=c17 -O2, no sanitizers, one machine. O(1) operations predict a roughly flat time per operation as n grows 32-fold.

Summary

A prompt is a request; a spec is a contract. The one-line queue made nine decisions and announced only one, as a benefit.
An ADT spec has seven parts: header, pre- and postconditions, invariant, ownership and lifetime, error convention, tests, and a budget per operation.
A precondition violation is a caller bug and may be an assert; a condition correct programs meet must be reported in every build, including -DNDEBUG.
The ownership and lifetime section is never delegated: the rule depends on code outside the module, and an uninformed agent invents one that compiles.
Tests written first are the spec in executable form; the valuable ones cross a boundary of the representation, such as growth while wrapped.
Both of the Pair's defects were traced to numbered rules and found by instruments, not by reading the agent's note.

Key terms

specification (spec): a written contract of what a module promises callers and requires of them.
precondition: what must hold when a function is called; if it fails, the caller has the bug.
postcondition: what a function promises on return, given that its precondition held.
invariant: a condition on a data structure that each operation may assume on entry and must restore on return.
precondition violation: a call breaking a precondition; checked by assert, undefined without it.
reported error: a failure a correct program can meet, detected in every build and returned to the caller.
ownership and lifetime section: the spec part saying who frees each piece of memory and how long each pointer is valid.
complexity budget: the cost each operation may have, stated in the spec with its input-size variable.
stack: an ADT that returns items last-in, first-out.
queue: an ADT that returns items first-in, first-out (FIFO).
map: an ADT that associates each key with one value, looked up by key.
ring buffer: an array used as a queue, whose positions wrap from the last slot to slot 0.
model-based test: a test comparing the code with a simple correct model over the same operations.

Companion code

15 files for this chapter, compiled with the book's flags.

Read the code Download ch11.zip

Connections

Where this chapter and another point to each other most often.

Chapter 6: The Stack and the Heap: Dynamic Memory and Ownership
The station's rvec and sensor_db follow the rule set in Chapter 6 and kept in Chapter 7: a container stores copies of the readings it is given, and the caller keeps whatever it passes in.
Chapter 8: Growable Arrays and Linked Lists: The Cost of Growth
For the upload queue, with n readings held: rq_push is O(1) amortized and O(n) on the call that grows (doubling, Chapter 8); rq_pop, rq_size and rq_destroy are O(1); space is O(capacity), with capacity at most the larger of the initial capacity and twice the largest n ever held.
Chapter 9: Files, Bits, and Function Pointers: ADTs Behind a Header
Chapter 9 showed the C mechanism (an opaque pointer) and the reason, after Parnas (1972): the representation is the module's secret.
Chapter 10: Complexity and Sorting: Your First Delegation
Chapter 10's sort spec had a signature, tests and a budget.

See it on the map

11 Specify First: Abstract Data Types