Add Missing this Binding + Method Checking Ordering

[rcosta358]

Closes #78.

Add Missing this Binding

Fixes the error Variable 'this' not found when a method combined a state refinement with a parameter refinement that referenced this. Fixed this by adding this to the context in AuxStateHandler.createStatePredicate.

Method Checking Ordering

This PR also fixes invocation parameter refinement checking to use the receiver’s pre-call state instead of its post-call state, which means the order of checking a parameter is now check pre-conditions -> check parameter refinements -> update with post-conditions. This keeps the existing state transition behavior, but delays applying it until after parameter validation.

Why?

In the following example, in the update method, the parameter refinement percentage > progress(this) should be checked against the receiver's state before the call. Instead, the verifier was applying the receiver state transition first and only then validating the parameter refinement, which meant the condition was always false (x > x => false ).

@Ghost("int progress")
@StateSet({"created", "downloading", "completed"})
public class Downloader {

    @StateRefinement(to="created(this) && progress(this) == 0")
    public Downloader() {}

    @StateRefinement(from="created(this) && progress(this) == 0", to="downloading(this) && progress(this) == 0")
    public void start() {}

    @StateRefinement(from="downloading(this)", to="downloading(this) && progress(this) == percentage")
    public void update(@Refinement("percentage > progress(this)") int percentage) {}

    @StateRefinement(from="downloading(this) && progress(this) == 100", to="completed(this)")
    public void finish() {}
}

[CatarinaGamboa]

Let's just add some tests that actually exercise the state, along with the ghost just to check, that verification actually supports this