Add Ghost Dot Syntax

[rcosta358]

This PR adds support for dot syntax in ghosts and states while keeping it backward compatible with the previous syntax. For this, a new non-terminal dotCall was added to the grammar and implemented in the AST visitor.

Currently, all of these equivalent: size(this), this.size(), and size(). To refer to the previous value of size, we can either use size(old(this)) or old(this).size.

In the future, we plan to drop the functional syntax and only keep the dot syntax to avoid ambiguity and confusion.

Example

@Ghost("int n")
public class CorrectDotNotationIncrementOnce {

    // explicit this
    @StateRefinement(to="this.n() == 0")
    public CorrectDotNotationIncrementOnce() {}

    // implicit this
    @StateRefinement(from="n() == 0", to="n() == old(this).n() + 1")
    public void incrementOnce() {}
}