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 runtime errors. However, the combination of these features pushes the language beyond current object-oriented verification techniques. In this paper, we address this by extending a higher-order separation logic with new assertions for reasoning about delegates and variables. We faithfully capture the semantics of C delegates including their capture of the l-value of a variable, and that "stack" variables can live beyond their "scope". We demonstrate that our logic is sound and illustrate its use by specifying and verifying a series of interesting and challenging examples. © 2010 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Svendsen, K., Birkedal, L., & Parkinson, M. (2010). Verifying generics and delegates. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6183 LNCS, pp. 175–199). https://doi.org/10.1007/978-3-642-14107-2_9
Mendeley helps you to discover research relevant for your work.