Design by Contract

---

Definition

---

Contract Examples

/**
 * Withdraws money from account.
 *
 * @param amount the amount to withdraw
 *
 * @precondition amount > 0
 * @precondition amount <= getBalance()
 *
 * @postcondition getBalance() == old(getBalance()) - amount
 * @postcondition result == true
 *
 * @throws IllegalArgumentException if amount <= 0
 * @throws InsufficientFundsException if amount > getBalance()
 */
public boolean withdraw(Money amount) {
    // Check preconditions
    if (amount.isNegativeOrZero()) {
        throw new IllegalArgumentException("Amount must be positive");
    }
    if (amount.isGreaterThan(balance)) {
        throw new InsufficientFundsException(amount, balance);
    }

    // Perform operation
    Money oldBalance = balance;
    balance = balance.subtract(amount);

    // Assert postcondition (development mode)
    assert balance.equals(oldBalance.subtract(amount))
        : "Balance invariant violated";

    return true;
}

/**
 * Class invariant: balance >= 0 at all times
 */
public class BankAccount {
    private Money balance;

    private void checkInvariant() {
        assert balance.isNonNegative() : "Balance cannot be negative";
    }
}

---

Preconditions

// Preconditions: What caller must satisfy

public class Stack<E> {
    private Object[] elements;
    private int size;

    /**
     * Pops and returns the top element.
     *
     * @precondition !isEmpty()
     * @return the top element
     * @throws EmptyStackException if stack is empty
     */
    public E pop() {
        // Validate precondition
        if (isEmpty()) {
            throw new EmptyStackException();
        }

        @SuppressWarnings("unchecked")
        E result = (E) elements[--size];
        elements[size] = null;  // Help GC
        return result;
    }
}

// Modern Java approach: Objects utility methods
public class ArrayUtils {

    public static <T> void sort(T[] array, Comparator<T> comparator) {
        // Validate preconditions
        Objects.requireNonNull(array, "array cannot be null");
        Objects.requireNonNull(comparator, "comparator cannot be null");

        // Proceed with operation
        Arrays.sort(array, comparator);
    }
}

// Using Guava Preconditions
public void setAge(int age) {
    Preconditions.checkArgument(age >= 0, "age must be non-negative: %s", age);
    Preconditions.checkArgument(age < 150, "age must be realistic: %s", age);
    this.age = age;
}

---

Postconditions

// Postconditions: What method guarantees

public class SortedList<E extends Comparable<E>> {

    /**
     * Adds element maintaining sorted order.
     *
     * @postcondition contains(element) == true
     * @postcondition isSorted() == true
     * @postcondition size() == old(size()) + 1
     */
    public void add(E element) {
        int index = findInsertionPoint(element);
        list.add(index, element);

        // Development-time postcondition check
        assert contains(element) : "Element should be in list";
        assert isSorted() : "List should remain sorted";
    }

    private boolean isSorted() {
        for (int i = 1; i < list.size(); i++) {
            if (list.get(i-1).compareTo(list.get(i)) > 0) {
                return false;
            }
        }
        return true;
    }
}

// Postcondition with return value
public class MathUtils {

    /**
     * @postcondition result >= 0
     * @postcondition result * result <= n
     * @postcondition (result + 1) * (result + 1) > n
     */
    public static int sqrt(int n) {
        if (n < 0) {
            throw new IllegalArgumentException("n must be non-negative");
        }

        int result = (int) Math.sqrt(n);

        assert result >= 0 : "Result must be non-negative";
        assert result * result <= n : "Result squared must not exceed n";

        return result;
    }
}

---

Class Invariants

// Invariants: Always true for valid object state

public class DateRange {
    private LocalDate start;
    private LocalDate end;

    /**
     * Invariant: start <= end
     */
    public DateRange(LocalDate start, LocalDate end) {
        Objects.requireNonNull(start);
        Objects.requireNonNull(end);

        if (end.isBefore(start)) {
            throw new IllegalArgumentException(
                "End date must not be before start date");
        }

        this.start = start;
        this.end = end;

        checkInvariant();
    }

    public void setEnd(LocalDate newEnd) {
        Objects.requireNonNull(newEnd);

        if (newEnd.isBefore(start)) {
            throw new IllegalArgumentException(
                "End date must not be before start date");
        }

        this.end = newEnd;

        checkInvariant();  // Verify after mutation
    }

    private void checkInvariant() {
        assert !end.isBefore(start) : "Invariant violated: end < start";
    }
}

// Invariants can be checked by framework
@Validated
public class Account {
    @AssertTrue(message = "Balance must be non-negative")
    public boolean isBalanceValid() {
        return balance.compareTo(BigDecimal.ZERO) >= 0;
    }
}

---

Contract Inheritance (LSP)

---

Implementing Contracts

// Modern approaches to Design by Contract

// 1. Assertions (development only)
public void deposit(Money amount) {
    assert amount.isPositive() : "Precondition: amount must be positive";

    Money oldBalance = balance;
    balance = balance.add(amount);

    assert balance.equals(oldBalance.add(amount)) : "Postcondition failed";
}

// 2. Bean Validation
public class TransferRequest {
    @NotNull
    @Positive
    private BigDecimal amount;

    @NotNull
    @Pattern(regexp = "^[A-Z]{3}$")
    private String currency;

    @NotBlank
    private String targetAccount;
}

@Validated
public interface TransferService {
    void transfer(@Valid TransferRequest request);
}

// 3. Explicit validation
public class Guard {
    public static <T> T requireNonNull(T obj, String message) {
        if (obj == null) {
            throw new IllegalArgumentException(message);
        }
        return obj;
    }

    public static void require(boolean condition, String message) {
        if (!condition) {
            throw new IllegalArgumentException(message);
        }
    }

    public static void ensure(boolean condition, String message) {
        if (!condition) {
            throw new IllegalStateException(message);
        }
    }
}

public void process(Order order) {
    Guard.requireNonNull(order, "order is required");
    Guard.require(order.hasItems(), "order must have items");

    // ... process ...

    Guard.ensure(order.isProcessed(), "order should be processed");
}

---

Tips & Tricks

---