Reasoning About Method Calls in Interface Specifications.
Ádám Darvas, Péter Müller · The Journal of Object Technology · 2006
Interface specifications in languages such as Eiffel, the Java Modeling Language (JML), and Spec# are based on side-effect free expressions of the programming language.In particular, such specifications contain calls to side-effect free methods to describe the program behavior without exposing implementation details.Reasoning about such specifications requires an encoding of programming language expressions in a program logic.This encoding is non-trivial for method calls.In this paper, we illustrate the subtle problems any encoding of method calls in specifications has to address.We present a sound encoding that allows side-effect free methods to create and initialize objects by explicitly modeling such modifications of the heap.