Method Contracts & Invariants — State method contracts (inputs/outputs) and invariants - Java

SECTION 1

Historical Context & Motivation

Imagine you order food at a restaurant. You expect a menu that tells you exactly what each dish contains, and the kitchen promises to deliver what you ordered. If either side breaks its promise — you order something not on the menu, or the kitchen sends out the wrong plate — things fall apart. Early software development had the same problem: methods were written with no clear agreement about what they expected or what they would return, and bugs were rampant as a result.

The idea of making these agreements explicit in code grew out of decades of research into writing reliable, bug-free software. Pioneers in computer science realized that if programmers stated their assumptions clearly — what a method needs to work correctly, what it guarantees when it finishes, and what must always remain true — then entire categories of bugs could be prevented before the code ever ran.

1969 • Hoare Logic

Sir Tony Hoare published a landmark paper introducing preconditions and postconditions as formal tools for reasoning about program correctness. This laid the theoretical foundation for method contracts.

1986 • Design by Contract

Bertrand Meyer coined the term Design by Contract while creating the Eiffel programming language, which built preconditions, postconditions, and invariants directly into the language syntax.

1995 • Java Released

Java 1.0 launched without built-in contract keywords, but its strong type system and exception handling gave programmers tools to enforce contracts manually through parameter validation and Javadoc documentation.

2002 • Java assert Keyword

Java 1.4 introduced the assert keyword, giving developers a lightweight way to check preconditions, postconditions, and invariants directly in their code at runtime.

2010s • Modern Tooling

Annotations like @NotNull and @Nullable became popular, and IDEs like IntelliJ began checking contracts automatically, bringing contract ideas into everyday Java development.

The central question these ideas address is straightforward: How can we write methods that clearly communicate their rules so that callers and implementers both know exactly what is expected? This is the problem that method contracts and invariants solve.

SECTION 2

Core Principles & Definitions

A method contract is an agreement between the code that calls a method (the caller) and the method itself (the implementer). The contract spells out three things: what the caller must provide, what the method promises to deliver, and what truths must always hold. These three parts have formal names — preconditions, postconditions, and invariants — and together they form the backbone of reliable Java code.

Precondition

A condition that must be true before a method runs. It defines valid inputs. For example, a withdraw(amount) method might require amount > 0. The caller is responsible for satisfying preconditions.

Postcondition

A condition that must be true after a method finishes. It defines the guaranteed output or side effect. For example, after withdraw(amount), the balance must have decreased by exactly amount. The implementer is responsible for meeting postconditions.

Invariant

A condition that must always remain true throughout an object's lifetime. For a BankAccount, an invariant might be balance >= 0. No method should ever leave the object in a state that violates its invariant.

Defensive Programming

The practice of checking preconditions at the start of a method and throwing clear exceptions like IllegalArgumentException when they are violated. This catches bugs early and provides helpful error messages instead of mysterious crashes.

Documentation

Contracts should be written in Javadoc comments using @param, @return, and @throws tags so other programmers can understand and rely on the contract without reading the source code.

✦

KEY TAKEAWAY

Think of a method contract like a vending machine agreement. You (the caller) must insert the right amount of money and press a valid button — those are the preconditions. The machine (the method) promises to give you the snack you selected — that is the postcondition. And no matter how many snacks are bought, the machine must never have a negative inventory — that is the invariant.

SECTION 3

Visual Explanation — The Contract Flow

This diagram shows the full lifecycle of a method contract. The precondition is checked at the method's entry. The postcondition is verified when the method exits. The class invariant must hold true before and after every public method call.

Follow the arrows from left to right. The caller invokes account.withdraw(50). Before the method body executes, the precondition gate checks that amount > 0 and amount <= balance. If those pass, the method body runs and subtracts the amount. On the way out, the postcondition verifies that the balance decreased by exactly the withdrawn amount. Throughout the entire process, the class invariant (balance >= 0) must remain true. If any of these checks would fail, we know a bug exists — either in the calling code or the method itself.

