Reasoning About Method Calls in Interface
Specifications
Ádám Darvas and Peter
Müller, ETH Zurich,
Switzerland
|
 |
REFEREED
ARTICLE
PDF Version |
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/issues
2006 06/article3
|
