Fix this Resolution in Parameter Refinements

[rcosta358]

Fixed issue where this references in parameter refinements were not resolved, because they weren’t being substituted with the specific object on which the method was invoked.

Now we can actually catch index out-of-bounds errors! 😄

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

    public void ArrayList();

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

	// this refinement previously caused the error "Variable 'this' not found"
	public E get(@Refinement("_ < size(this)") int index); 
}

public class Test {
    public static void main(String[] args) {
        ArrayList<Integer> list = new ArrayList<>();
        list.get(0); // refinement error!
    }
}

[CatarinaGamboa]

Cool!