Verifying Generics and Delegates
Recently, object-oriented languages, such as C#, have been extended with language features prevalent in most functional languages: parametric polymorphism and higher-order functions. In the OO world these are called generics and delegates, respectively. These features allow for greater code reuse and reduce the possibilities for run-time errors. However, the combination of these features pushes the language beyond current object-oriented verification techniques. In this paper, the authors address this by extending a higher-order separation logic with new assertions for reasoning about delegates and variables.