Implicit Constructor Refinements

[rcosta358]

Description

This PR allows external refinement interfaces to omit constructor declarations while still correctly initializing typestate and ghost information, which previously was impossible:

Constructors must always be present for typestate checking to work correctly, because they are the point where the initial state values are assigned. Otherwise, the initial values are not set and the verifier won’t be able to track the state of the object across method calls. liquidjava-docs

Example

@ExternalRefinementsFor("java.io.InputStreamReader")
@StateSet({"open", "closed"})
public interface InputStreamReaderRefinements {

    // public void InputStreamReader(InputStream in);

    @StateRefinement(from = "open(this)")
    int read();

    @StateRefinement(from = "open(this)", to = "closed(this)")
    void close();

    public static void main(String[] args) throws IOException {
        InputStreamReader isr = new InputStreamReader(System.in);
        isr.read();
        isr.close();
    }
}

Previously, isr.read() would fail because isr was initialized with an unknown state (true) when no constructor declaration was present.

Now, objects are automatically initialized with their default states, allowing the verification to work correctly even when constructors are omitted.

Related Issue

None.

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