Abstract
In the context of a formal programming methodology and verification system for ownership-based invariants in object-oriented programs, a friendship system is defined. Friendship is a flexible protocol that allows invariants expressed over shared state. Such invariants are more expressive than those allowed in exisiting ownership type systems because they link objects that are not in the same ownership domain. Friendship permits the modular verification of cooperating classes. This paper defines friendship, sketches a soundness proof, and provides several realistic examples.
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
Apt, K.R., Olderog, E.-R.: Verification of Sequential and Concurrent Programs, 2nd edn. Springer, Heidelberg (1997)
Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. In: Eisenbach, S., Leavens, G.T., Müller, P., Poetzsch-Heffter, A., Poll, E. (eds.) Formal Techniques for Java-like Programs 2003 (July 2003), Available as Technical Report 408, Department of Computer Science, ETH Zurich. A newer version of this paper is [BDF+ 03b]
Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verificationof object-oriented programs with invariants. Manuscript KRML 122b (December 2003), Available from http://research.microsoft.com/~leino/papers.html
Boyapati, C., Liskov, B., Shrira, L.: Ownership types for object encapsulation. In: POPL, pp. 213–223 (2003)
Banerjee, A., Naumann, D.A.: Ownership confinement ensures representation independence for object-oriented programs. Extended version of [BN02b], Available from http://www.cs.stevens-tech.edu/~naumann/oceri.ps (2002)
Banerjee, A., Naumann, D.A.: Representation independence, confinement and access control. In: POPL, pp. 166–177 (2002)
Banerjee, A., Naumann, D.A.: Ownership transfer and abstraction. Technical Report TR 2004-1, Computing and Information Sciences, Kansas State University (2003)
Barnett, M., Schulte, W.: Runtime verification of.NET contracts. The Journal of Systems and Software 65(3), 199–208 (2003)
Clarke, D., Drossopoulou, S.: Ownership, encapsulation and the disjointness of type and effect. In: OOPSLA (November 2002)
Cheon, Y., Leavens, G.T.: A runtime assertion checker for the Java Modeling Language (JML). In: Arabnia, H.R., Mun, Y. (eds.) Proceedings of the InternationalConference on Software Engineering Research and Practice (SERP 2002), Las Vegas, Nevada, USA, June 24-27, pp. 322–328. CSREA Press (2002)
Clarke, D.: Object ownership and containment. Dissertation, Computer Science and Engineering, University of New South Wales, Australia (2001)
Clarke, D.G., Noble, J., Potter, J.M.: Simple ownership types for object containment. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, p. 53. Springer, Heidelberg (2001)
DeLine, R., Fähndrich, M.: Enforcing high-level protocols in low-level software. In: PLDI, pp. 59–69 (2001)
DeLine, R., Fähndrich, M.: The Fugue protocol checker: Is your softwarebaroque? Available from http://research.microsoft.com/~maf/papers.html (2003)
Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. Research Report 159, Compaq Systems Research Center (December 1998)
de Roever, W.-P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge University, Cambridge (2001)
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)
Gunnerson, E.: A Programmer’s Introduction to C#. Apress, Berkeley (2000)
Jones, C.B.: Tentative steps towards a development method for interfering programs. ACM Transactions on Programming Languages and Systems 5(4), 596–619 (1983)
Liskov, B., Guttag, J.: Abstraction and Specification in Program Development. MIT Press, Cambridge (1986)
Leino, K.R.M., Müller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 491–515. Springer, Heidelberg (2004) (to appear)
Leino, K.R.M., Nelson, G.: Data abstraction and information hiding. ACM Transactions on Programming Languages and Systems 24(5), 491–553 (2002)
Liskov, B.H., Wing, J.M.: A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems 16(6) (1994)
Meyer, B.: Object-oriented Software Construction, 2nd edn. Prentice Hall, New York (1997)
Müller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for object structures. Technical Report 424, ETH Zürich, Chair of Software Engineering (October 2003)
Müller, P.: Modular Specification and Verification of Object-Oriented Programs. LNCS, vol. 2262. Springer, Heidelberg (2002)
Naumann, D.A., Barnett, M.: Towards imperative modules: Reasoning about invariants and sharing of mutable state (extended abstract). In: LICS (2004) (to appear)
O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: POPL, pp. 268–280 (2004)
Pierik, C., de Boer, F.S.: A syntax-directed Hoare logic for object-oriented programming concepts. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 64–78. Springer, Heidelberg (2003)
Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55–74 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barnett, M., Naumann, D.A. (2004). Friends Need a Bit More: Maintaining Invariants Over Shared State. In: Kozen, D. (eds) Mathematics of Program Construction. MPC 2004. Lecture Notes in Computer Science, vol 3125. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27764-4_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-27764-4_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22380-1
Online ISBN: 978-3-540-27764-4
eBook Packages: Springer Book Archive