Reasoning About Reference Behavior with RESOLVE.

As an alternative to reasoning about references explicitly and ACM SIGSOFT Software Engineering Notes Page 18 July 2018 Volume 43 Number 3 routinely as needed for Java-like programs, this paper summarizes the RESOLVE approach in reasoning via reference-hiding data abstractions for the majority of programs and only reasoning about references when they are unavoidable. Furthermore, this paper raises discussion topics for reasoning about various implementation classifications and to explore when there is a need to be concerned about establishing the frame property