Reasoning about Function Objects
METADATA ONLY
Loading...
Author / Producer
Date
2010
Publication Type
Conference Paper
ETH Bibliography
yes
Citations
Altmetric
METADATA ONLY
Data
Rights / License
Abstract
Modern object-oriented languages support higher-order implementations through function objects such as delegates in C#, agents in Eiffel, or closures in Scala. Function objects bring a new level of abstraction to the object-oriented programming model, and require a comparable extension to specification and verification techniques. We introduce a verification methodology that extends function objects with auxiliary side-effect free (pure) methods to model logical artifacts: preconditions, postconditions and modifies clauses. These pure methods can be used to specify client code abstractly, that is, independently from specific instantiations of the function objects. To demonstrate the feasibility of our approach, we have implemented an automatic prover, which verifies several non-trivial examples.
Permanent link
Publication status
published
External links
Editor
Book title
Objects, Models, Components, Patterns
Journal / series
Volume
6141
Pages / Article No.
79 - 96
Publisher
Springer
Event
48th International Conference on Objects, Models, Components, Patterns (TOOLS 2010)
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Organisational unit
03653 - Müller, Peter / Müller, Peter