Reasoning About Method Calls in Interface Specifications

Abstract

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 l.janguage expressions in a program logic. This encoding is non-trivial for method calls. This paper illustrates the subtle problems any encoding of method calls in specifications has to address. The paper gives sound encoding that allows side-effect free methods to create and initialize objects by explicitly modeling such modifications of the heap.

Cite as:

Adam Darvas, Peter Müller, “Reasoning About Method Calls in Interface Specifications”, Journal of Object Technology, Volume 5, no. 5 (June 2006), pp. 59-85, doi:10.5381/jot.2006.5.5.a3.