SECTION 4

How Contracts Work in Java Code

Java does not have built-in contract keywords like Eiffel's require and ensure. Instead, Java programmers enforce contracts using three complementary techniques: Javadoc documentation to communicate the contract, runtime validation to enforce preconditions by throwing exceptions, and assert statements to verify postconditions and invariants during testing.

Technique 1 — Javadoc Contract

The @param tag describes each parameter and its valid range (the precondition on that input). The @return tag describes what the method promises to return (part of the postcondition). The @throws tag states which exception is thrown when a precondition is violated. Together these three tags form a human-readable contract that any developer can consult without reading the implementation.

Technique 2 — Guard Clauses for Preconditions

A guard clause is an if statement at the very beginning of a method that checks each precondition and throws an exception immediately if the condition is violated. For example, if (amount <= 0) throw new IllegalArgumentException("amount must be positive"); protects the method from bad input. This is called defensive programming because you defend the method against misuse. Guard clauses should always run in production, unlike asserts.

Technique 3 — Assert Statements

The assert keyword lets you verify postconditions and invariants during development. Writing assert balance >= 0 : "Invariant violated: negative balance"; at the end of a method will throw an AssertionError if the invariant is broken. Asserts can be enabled with the -ea flag when running Java and are typically disabled in production for performance. They serve as executable documentation — living proof that the contract is being honored.

💡

Precondition vs. Postcondition Responsibility

A useful rule of thumb: the caller is responsible for meeting preconditions. The method is responsible for meeting postconditions. If a precondition fails, it is the caller's bug. If a postcondition fails, it is the method's bug. This clear division of blame makes debugging much easier.

SECTION 5

Anatomy of a Full Contract

Let's see what a complete method contract looks like in practice. The diagram below shows a fully annotated BankAccount class with its withdraw method. Every element of the contract — preconditions, postconditions, invariant, Javadoc, and guard clauses — is labeled so you can see exactly where each piece lives in the code.

The code on the left shows a complete withdraw method. Dashed amber boxes mark precondition guard clauses. The green dashed box marks the postcondition assert. The pink dashed box marks the invariant assert. Labels on the right identify each part of the contract.

Contract Part	Where It Lives	Who Is Responsible	What Happens on Violation
Precondition	Guard clause at method start	Caller	`IllegalArgumentException`
Postcondition	`assert` before `return`	Method implementer	`AssertionError`
Invariant	`assert` at end of every public method	Class designer	`AssertionError`

Summary of contract parts, their locations, and responsibilities

SECTION 6

Worked Example — Building a StudentGradeBook Contract

Let's walk through writing a method contract from scratch. We will build a addGrade method for a StudentGradeBook class. The method accepts a grade between 0 and 100, adds it to the list of grades, and returns the updated average.

Writing a Complete Method Contract for addGrade

1
Step 1 — Identify the Preconditions (What Must Be True Before)

Ask yourself: what inputs would break this method? A grade below 0 or above 100 makes no sense. Also, passing a null student name would be invalid. So our preconditions are: grade >= 0 and grade <= 100.

Preconditions: 0 <= grade <= 100
2
Step 2 — Identify the Postconditions (What Must Be True After)

After the method runs, the list of grades should contain one more element than before. The new element should equal the grade that was passed in. The returned average should equal the sum of all grades divided by the count of grades.

Postconditions: grades.size() == oldSize + 1 and return value equals the correct average
3
Step 3 — Identify the Class Invariant

What must always be true about a StudentGradeBook? The list of grades should never be null. Every grade in the list should be between 0 and 100. The computed average should always be between 0 and 100 as well (or undefined if no grades exist).

Invariant: grades != null and all elements are in [0, 100]
4
Step 4 — Write the Javadoc

Now translate these conditions into Javadoc: @param grade the grade to add, must be between 0 and 100 inclusive, @return the updated average of all grades, and @throws IllegalArgumentException if grade < 0 or grade > 100.
5
Step 5 — Write the Guard Clauses and Asserts

