Initialize Unknown States

[rcosta358]

Description

This PR initializes object instances with their default typestate (first state from each state set) when their refinement is unknown (true).

This fixes cases we try to verify an object without an explicit constructor invocation.
Also, this also improves external refinement interfaces that do not declare a constructor method.
Previously, this was required:

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

With this change, this is now optional.

Examples

No Explicit Constructor Call

ImageWriteParam param = writer.getDefaultWriteParam(); // state1(this) == 0 (start)
if (param.canWriteCompressed()) {
    param.setCompressionMode(ImageWriteParam.MODE_EXPLICIT);
    param.setCompressionQuality(0.5f);
}

Previously, param.canWriteCompressed() would fail because param had unknown state (true) and it required it to be in either start() or !start(), but each was checked separately since they are from different state refinements.
Now param is initialized with the default start state.

No Explicit Constructor Declaration

@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); // state1(this) == 0 (open)
        isr.read();
        isr.close();
    }
}

Previously, isr.read() would fail because isr had unknown state (true).
Now isr is initialized with the default open state.

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