Set this As Default Argument in Ghost Invocations

[rcosta358]

Previously, if a ghost invocation had no arguments, we would get the error Index 0 out of bounds for length 0.

Instead of giving the user a better error message, what if we set this as the default argument for ghost invocations, when none is provided? Most of the time, this is the one we intend to use, so this would be an improvement.

This way, we can write simpler and easier to read refinements:

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

    public void ArrayList();

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

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

This was done by checking if the arguments are empty in the parser and if so add the variable this to the list.

[alcides]

Just for the record:

Java does this with m() being a short-hand version of this.m(). In this case, the elements between parentheses are exactly the same.

Here, the idea is that m() is the same as m(this), which kind of changes the things between parentheses, having the potential of being a source of confusion for reading and writing refinements.

On one hand, if we end up implementing dot-syntax for refinements (I usually think it's a good idea), the "this" makes sense before the "."

But if we have non-interpreted functions as "functions", then adding an extra parameter when having zero elements syntactically seems a bit off to me.

[rcosta358]

We can change the syntax then, if everyone agrees.

[rcosta358]

What do you think @CatarinaGamboa?