Return implies state

[CatarinaGamboa]

Description

Allow observer methods to give information about the object state.

Example

In refinements allow observers to mention the object state.

@StateSet({"hasMore", "noMore"})
@ExternalRefinementsFor("java.util.Scanner")
public interface IteratorRefinements {

    @Refinement("_ == true --> hasMore(this)")
    boolean hasNext();

    @StateRefinement(from = "hasMore(this)", to = "noMore(this)") // addition
    String next();
}

Client code:

    public static void readOne(Scanner it) {
        if (it.hasNext()) {
            it.next(); // allow
        }
    }

    public static void nextNotInElse(Scanner it) {
        if (!it.hasNext()) {
            it.next(); // State Refinement Error
        }
    }

Type of change

• Bug fix
• New feature
• Documentation update
• Code refactoring

Checklist

• Added/updated tests under liquidjava-example/src/main/java/testSuite/ (Correct* / Error*)
• mvn test passes locally
• Updated docs/README if behavior or API changed