ArrayList

This example refines the java.util.ArrayList standard-library class without modifying its source code. A ghost variable tracks the size of the list, and a parameter refinement prevents out-of-bounds accesses.

import liquidjava.specification.*;

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

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

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

ArrayList<String> list = new ArrayList<>();
list.add("apple");
list.get(0);
list.get(1); // Refinement Error

The key idea is that LiquidJava turns the usual runtime condition for get(i) into a static precondition over the tracked size ghost variable.