A modular verification methodology for C# delegates

Abstract

Function objects are used to express higher-order features in object-oriented programs. C# provides the delegate construct to simplify the implementation of function objects. A delegate instance represents a method together with a target object. Sound reasoning about delegates requires that the precondition of the underlying method holds whenever a delegate is invoked. This is difficult to achieve if the method precondition depends on the state of the target object. Proving such a precondition when the delegate is invoked is in general not possible because properties of the target object are typically not known at the invocation site. Proving the precondition when the delegate is instantiated is not sufficient either because the state of the target might change before the delegate is invoked. In this paper, we present a verification methodology for C# delegates. Properties of the target object are expressed as invariant of the delegate. Our methodology keeps track when this invariant can be assumed to hold. It enables modular verification of interesting implementations and is proven sound. © 2009 Springer-Verlag.