At the top of the method, add: if (grade < 0 || grade > 100) throw new IllegalArgumentException("Grade must be 0–100");. After the logic, add: assert grades.size() == oldSize + 1; for the postcondition and assert grades.stream().allMatch(g -> g >= 0 && g <= 100); for the invariant.

Complete contract: Javadoc + guard clause + postcondition assert + invariant assert

💡

Pro Tip

Always write the contract before you write the method body. Thinking about preconditions and postconditions first forces you to understand the problem clearly, which leads to cleaner, simpler code.

SECTION 7

Strengths & Limitations of Method Contracts

Method contracts are powerful, but like any tool they have tradeoffs. Understanding when contracts shine and where they have limitations will help you apply them effectively in your Java projects.

Strengths	Limitations
Catches bugs early — precondition checks fail immediately at the source of the problem, not deep inside unrelated code.	Adds lines of code — guard clauses and asserts make methods longer, which may feel like overhead in small programs.
Serves as documentation — the contract tells other programmers exactly how to use the method correctly.	Java lacks native contract syntax — unlike Eiffel, Java relies on manual coding, so contracts can be inconsistent if programmers forget them.
Assigns clear blame — when a test fails, you immediately know whether the bug is in the caller or the method.	Assert statements are disabled by default — you must remember to run with `-ea` to activate assert checks.
Improves teamwork — when multiple people work on a codebase, contracts prevent misunderstandings about method usage.	Complex invariants can be expensive to verify — checking every element of a large list after every method call has performance costs.

Tradeoffs of using method contracts in Java

✦

KEY TAKEAWAY

Method contracts are like seat belts in a car. They add a small step every time you drive, and most of the time you do not "need" them. But the one time something goes wrong, they save you from a catastrophic crash. The cost of writing contracts is tiny compared to the hours you would spend hunting down a mysterious NullPointerException without them.

SECTION 8

Connection to Advanced Software Design

Method contracts are your first step into a much larger world of software correctness. As you advance, you will encounter tools and ideas that build directly on the foundation you have learned here. The table below shows how the basic concepts you now know connect to more advanced techniques used in professional software engineering.

What You Know Now	Advanced Version	Where You'll See It
Precondition guard clauses with `if` statements	Annotation-based validation (`@NotNull`, `@Min`, `@Max`)	Spring Framework, Jakarta Bean Validation
Postcondition asserts	Unit testing frameworks (JUnit) that verify outcomes automatically	AP CS A and professional codebases
Class invariants checked by asserts	Property-based testing that generates thousands of random inputs to stress-test invariants	Libraries like jqwik and QuickCheck
Javadoc contract documentation	Formal specification languages (JML — Java Modeling Language)	University CS courses, safety-critical systems

From beginner contracts to advanced software correctness

One particularly important principle that grows from contracts is the Liskov Substitution Principle (LSP). It states that if a subclass overrides a method, the subclass must not strengthen preconditions (demand more from the caller) and must not weaken postconditions (promise less). In other words, a subclass must honor its parent's contract. You will study this in depth when you learn about inheritance and polymorphism, and the contract vocabulary you have built here will make it much easier to understand.

SECTION 9

Practice Problems

Question 1: CONCEPTUAL

A method called divide(int a, int b) returns the integer result of a / b. What is the most important precondition for this method, and why? Who is responsible for making sure this precondition is met — the caller or the method?

Show answer

The most important precondition is b != 0 because dividing by zero is undefined and would cause an ArithmeticException at runtime. The caller is responsible for satisfying this precondition. The method should document this requirement in its Javadoc using @throws IllegalArgumentException if b is 0, and it should include a guard clause: if (b == 0) throw new IllegalArgumentException("divisor cannot be zero");.

Question 2: BASIC

Write the Javadoc comment (including @param, @return, and @throws tags) for a method setAge(int age) that sets a person's age. The age must be between 0 and 150 inclusive.

