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.
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
Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. JOT 3(6) (2004)
Barnett, M., Leino, K.R.M., 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)
Barnett, M., Naumann, D.: Friends need a bit more: Maintaining invariants over shared state. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 54–84. Springer, Heidelberg (2004)
Börger, E., Fruja, N.G., Gervasi, V., Stärk, R.F.: A high-level modular definition of the semantics of C#. Theoretical Computer Science 336(2-3), 235–284 (2005)
Dhara, K.K., Leavens, G.T.: Forcing behavioral subtyping through specification inheritance. In: ICSE, pp. 258–267. IEEE Computer Society Press, Los Alamitos (1996)
C# language specification. ECMA Standard 334 (June 2005)
Eiffel analysis, design and programming language. ECMA Standard 367 (June 2005)
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns. Addison-Wesley, Reading (1995)
Jacobs, B.: A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs. PhD thesis, Katholieke Universiteit Leuven (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., Schulte, W.: Using history invariants to verify observers. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 80–94. Springer, Heidelberg (2007)
Müller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Science of Computer Programming 62, 253–286 (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Müller, P., Ruskiewicz, J.N. (2009). A Modular Verification Methodology for C# Delegates. In: Abrial, JR., Glässer, U. (eds) Rigorous Methods for Software Construction and Analysis. Lecture Notes in Computer Science, vol 5115. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11447-2_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-11447-2_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11446-5
Online ISBN: 978-3-642-11447-2
eBook Packages: Computer ScienceComputer Science (R0)