Reasoning About Method Calls in Interface Specifications

Ádám Darvas and Peter Müller, ETH Zurich, Switzerland

REFEREED
ARTICLE

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 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.

Note: Due to the typographical sophistication of this article, no HTML version is available. Please use the PDF version.

About the authors

		Ádám Darvas is PhD student at ETH Zurich. He works on semantics of modular specification languages and on the development of the Jive verification tool. Email: adam.darvas@inf.ethz.ch.
		Peter Müller is assistant professor and head of the Software Component Technology Group at ETH Zurich. His research focuses on specification and verification of object-oriented software. Email: peter.mueller@inf.ethz.ch.

Cite this article as follows: : Reasoning About Method Calls in Interface Specifications, in Journal of Object Technology, vol. 05, no. 5, Special Issue: ECOOP 2005 Workshop FTfJP, June 2006, pages 59–85, http://www.jot.fm/issues/issue_2006_06/article3

outlook