State Based Ownership, Reentrance, and Encapsulation

1. Aldrich, J., Chambers, C.: Ownership domains: Separating aliasing policy from mechanism. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 1–25. Springer, Heidelberg (2004)

   Chapter  Google Scholar 

2. Banerjee, A., Naumann, D.A.: Ownership confinement ensures representation independence for object-oriented programs. In: Journal of the ACM (2002) Accepted, revision pending. Extended version of [3]

   Google Scholar 

3. Banerjee, A., Naumann, D.A.: Representation independence, confinement and access control. In: POPL (2002)

   Google Scholar 

4. Banerjee, A., Naumann, D.A.: Ownership transfer and abstraction. Technical Report TR 2004-1, Computing and Information Sciences, Kansas State University (2003)

   Google Scholar 

5. Banerjee, A., Naumann, D.A.: State based encapsulation and generics. Technical Report CS Report 2004-11, Stevens Institute of Technology (2004)

   Google Scholar 

6. Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3 (2004)

   Google Scholar 

7. 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)

   Chapter  Google Scholar 

8. Barnett, M., Naumann, D.A., Schulte, W., Sun, Q.: 99.44% pure: useful abstractions in specifications. In: Malenfant, J., Østvold, B.M. (eds.) ECOOP 2004. LNCS, vol. 3344. Springer, Heidelberg (2005)

   Google Scholar 

9. Barnett, M., Naumann, D.A.: Friends need a bit more: Maintaining invariants over shared state. In: Mathematics of Program Construction (2004)

   Google Scholar 

10. Borba, P.H.M., Sampaio, A.C.A., Cornélio, M.L.: A refinement algebra for object-oriented programming. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol. 2743. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

11. Boyapati, C., Liskov, B., Shrira, L.: Ownership types for object encapsulation. In: POPL (2003)

    Google Scholar 

12. Boyland, J., Noble, J., Retert, W.: Capabilities for sharing: A generalisation of uniqueness and read-only. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, p. 2. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

13. Cavalcanti, A.L.C., Naumann, D.A.: Forward simulation for data refinement of classes. In: Formal Methods Europe (2002)

    Google Scholar 

14. Clarke, D., Drossopoulou, S.: Ownership, encapsulation and the disjointness of type and effect. In: OOPSLA (2002)

    Google Scholar 

15. Clarke, D.G., Potter, J., Noble, J.: Ownership types for flexible alias protection. In: OOPSLA (1998)

    Google Scholar 

16. Detlefs, D.L., Leino, K.R.M., Nelson, G.: Wrestling with rep exposure. Research 156, DEC Systems Research Center (1998)

    Google Scholar 

17. Guttag, J.V., Horning, J.J. (eds.): Larch: Languages and Tools for Formal Specification. Texts and Monographs in Computer Science. Springer, Heidelberg (1993)

    MATH  Google Scholar 

18. Hoare, C.A.R.: Proofs of correctness of data representations. Acta Inf. 1 (1972)

    Google Scholar 

19. Igarashi, A., Pierce, B., Wadler, P.: Featherweight Java: A minimal core calculus for Java and GJ. ACM Trans. Prog. Lang. Syst. 23 (2001)

    Google Scholar 

20. Jacobs, B., Poll, E.: Java program verification at Nijmegen: Developments and perspective. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol. 3233, pp. 134–153. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

21. 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)

    Chapter  Google Scholar 

22. Meyer, B.: Object-oriented Software Construction, 2nd edn (1997)

    Google Scholar 

23. Mijajlovic, I., Torp-Smith, N., O’Hearn, P.: Refinement and separation contexts. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 421–433. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

24. Mitchell, J.C.: Representation independence and data abstraction. In: POPL (1986)

    Google Scholar 

25. Müller, P., Poetzsch-Heffter, A., Leavens, G.: Modular invariants for object structures. Technical Report 424, ETH Zürich (October 2003)

    Google Scholar 

26. Naumann, D.A.: Observational purity and encapsulation. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 190–204. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

27. Naumann, D.A.: Verifying a secure information flow analyzer. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 211–226. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

28. Naumann, D.A., Barnett, M.: Towards imperative modules: Reasoning about invariants and sharing of mutable state (extended abstract). In: LICS (2004)

    Google Scholar 

29. O’Hearn, P., Yang, H., Reynolds, J.: Separation and information hiding. In: POPL (2004)

    Google Scholar 

30. Smith, F., Walker, D., Morrisett, G.: Alias types. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, p. 366. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

31. Vitek, J., Bokowski, B.: Confined types in Java. Software Practice and Experience 31 (2001)

    Google Scholar 

Download references