Abstract
Modern object-oriented languages support higher-order implementations through function objects such as delegates in C#, agents in Eiffel, or closures 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 extends function objects with auxiliary side-effect free (pure) methods to model logical artifacts: preconditions, postconditions and modifies clauses. These pure methods can be used to specify client code abstractly, that is, independently from specific instantiations of the function objects. To demonstrate the feasibility of our approach, we have implemented an automatic prover, which verifies several non-trivial 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
Banerjee, A., Naumann, D., Rosenberg, S.: Regional Logic for Local Reasoning about Global Invariants. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 387–411. Springer, Heidelberg (2008)
Barnett, M., Leino, R., Schulte, W.: The Spec# Programming System: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)
Berger, M., Honda, K., Yoshida, N.: A logical analysis of aliasing in imperative higher-order functions. In: ICFP ’05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, pp. 280–293. ACM, New York (2005)
Biering, B., Birkedal, L., Torp-Smith, N.: BI-hyperdoctrines, higher-order separation logic, and abstraction. In: ToPLAS (2008)
Börger, E., Fruja, N.G., Gervasi, V., Stärk, R.F.: A high-level modular definition of the semantics of C#. Theor. Comput. Sci. 336(2-3), 235–284 (2005)
Clarke, D., Drossopoulou, S.: Ownership, encapsulation and the disjointness of type and effect. In: OOPSLA ’02, vol. 37, pp. 292–310. ACM Press, New York (2002)
Darvas, Á.: Reasoning About Data Abstraction in Contract Languages. PhD thesis, ETH Zurich, Switzerland (to appear, 2009)
Darvas, A., Leino, K.R.M.: Practical reasoning about invocations and implementations of pure methods. In: Dwyer, M.B., Lopes, A. (eds.) FASE 2007. LNCS, vol. 4422, pp. 336–351. Springer, Heidelberg (2007)
Distefano, D., Parkinson, M.J.: jStar: Towards Practical Verification for Java. In: OOPSLA ’08: Proceedings of the 23rd ACM SIGPLAN conference on Object oriented programming systems languages and applications, pp. 213–226 (2008)
EVE: Eiffel Verification Environment, http://eve.origo.ethz.ch
Findler, R.B., Felleisen, M.: Contracts for higher-order functions. SIGPLAN Not. 37(9), 48–59 (2002)
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison Wesley, Reading (1994)
Honda, K., Yoshida, N., Berger, M.: An observationally complete program logic for imperative higher-order frame rules. In: LICS ’05: Proceedings of the Symposium on Logic in Computer Science, USA, pp. 260–279. IEEE Computer Society, Los Alamitos (2005)
Jacobs, B.: A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs. PhD thesis, Katholieke Universiteit Leuven (2007)
Rustan, K., Leino, M.: Specification and verification of object-oriented software. Marktoberdorf International Summer School 2008, lecture notes (2008)
Rustan, K., Leino, M.: This is boogie 2. Technical Report Manuscript KRML 178, Microsoft Research (2008)
Kanig, J., Filliâtre, J.-C.: Who: A Verifier for Effectful Higher-order Programs. In: ACM SIGPLAN Workshop on ML, Edinburgh, Scotland, UK (2009)
Kassios, I.T.: Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 268–283. Springer, Heidelberg (2006)
Krishnaswami, N., Aldrich, J., Birkedal, L.: Modular verification of the subject-observer pattern via higher-order separation logic. In: FTJP (2007)
Leavens, G.T., Leino, K.R.M., Müller, P.: Specification and verification challenges for sequential object-oriented programs. Formal Aspects of Computing 19(2), 159–189 (2007)
Leino, K.R.M., Müller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 491–516. Springer, Heidelberg (2004)
Leino, K.R.M., Müller, P.: Verification of equivalent-results methods. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 307–321. Springer, Heidelberg (2008)
Müller, P., Ruskiewicz, J.N.: A modular verification methodology for C# delegates. In: Abrial, J.-R., Glässer, U. (eds.) Rigorous Methods for Software Construction and Analysis. LNCS, vol. 5115, pp. 187–203. Springer, Heidelberg (to appear, 2009)
Nordio, M., Calcagno, C., Meyer, B., Müller, P.: Reasoning about Function Objects. Technical Report 615, ETH Zurich (2008)
Nordio, M., Calcagno, C., Müller, P., Meyer, B.: A Sound and Complete Program Logic for Eiffel. In: Oriol, M. (ed.) TOOLS-EUROPE 2009. Lecture Notes in Business and Information Processing, vol. 33, pp. 195–214 (2009)
O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: POPL ’04, pp. 268–280 (2004)
Paige, R., Ostroff, J.: ERC: an Object-Oriented Refinement Calculus for Eiffel. Formal Aspects of Computing 16, 51–79 (2004)
Parkinson, M., Bierman, G.: Separation logic and abstraction. In: POPL ’05, vol. 40, pp. 247–258. ACM, New York (2005)
Parkinson, M.J., Bierman, G.M.: Separation logic, abstraction and inheritance. In: POPL ’08, pp. 75–86. ACM, New York (2008)
Régis-Gianas, Y., Pottier, F.: A hoare logic for call-by-value functional programs. In: Audebaud, P., Paulin-Mohring, C. (eds.) MPC 2008. LNCS, vol. 5133, pp. 305–335. Springer, Heidelberg (2008)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS (2002)
Schoeller, B.: Making classes provable through contracts, models and frames. PhD thesis, ETH Zurich (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
Nordio, M., Calcagno, C., Meyer, B., Müller, P., Tschannen, J. (2010). Reasoning about Function Objects. In: Vitek, J. (eds) Objects, Models, Components, Patterns. TOOLS 2010. Lecture Notes in Computer Science, vol 6141. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13953-6_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-13953-6_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-13952-9
Online ISBN: 978-3-642-13953-6
eBook Packages: Computer ScienceComputer Science (R0)