Summary

A method whose parameter refinement mentions the receiver's ghost (index < size(this)) fails with Not Found Error: Variable 'this' could not be found when it is called on another call's result, as in m.get("k").get(0). With a local variable in between, the verifier reports the expected refinement error (the receiver's size is unknown), so only the chained form breaks.

Minimal reproducer

ArrayListRefinements.java:

import liquidjava.specification.ExternalRefinementsFor;
import liquidjava.specification.Ghost;
import liquidjava.specification.Refinement;
import liquidjava.specification.StateRefinement;

@ExternalRefinementsFor("java.util.ArrayList")
@Ghost("int size")
public interface ArrayListRefinements<E> {
    @StateRefinement(to = "size(this) == 0")
    void ArrayList();

    @StateRefinement(to = "size(this) == size(old(this)) + 1")
    boolean add(E e);

    E get(@Refinement("_ >= 0 && _ < size(this)") int index);

    @Refinement("_ == size(this) && _ >= 0")
    int size();
}

Client.java:

import java.util.ArrayList;
import java.util.HashMap;

public class Client {
    public static void main(String[] args) {
        HashMap<String, ArrayList<String>> m = new HashMap<>();
        ArrayList<String> l = new ArrayList<>();
        l.add("a");
        m.put("k", l);
        String s = m.get("k").get(0);   // Not Found Error: Variable 'this' could not be found
    }
}

Expected: a refinement error at get(0) (the list comes from HashMap.get, so its size is unknown), the same one the verifier gives for ArrayList<String> x = m.get("k"); x.get(0);: index == 0 is not a subtype of index >= 0 && index < size(x).

Seen on 1a506fe and main at 19991d3.

Why it matters: real code

Chained reads from a map of lists are common. One of five mined GitHub methods using ArrayList does this: Minimum-Vertex-Cover MVC.readGraph, while (lineNum <= Integer.parseInt(result.get("0").get(0))). The error stops verification of the whole method, and its message points at this, which the user never wrote.

Found while checking mined client code against JDK specs (liquid-java/co-specification, verifier probe V38).