Reasoning about Function Objects

Abstract

Modern object-oriented languages support higher-order implementations through function objects such as delegates in C#, agents in Eiffel, or function objects 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 equips each function object with side-effect free (pure) methods for its pre- and postcondition, respectively. These pure methods can be used to specify client code relatively to the contract of the function object. We demonstrate the expressiveness of our approach through several non-trivial examples. It can be combined with any verification technique that supports pure methods, as illustrated by our experiments with Spec#.