Show answer

A correct Javadoc would be:

/** Sets the age of this person. @param age the person's age; must be between 0 and 150 inclusive @throws IllegalArgumentException if age < 0 or age > 150 */

. Notice there is no @return tag because a setter typically returns void. The Javadoc clearly states the valid range (the precondition) and what exception is thrown on violation, giving the caller all the information they need to use the method correctly.

Question 3: INTERMEDIATE

Consider a Stack class with a pop() method. State the precondition, postcondition, and one class invariant. Then write the guard clause and assert statements in Java that enforce them.

Show answer

Precondition: the stack must not be empty (size() > 0). Postcondition: after pop, size() == oldSize − 1 and the returned value is the element that was on top. Class invariant: size() >= 0 (the size can never be negative). The guard clause is: if (isEmpty()) throw new IllegalStateException("Cannot pop from empty stack");. The postcondition assert is: assert size() == oldSize - 1;. The invariant assert is: assert size() >= 0 : "Invariant violated: negative size";. Note we use IllegalStateException here instead of IllegalArgumentException because the problem is the object's state, not a bad argument.

Question 4: APPLIED

You are building a TemperatureConverter class. The method celsiusToFahrenheit(double celsius) converts a Celsius temperature to Fahrenheit. Absolute zero is −273.15°C. Write the complete method contract including Javadoc, a guard clause, and an assert statement for the postcondition that fahrenheit = celsius × 9/5 + 32.

Show answer

The Javadoc states:

/** Converts Celsius to Fahrenheit. @param celsius temperature in Celsius; must be >= -273.15 @return the equivalent temperature in Fahrenheit @throws IllegalArgumentException if celsius < -273.15 */

. The guard clause is: if (celsius < -273.15) throw new IllegalArgumentException("Temperature below absolute zero");. The method body computes double fahrenheit = celsius * 9.0 / 5.0 + 32;. The postcondition assert uses a small tolerance for floating-point comparison: assert Math.abs(fahrenheit - (celsius * 9.0/5.0 + 32)) < 0.001;. This is a real-world example of how contracts can involve physical constraints (absolute zero) and mathematical precision (floating-point tolerance).

Question 5: CRITICAL THINKING

A teammate writes a SavingsAccount subclass that extends BankAccount. Their overridden withdraw method adds a new precondition: the balance after withdrawal must be at least $100 (a minimum balance requirement). Does this violate the parent class's contract? Explain your reasoning using the concepts of preconditions, postconditions, and the Liskov Substitution Principle.

Show answer

Yes, this violates the parent class's contract and the Liskov Substitution Principle. The parent BankAccount.withdraw allows any withdrawal where amount <= balance and amount > 0. The subclass adds a stronger precondition (balance after withdrawal must be at least $100), which means some calls that would succeed on the parent will fail on the subclass. This breaks substitutability — code written to work with a BankAccount would unexpectedly fail when handed a SavingsAccount. A better design would make the minimum balance part of the class invariant (e.g., balance >= 100) and have the parent's precondition check reference the invariant, so both classes share a consistent contract.

SUMMARY

Summary — Method Contracts & Invariants

Summary

A method contract is a formal agreement between the caller and the method. It consists of three parts: preconditions (what must be true before the method runs — the caller's responsibility), postconditions (what the method guarantees when it finishes — the implementer's responsibility), and invariants (what must always remain true about the object's state). In Java, contracts are communicated through Javadoc comments and enforced through guard clauses (which throw exceptions for bad input) and assert statements (which verify postconditions and invariants during development).

Writing contracts before you write code forces you to think clearly about valid inputs, expected outputs, and object consistency. This practice — rooted in Design by Contract principles from the 1980s — prevents bugs, makes debugging easier by assigning clear responsibility, and creates self-documenting code that teammates can rely on. As you advance, these ideas will connect directly to unit testing, annotation-based validation, and the Liskov Substitution Principle — the rule that subclasses must never break their parent class's contract.