Portal de Periódicos da CAPES

Reasoning About Method Calls in Interface Specifications.

2006; EtH Zurich; Volume: 5; Issue: 5 Linguagem: Inglês

10.5381/jot.2006.5.5.a3

1660-1769

Ádám Darvas, Péter Müller,

Software Testing and Debugging Techniques

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.