Overview
7 Reasoning About Correctness
The chapter opens by reframing correctness as more than just “the code does what the tests say” or “the code meets the requirements.” Instead, it argues that simple and correct software can be reasoned about algebraically: by identifying the sets of values our data types denote, the operations that combine them, and the laws those operations should satisfy. Using a messy ETL example with duplicate customer records, conflicting values, and optional fields, it shows that implementation details can obscure what the problem really is, while algebraic thinking helps separate meaning from mechanics.
From there, the chapter develops a practical style of reasoning based on binary operations, associativity, ordering, and monotonicity. It demonstrates how everyday Java code often hides algebraic structure in loops, collections, and mutating APIs, and how that structure can be made explicit by treating lists and maps as values that can be “added” together. That perspective leads to reusable abstractions built from standard library tools such as streams, comparators, and binary operators, allowing the duplicate-cleaning pipeline to collapse into a much smaller and more general form.
The final part of the chapter focuses on proving correctness with exhaustive, property-based tests. It shows how to enumerate all possible states of a domain, including records with optional fields, and then assert laws over every value or every pair and triple of values. For the example domain, correctness is captured by properties like associativity, order preservation, and monotonicity, which can be checked independently of implementation choices. The chapter ends by extending these ideas to Optional through lifting, showing how ordinary binary operations can be transformed to work across missing values while keeping the same algebraic guarantees.
A first look at the world we’re in
A sea of missing and undefined data
An exciting first example!
Algebraic laws must hold for all possible inputs
An algebra appears!
Addition is a closed binary operation
Designing our algebra by copying existing, well-trodden design patterns
Extracting the grouping logic into its own generic function
the state management involved in grouping
Visualizing common methods as algebraic binary operations
translating into a binary operation
Visualizing adding something to a map as a binary operation combining maps
How we’re pipelining our work
Algebraic reasoning leads to deep insights that can remove redundant computation
The set of values that comprises an Integer in Java
figuring out the concrete set of values that complex data types denote
Translating between English, Java, and math
Stealing from the math people lets us express complex ideas succinctly
The associativity property
Associativity buys flexibility in execution
DRYing the code by extracting the duplicated logic into its own function
Another look at the requirements
Describing the requirements in terms of Comparator
We get to decide what the relationship between our values means
Defining what it means for one record to be “more favorable” than another
Policy and AuditFindings sorted lexicographically
The properties associated with Java’s standard Comparable interface
Examples of order not being preserved during an operation
Functions that operate on ordered data don’t have to preserve that order
The Monotonic property
Visualizing Optional as a parallel universe
Jumping entire functions to the Optional universe
Summary
- Algebraic thinking enables us to rigorously define correctness
- If we know what correct means our tests suite can verify it
- Being able to describe correctness is important in the age of large Language Models
- Algebra doesn’t need to be fancy! An entire “algebra” can be a single operation
- We do algebra in Java by thinking about what equations hold between data types
- Algebraic properties are based around assertions that begin with “for all states…”
- Math uses an upside-down capital “A” (∀) as a shorthand meaning “for all”
- Notation allows us express complex relationships between variables compactly (∀𝑎, 𝑏, 𝑐)
- Expressing ideas in mathematical notation forces us to be precise about what we mean
- Associativity is the most common property you’ll find in programming
- Associative operations can be grouped in any order (∀𝑎, 𝑏, 𝑐 ∈ 𝑋, (𝑎 + (𝑏 + c)) = ((𝑎 + 𝑏) + 𝑐)
- Associativity enables parallel computation by decoupling us from sequential application
- Algebraic thinking can guide us towards simpler, smaller implementations
- Don’t force a property to work. Clear data semantics outweighs elegant algebras
- Commutativity means that “the order of arguments doesn’t matter”
- The Commutativity Law: ∀𝑎, 𝑏 ∈ 𝑋, 𝑎 + 𝑏 = 𝑏 + 𝑎
- The ordering properties used by Comparator are
- Reflexivity: ∀𝑎 ∈ 𝑋, 𝑎 ≤ 𝑎
- Antisymmetry: ∀𝑎, 𝑏 ∈ 𝑋, 𝐼𝐹 𝑎 ≤ 𝑏 𝐴𝑁𝐷 𝑏 ≤ 𝑎 𝑇𝐻𝐸𝑁 𝑏 = 𝑎
- Transitivity: ∀𝑎, 𝑏, 𝑐 ∈ 𝑋, 𝐼𝐹 𝑎 ≤ 𝑏 𝐴𝑁𝐷 𝑏 ≤ 𝑐 𝑇𝐻𝐸𝑁 𝑎 ≤ 𝑐
- Orders are so “obvious” that they’re the easiest to overlook.
- Many problems can be solved by realizing they’re ordered (even minimally)
- Monotonicity describes functions which preserve the ordering properties of their data
- The monotonicity law: ∀𝑎1, 𝑎2, 𝑏1, 𝑏2 ∈ 𝑋, 𝐼𝐹 𝑎1 ≤ 𝑏1 𝐴𝑁𝐷 𝑎2 ≤ 𝑏2 𝑇𝐻𝐸𝑁 𝑎1 + 𝑎2 ≤ 𝑏1 + 𝑏2
- The hardest part of monotonicity is realizing that it’s not saying something complicated
- Not adding algebraic interfaces into the code is usually a good call (but it’s up to you!)
- BinaryOperator and UnaryOperator are useful Algebraic interfaces built into Java
- Algebraic properties can guide our implementation in both the small and large
- Designing around an algebra lets you leverage Java’s most powerful tooling
- An implementation doesn’t need to match the algebra!
- With practice, you can see the algebra that underpins any implementation
- Studying algebraic properties lets us see the commonalities that unite programming
- A useful mental model for Optional is to think of it as being its own parallel universe
- We can move data, functions, and behavior into the Optional universe using transforms
- Optional.of moves data from the “normal” universe into the Optional one
- A special function called “lift” can move functions into the Optional universe
- Algebraic thinking has the same effect as data modeling. It simplifies everything.
FAQ
What does this chapter mean by “correctness”?
Correctness is defined in terms of algebraic properties and invariants that hold for all possible states, not just a few examples or implementation-specific tests. An implementation is correct when it satisfies the laws that describe the intended behavior of the data and operations.Why does the chapter focus so much on algebraic reasoning?
Because algebraic reasoning lets us describe what code means rather than how it is implemented. That makes it easier to reason equationally, identify universal laws, and write tests that verify behavior independently of a specific algorithm.What is a binary operation in the context of this chapter?
A binary operation is a deterministic function that takes two values of the same type and returns a value of that same type. In the chapter, operations like combining duplicate records are reshaped into binary operations so they can be reasoned about algebraically.Why is associativity important for combining data?
Associativity means that grouping does not affect the result:(a + (b + c)) = ((a + b) + c). This matters because it lets the computation be rearranged, which is essential for using tools like reduce and for enabling parallel execution safely.How does the chapter use “for all possible states” in testing?
It generates every possible value in the domain and checks that an invariant holds for each one. This turns a vague idea of correctness into an exhaustive property-based style test, such as verifying a law for every possibleRawData value.Why does the chapter create all possible RawData values?
To prove properties over the entire state space, not just representative examples. Since the domain is small enough, the chapter can enumerate every possible state and use that set to test algebraic laws exhaustively.What does monotonicity mean in this chapter?
Monotonicity means the operation preserves order: if one input is “less than or equal to” another, then the result should not move backward in that ordering. For this domain, combining records should only move toward the more favorable outcome.Why does the chapter introduce Comparator and maxBy?
Because the business rule “pick the more favorable record” is really an ordering problem. By expressing the domain as an ordering, the implementation can reuse Java’s built-in Comparator and maxBy instead of encoding custom conditional logic.What is lifting in relation to Optional?
Lifting is the process of taking a function from the normal world and turning it into a function that works on Optional values. If both values are present, the function is applied; otherwise the result is Optional.empty().
Data-Oriented Programming in Java ebook for free
