Data abstraction specifiers are used to describe the behavior of methods without specifying implementation details. When writing REQUIRES, MODIFIES, and EFFECTS clauses, you should never refer to specific fields of the class.

They help clarify what a method requires, what it modifies, and what effects it produces. These specifiers ensure that method behavior is well-documented, making the code easier to understand and maintain.

INVARIANT

When designing a class that maintains related data in multiple structures (e.g., two lists storing related information), it is important to ensure consistency throughout the class. This consistency is enforced through a class invariant—a condition that must always hold true for a valid object.

Example

import java.util.ArrayList;
import java.util.List;

/**
 * INVARIANT: courseList and gradeList are always the same size;
 *            each course has an associated grade, and vice versa, at 
 *            matching indices.
 */
public class StudentTranscript {
    private List<String> courseList;
    private List<Double> gradeList;

    public StudentTranscript() {
        this.courseList = new ArrayList<>();
        this.gradeList = new ArrayList<>();
    }
}

Because course info is stored in two separate lists, courseList and gradeList we need to specify an INVARIANT for the class.

REQUIRES

Specifies a condition that must be true before the method is called for it to function correctly. If the condition is not met, the method's behavior is undefined.

Example

// REQUIRES: age >= 0
public void setAge(int age) {
    this.age = age;
}

The method setAge expects age to be non-negative before being called.

MODIFIES

Specifies which objects (if any) are modified by the method, with the modification persisting after the method ends. If no objects are modified, this specifier is omitted.

Example

// MODIFIES: this
public void incrementAge() {
    this.age += 1;
}

The method incrementAge modifies the object's age field.

EFFECTS

Describes what the method does when called, without detailing how it is implemented. This includes return values, exceptions thrown, and observable behavior.

Example

// EFFECTS: Returns the age multiplied by 7 (dog years)
public int getAgeInDogYears() {
    return this.age * 7;
}

The method getAgeInDogYears returns the dog's age in dog years.

Complete Example

We have a BankAccount class that allows depositing, withdrawing, and transferring money between accounts. The method transferTo moves funds from one account to another while ensuring the transfer is valid.

public class BankAccount {
    private double balance;
    private String owner;

	// REQUIRES: initialBalance >= 0
    // EFFECTS: Constructs a new bank account with an owner
    //          and balance
    public BankAccount(String owner, double initialBalance) {
        this.owner = owner;
        this.balance = initialBalance;
    }

    // REQUIRES: amount > 0
    // MODIFIES: this
    // EFFECTS: Adds the given amount to the balance
    public void deposit(double amount) {
        this.balance += amount;
    }

    // REQUIRES: amount > 0 && amount <= balance
    // MODIFIES: this
    // EFFECTS: Deducts the given amount from the balance
    public void withdraw(double amount) {
        this.balance -= amount;
    }

    // REQUIRES: amount > 0 && amount <= this.balance
    // MODIFIES: this, recipient
    // EFFECTS: Transfers the given amount from this account to 
    //          recipient
    public void transferTo(BankAccount recipient, double amount) {
        this.withdraw(amount);
        recipient.deposit(amount);
    }

    // EFFECTS: Returns the current balance of the account
    public double getBalance() {
        return this.balance;
    }

    // EFFECTS: Returns the name of the account owner
    public String getOwner() {
        return this.owner;
    }
}

Explanation

1. BankAccount(String owner, double initialBalance) (constructor)

• REQUIRES: initialBalance >= 0 (a bank account cannot have a negative starting balance)
• EFFECTS: Initializes a new bank account with the given owner and starting balance

2. deposit(double amount)

• REQUIRES: amount > 0 (the deposit must be a positive amount)
• MODIFIES: this (the current account balance changes)
• EFFECTS: Increases the balance by the deposit amount

3. withdraw(double amount)

• REQUIRES: amount > 0 && amount <= balance (the withdrawal must be positive and within available funds)
• MODIFIES: this (the current account balance decreases)
• EFFECTS: Reduces the balance by the withdrawal amount

4. transferTo(BankAccount recipient, double amount)

• REQUIRES: amount > 0 && amount <= this.balance (the transfer must be a positive amount within available funds)
• MODIFIES: this, recipient (both the sender and recipient balances change)
• EFFECTS: Deducts amount from this account and adds it to the recipient’s balance

5. getBalance() And getOwner()

• EFFECTS: Simply return information without modifying the object