Abstract
Recently, object-oriented languages, such as C\(^\sharp\), 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\(^\sharp\) 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., Hähnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. Software and System Modeling 4, 32–54 (2005)
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec\(^\sharp\) programming system: An overview. In: CASSIS, pp. 49–69 (2005)
Biering, B., Birkedal, L., Torp-Smith, N.: Bi hyperdoctrines and higher-order separation logic. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 233–247. Springer, Heidelberg (2005)
Bornat, R., Calcagno, C., O’Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In: Proceedings of POPL, pp. 259–270 (2005)
Bornat, R., Calcagno, C., Yang, H.: Variables as resources in separation logic. In: Proceedings of MFPS, pp. 125–146 (2005)
Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. In: FMICS, pp. 73–89 (2003)
Distefano, D., Parkinson, M.J.: jstar: towards practical verification for java. In: OOPSLA, pp. 213–226 (2008)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: PLDI, pp. 234–245 (2002)
Krishnaswami, N.R., Aldrich, J., Birkedal, L., Svendsen, K., Buisse, A.: Design patterns in separation logic. In: Proceedings of TLDI 2009, pp. 105–116 (2009)
Müller, P., Ruskiewicz, J.N.: A modular verification methodology for C# delegates. In: Glässer, U., Abrial, J.-R. (eds.) Rigorous Methods for Software Construction and Analysis (2007) ( to appear)
Nanevski, A., Ahmed, A., Morrisett, G., Birkedal, L.: Abstract predicates and mutable adts in hoare type theory. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 189–204. Springer, Heidelberg (2007)
Nordio, M., Calcagno, C., Meyer, B., Müller, P.: Reasoning about function objects. Technical Report 615, ETH Zurich (2009)
O’Hearn, P.W.: Resources, concurrency and local reasoning. Theor. Comput. Sci. 375(1-3), 271–307 (2007)
Parkinson, M.: Local Reasoning for Java. PhD thesis, University of Cambridge (November 2005)
Parkinson, M., Bierman, G.: Separation logic, abstraction and inheritance. In: ACM Symposium on Principles of Programming Languages (POPL 2008). ACM Press, New York (January 2008)
Parkinson, M.J., Bierman, G.M.: Separation logic and abstraction. In: Proceedings of POPL, pp. 247–258 (2005)
Parkinson, M.J., Bornat, R., Calcagno, C.: Variables as resource in Hoare logic. In: Proceedings of LICS, pp. 137–146. IEEE, Los Alamitos (2006)
Petersen, R.L., Birkedal, L., Nanevski, A., Morrisett, G.: A realizability model for impredicative hoare type theory. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 337–352. Springer, Heidelberg (2008)
Schwinghammer, J., Birkedal, L., Reus, B., Yang, H.: Nested hoare triples and frame rules for higher-order store. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 440–454. Springer, Heidelberg (2009)
Svendsen, K., Birkedal, L., Parkinson, M.: Verifying generics and delegates (technical appendix). Technical report (2009), http://www.itu.dk/people/kasv/generics-delegates-tr.pdf
Yoshida, N., Honda, K., Berger, M.: Logical reasoning for higher-order functions with local state. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 361–377. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Svendsen, K., Birkedal, L., Parkinson, M. (2010). Verifying Generics and Delegates. In: D’Hondt, T. (eds) ECOOP 2010 – Object-Oriented Programming. ECOOP 2010. Lecture Notes in Computer Science, vol 6183. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14107-2_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-14107-2_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14106-5
Online ISBN: 978-3-642-14107-2
eBook Packages: Computer ScienceComputer Science (R0)