Anindya Banerjee
Skip Abstract Section
Abstract
Dedicated to the memory of John C. Reynolds (1935--2013).
The hiding of internal invariants creates a mismatch between procedure specifications in an interface and proof obligations on the implementations of those procedures. The mismatch is sound if the invariants depend only on encapsulated state, but encapsulation is problematic in contemporary software due to the many uses of shared mutable objects. The mismatch is formalized here in a proof rule that achieves flexibility via explicit restrictions on client effects, expressed using ghost state and ordinary first order assertions. The restrictions amount to a stateful frame condition that must be satisfied by any client; this dynamic encapsulation boundary complements conventional scope-based encapsulation. The technical development is based on a companion article, Part I, that presents Region Logic---a programming logic with stateful frame conditions for commands.
- Amtoft, T., Bandhakavi, S., and Banerjee, A. 2006. A logic for information flow in object-oriented programs. In Proceedings of the ACM Symposium on Principles of Programming Languages. 91--102. Google Scholar
Digital Library
- Apt, K. R., de Boer, F. S., and Olderog, E.-R. 2009. Verification of Sequential and Concurrent Programs 3rd Ed. Springer. Google ScholarDigital Library
- Apt, K. R., de Boer, F. S., Olderog, E.-R., and de Gouw, S. 2012. Verification of object-oriented programs: A transformational approach. J. Comput. Syst. Sci. 78, 3, 823--852. Google ScholarDigital Library
- Back, R.-J. and von Wright, J. 1998. Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science, Springer-Verlag. Google ScholarDigital Library
- Banerjee, A., Naumann, D. A., and Rosenberg, S. 2013. Local reasoning for global invariants, Part I: Region logic. J. ACM, To appear. Google ScholarDigital Library
- Barnett, M., Leino, K. R. M., and Schulte, W. 2005. The Spec# programming system: An overview. In Proceedings of the International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS’04). Revised Selected Papers. Lecture Notes in Computer Science, vol. 3362, 49--69. Google ScholarDigital Library
- Beckert, B., Hähnle, R., and Schmitt, P. H. 2007. Verification of Object-Oriented Software: The KeY Approach. Lecture Notes in Computer Science, vol. 4334, Springer-Verlag. Google ScholarDigital Library
- Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P. W., Wies, T., and Yang, H. 2007. Shape analysis for composite data structures. In Proceedings of the Computer Aided Verification. Lecture Notes in Computer Science, vol. 4590, 178--192. Google ScholarDigital Library
- Bierhoff, K. and Aldrich, J. 2007. Modular typestate checking of aliased objects. In Proceedings of the ACM Conference on Object-Oriented Programming Languages, Systems, and Applications. 301--320. Google ScholarDigital Library
- Birkedal, L., Torp-Smith, N., and Yang, H. 2005. Semantics of separation-logic typing and higher-order frame rules. In Proceedings of the IEEE Symposium on Logic in Computer Science. 260--269. Google ScholarDigital Library
- Birkedal, L., Torp-Smith, N., and Yang, H. 2006. Semantics of separation-logic typing and higher-order frame rules for Algol-like languages. Log. Meth. Comput. Sci. 2, 5:1, 1--33.Google Scholar
- Bornat, R., Calcagno, C., O’Hearn, P. W., and Parkinson, M. J. 2005. Permission accounting in separation logic. In Proceedings of the ACM Symposium on Principles of Programming Languages. 259--270. Google ScholarDigital Library
- Cameron, N. R., Drossopoulou, S., Noble, J., and Smith, M. J. 2007. Multiple ownership. In Proceedings of the ACM Conference on Object-Oriented Programming Languages, Systems, and Applications. 441--460. Google ScholarDigital Library
- Chin, W.-N., David, C., Nguyen, H. H., and Qin, S. 2008. Enhancing modular OO verification with separation logic. In Proceedings of the ACM Symposium on Principles of Programming Languages. 87--99. Google ScholarDigital Library
- Cohen, E., Dahlweid, M., Hillebrand, M. A., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., and Tobies, S. 2009. VCC: A practical system for verifying concurrent C. In Proceedings of the Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol. 5674, 23--42. Google ScholarDigital Library
- Cohen, E., Moskal, M., Schulte, W., and Tobies, S. 2010. Local verification of global invariants in concurrent programs. In Computer Aided Verification, Lecture Notes in Computer Science, vol. 6174, 480--494. Google ScholarDigital Library
- Dietl, W. and Müller, P. 2005. Universes: Lightweight ownership for JML. J. Obj. Tech. 4, 5--32.Google ScholarCross Ref
- Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M. J., and Vafeiadis, V. 2010. Concurrent abstract predicates. In Proceedings of the European Conference on Object-Oriented Programming. 504--528. Google ScholarDigital Library
- Distefano, D. and Parkinson, M. J. 2008. jStar: Towards practical verification for Java. In Proceedings of the ACM Conference on Object-Oriented Programming Languages, Systems, and Applications. 213--226. Google ScholarDigital Library
- Dockins, R., Hobor, A., and Appel, A. W. 2009. A fresh look at separation algebras and share accounting. In Proceedings of the Asian Symposium on Programming Languages and Systems. Lecture Notes in Computer Science, vol. 5904, 161--177. Google ScholarDigital Library
- Drossopoulou, S., Francalanza, A., Müller, P., and Summers, A. J. 2008. A unified framework for verification techniques for object invariants. In Proceedings of the European Conference on Object-Oriented Programming. Lecture Notes in Computer Science, vol. 5142, 412--437. Google ScholarDigital Library
- Filipovic, I., O’Hearn, P. W., Rinetzky, N., and Yang, H. 2010. Abstraction for concurrent objects. Theoret. Comput. Sci. 411, 51--52, 4379--4398. Google ScholarDigital Library
- Filliâtre, J.-C. and Marché, C. 2007. The Why/Krakatoa/Caduceus platform for deductive program verification (tool paper). In Computer Aided Verification, Lecture Notes in Computer Science, vol. 4590, 173--177. Google ScholarDigital Library
- Flanagan, C., Leino, K. R. M., Lillibridge, M., Nelson, G., Saxe, J. B., and Stata, R. 2002. Extended static checking for Java. In Proceedings of the ACM Conference on Programming Languages Design and Implementation. 234--245. Google ScholarDigital Library
- Grothoff, C., Palsberg, J., and Vitek, J. 2007. Encapsulating objects with confined types. ACM Trans. Program. Lang. Syst. 29, 6. Google ScholarDigital Library
- Harel, D., Pnueli, A., and Stavi, J. 1977. A complete axiomatic system for proving deductions about recursive programs. In Proceedings of the Annual ACM Symposium on Theory of Computing. 249--260. Google ScholarDigital Library
- He, J., Hoare, C. A. R., and Sanders, J. 1986. Data refinement refined (resumé). In Proceedings of the European Symposium on Programming. Lecture Notes in Computer Science, vol. 213, Springer, 187--196. Google ScholarDigital Library
- Hoare, C. A. R. 1971. Procedures and parameters: An axiomatic approach. In Proceedings of the Symposium on Semantics of Algorithmic Languages. E. Engeler Ed., Springer, 102--116.Google ScholarCross Ref
- Hoare, C. A. R. 1972. Proofs of correctness of data representations. Acta Inf. 1, 271--281.Google ScholarDigital Library
- Jones, C. B. 1983. Specification and design of (parallel) programs. In Proceedings of the IFIP Congress. 321--332.Google Scholar
- Kassios, I. T. 2006. Dynamic frames: Support for framing, dependencies and sharing without restrictions. In Formal Methods, Lecture Notes in Computer Science, vol. 4085, 268--283. Google ScholarDigital Library
- Kassios, I. T. 2011. The dynamic frames theory. Form. Asp. Comput. 23, 3, 267--288. Google ScholarCross Ref
- Kleymann, T. 1999. Hoare logic and auxiliary variables. Form. Asp. Comput. 11, 541--566.Google ScholarCross Ref
- Krishnaswami, N. R., Aldrich, J., Birkedal, L., Svendsen, K., and Buisse, A. 2009. Design patterns in separation logic. In Proceedings of the ACM Workshop on Types in Languages Design and Implementation. 105--116. Google ScholarDigital Library
- Krishnaswami, N. R., Aldrich, J., and Birkedal, L. 2010. Verifying event-driven programs using ramified frame properties. In Proceedings of the ACM Workshop on Types in Languages Design and Implementation. 63--76. Google ScholarDigital Library
- Kroening, D. and Strichman, O. 2008. Decision Procedures: An Algorithmic Point of View. Springer. Google Scholar
- Lahiri, S. K., Qadeer, S., and Walker, D. 2011. Linear maps. In Proceedings of the ACM Workshop on Programming Languages meets Program Verification. 3--14. Google ScholarDigital Library
- Leavens, G. T. and Müller, P. 2007. Information hiding and visibility in interface specifications. In Proceedings of the International Conference on Software Engineering. 385--395. Google ScholarDigital Library
- Leavens, G. T. and Naumann, D. A. 2013. Behavioral subtyping, specification inheritance, and modular reasoning. Tech. rep. CS-TR-13-03, Department of Computer Science, University of Central Florida.Google Scholar
- Leavens, G. T., Cheon, Y., Clifton, C., Ruby, C., and Cok, D. R. 2003. How the design of JML accommodates both runtime assertion checking and formal verification. In Proceedings of the Formal Methods for Components and Objects (FMCO’02). Lecture Notes in Computer Science, vol. 2852, Springer, 262--284.Google ScholarCross Ref
- Leavens, G. T., Leino, K. R. M., and Müller, P. 2007. Specification and verification challenges for sequential object-oriented programs. Form. Asp. Comput. 19, 2, 159--189. Google ScholarCross Ref
- Leino, K. R. M. 2008. This is Boogie 2. Manuscript KRML 178. http://research.microsoft.com/en-us/um/people/leino/papers/krml178.pdf.Google Scholar
- Leino, K. R. M. and Müller, P. 2004. Object invariants in dynamic contexts. In Proceedings of the European Conference on Object-Oriented Programming. Lecture Notes in Computer Science, vol. 3086, 491--516.Google ScholarCross Ref
- Leino, K. R. M. and Müller, P. 2006. A verification methodology for model fields. In Proceedings of the European Symposium on Programming Languages and Systems. Lecture Science on Computer Science, vol. 3924, 115--130. Google ScholarDigital Library
- Leino, K. R. M. and Schulte, W. 2007. Using history invariants to verify observers. In Proceedings of the European Symposium on Programming Languages and Systems. Lecture Notes in Computer Science, vol. 4421, 80--94. Google ScholarDigital Library
- Leino, K. R. M., Poetzsch-Heffter, A., and Zhou, Y. 2002. Using data groups to specify and check side effects. In Proceedings of the ACM Conference on Programming Language Design and Implementation. 246--257. Google ScholarDigital Library
- Liskov, B. H. and Wing, J. M. 1994. A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16, 6, 254--280. Google ScholarDigital Library
- Malecha, G., Morrisett, G., Shinnar, A., and Wisnesky, R. 2010. Toward a verified relational database management system. In Proceedings of the ACM Symposium on Principles of Programming Languages. 237--248. Google ScholarDigital Library
- Morgan, C. 1994. Programming from Specifications 2nd Ed. Prentice Hall. Google ScholarDigital Library
- Müller, P. 2002. Modular Specification and Verification of Object-Oriented Programs. Lecture Notes in Computer Science, vol. 2262, Springer.Google Scholar
- Müller, P. and Rudich, A. 2007. Ownership transfer in universe types. In Proceedings of the ACM Conference on Object-Oriented Programming Languages, Systems, and Applications. 461--478. Google ScholarDigital Library
- Müller, P., Poetzsch-Heffter, A., and Leavens, G. T. 2006. Modular invariants for layered object structures. Sci. Comput. Program. 62, 3, 253--286. Google ScholarDigital Library
- Nanevski, A., Morrisett, G., and Birkedal, L. 2006. Polymorphism and separation in Hoare type theory. In Proceedings of the International Conference on Functional Programming. 62--73. Google ScholarDigital Library
- Nanevski, A., Morrisett, J. G., and Birkedal, L. 2008. Hoare type theory, polymorphism and separation. J. Funct. Prog. 18, 5--6, 865--911. Google ScholarDigital Library
- Nanevski, A., Vafeiadis, V., and Berdine, J. 2010. Structuring the verification of heap-manipulating programs. In Proceedings of the ACM Symposium on Principles of Programming Languages. 261--274. Google ScholarDigital Library
- Naumann, D. A. 2001. Calculating sharp adaptation rules. Inf. Process. Lett. 77, 201--208. Google ScholarDigital Library
- Naumann, D. A. and Banerjee, A. 2010. Dynamic boundaries: Information hiding by second order framing with first order assertions. In Proceedings of the European Symposium on Programming Languages and Systems. Lecture Notes in Computer Science, vol. 6012, 2--22. Google ScholarDigital Library
- Naumann, D. A. and Barnett, M. 2004. Towards imperative modules: Reasoning about invariants and sharing of mutable state. In Proceedings of the IEEE Symposium on Logic in Computer Science. 313--323. Google ScholarDigital Library
- Naumann, D. A. and Barnett, M. 2006. Towards imperative modules: Reasoning about invariants and sharing of mutable state. Theoret. Comput. Sci. 365, 143--168. Google ScholarDigital Library
- Nipkow, T. 2002. Hoare logics for recursive procedures and unbounded nondeterminism. In Proceedings of the Conference on Computer Science Logic. Lecture Notes in Computer Science, vol. 2471, 103--119. Google ScholarDigital Library
- O’Hearn, P. W. and Tennent, R. D., Eds. 1997. ALGOL-like Languages. vol. 1 and vol. 2, Birkhäuser, Boston, Massachusetts.Google Scholar
- O’Hearn, P. W., Reynolds, J. C., and Yang, H. 2001. Local reasoning about programs that alter data structures. In Proceedings of the Conference on Computer Science Logic. Lecture Notes in Computer Science, vol. 2142, 1--19. Google ScholarDigital Library
- O’Hearn, P. W., Yang, H., and Reynolds, J. C. 2004. Separation and information hiding. In Proceedings of the ACM Symposium on Principles of Programming Languages. 268--280. Google ScholarDigital Library
- O’Hearn, P. W., Yang, H., and Reynolds, J. C. 2009. Separation and information hiding. ACM Trans. Program. Lang. Syst. 31, 3, 1--50. Google ScholarDigital Library
- Olderog, E.-R. 1983. On the notion of expressiveness and the rule of adaptation. Theoret. Comput. Sci. 24, 337--347.Google ScholarCross Ref
- Owicki, S. and Gries, D. 1976. An axiomatic proof technique for parallel programs I. Acta Inf. 6, 319--340.Google ScholarDigital Library
- Parkinson, M. 2007. Class invariants: the end of the road? In Proceedings of the International Workshop on Aliasing, Confinement and Ownership.Google Scholar
- Parkinson, M. J. and Bierman, G. M. 2005. Separation logic and abstraction. In Proceedings of the ACM Symposium on Principles of Programming Languages. 247--258. Google ScholarDigital Library
- Parkinson, M. J. and Bierman, G. M. 2008. Separation logic, abstraction and inheritance. In Proceedings of the ACM Symposium on Principles of Programming Languages. 75--86. Google ScholarDigital Library
- Petersen, R. L., Birkedal, L., Nanevski, A., and Morrisett, G. 2008. A realizability model for impredicative Hoare type theory. In Proceedings of the European Symposium on Programming Languages and Systems. Lecture Notes in Computer Science, vol. 4960, 337--352. Google ScholarDigital Library
- Pierik, C. 2006. Validation techniques for object-oriented proof outlines. Tech. rep. 2006-5, Universiteit Utrecht, SIKS Dissertation Series. ISBN 90-393-4217-2.Google Scholar
- Pierik, C. and de Boer, F. S. 2004. Modularity and the rule of adaptation. In Algebraic Methodology and Software Technology. Lecture Notes in Computer Science, vol. 3116, 394--408.Google ScholarCross Ref
- Pierik, C. and de Boer, F. 2005a. On behavioral subtyping and completeness. In Proceedings of the 7th ECOOP Workshop on Formal Techniques for Java-like Programs. J. Vitek and F. Logozzo Eds.Google Scholar
- Pierik, C. and de Boer, F. S. 2005b. A proof outline logic for object-oriented programming. Theoret. Comput. Sci. 343, 413--442. Google ScholarDigital Library
- Pierik, C., Clarke, D., and de Boer, F. S. 2005. Controlling object allocation using creation guards. In Formal Methods, Lecture Notes in Computer Science, vol. 3582, Springer, 59--74. Google ScholarDigital Library
- Poetzsch-Heffter, A. and Müller, P. 1999. A programming logic for sequential Java. In Proceedings of the European Symposium on Programming Languages and Systems. Lecture Notes in Computer Science, vol. 1576, 162--176. Google ScholarDigital Library
- Reynolds, J. C. 1981. The Craft of Programming. Prentice-Hall. Google ScholarDigital Library
- Reynolds, J. C. 1982. Idealized Algol and its specification logic. In Tools and Notions for Program Construction, D. Néel Ed., Cambridge University Press, 121--161.Google ScholarDigital Library
- Reynolds, J. C. 1998. Theories of Programming Languages. Cambridge University Press. Google ScholarDigital Library
- Rosenberg, S., Banerjee, A., and Naumann, D. A. 2010. Local reasoning and dynamic framing for the composite pattern and its clients. In Proceedings of the Verified Software: Theories, Tools, Experiments. Lecture Notes in Computer Science, vol. 6217, 183--198. (http://www.cs.stevens.edu/~naumann/pub/VERL/). Google ScholarDigital Library
- Roth, A. 2005. Specification and verification of encapsulation in Java programs. In Proceedings of the Formal Methods for Open Object-Based Distributed Systems (FMOODS). M. Steffen and G. Zavattaro Eds., Lecture Notes in Computer Science, vol. 3535, 195--210. Google ScholarDigital Library
- Roth, A. 2006. Specification and verification of object oriented software components. Ph.D. thesis, Karlsruhe Institute of Technology.Google Scholar
- Schmitt, P. H., Ulbrich, M., and Weiß, B. 2010. Dynamic frames in Java dynamic logic. In Proceedings of the Formal Verification of Object-Oriented Software (FoVeOOS) -- (Revised Selected Papers). Lecture Notes in Computer Science, vol. 6528, 138--152. Google ScholarDigital Library
- Schwinghammer, J., Yang, H., Birkedal, L., Pottier, F., and Reus, B. 2010. A semantic foundation for hidden state. In Proceedings of the Foundations of Software Science and Computational Structures. Lecture Notes in Computer Science, vol. 6014, 2--17. Google ScholarDigital Library
- Shaner, S. M., Leavens, G. T., and Naumann, D. A. 2007. Modular verification of higher-order methods with mandatory calls specified by model programs. In Proceedings of the ACM Conference on Object-Oriented Programming Languages, Systems, and Applications. 351--368. Google ScholarDigital Library
- Smans, J., Jacobs, B., Piessens, F., and Schulte, W. 2008. An automatic verifier for Java-like programs based on dynamic frames. In Proceedings of the Fundamental Aspects to Software Engineering. Lecture Notes in Computer Science, vol. 4961, Springer, 261--275. Google ScholarDigital Library
- Smans, J., Jacobs, B., Piessens, F., and Schulte, W. 2010. Automatic verification of Java programs with dynamic frames. Formal Aspects of Computing 22, 3--4, 423--457. Google ScholarCross Ref
- Thamsborg, J., Birkedal, L., and Yang, H. 2012. Two for the price of one: Lifting separation logic assertions. Log. Meth. Comput. Sci. 8, 3.Google ScholarCross Ref
- von Oheimb, D. and Nipkow, T. 2002. Hoare logic for NanoJava: Auxiliary variables, side effects, and virtual methods revisited. In Formal Methods, Lecture Notes in Computer Science, vol. 2391, 89--105. Google ScholarDigital Library
- Zee, K., Kuncak, V., and Rinard, M. C. 2008. Full functional verification of linked data structures. In Proceedings of the ACM Conference on Programming Language Design and Implementation. 349--361. Google ScholarDigital Library
Index Terms
- Local Reasoning for Global Invariants, Part II: Dynamic Boundaries
Recommendations
Separation and information hiding
We investigate proof rules for information hiding, using the formalism of separation logic. In essence, we use the separating conjunction to partition the internal resources of a module from those accessed by the module's clients. The use of a logical ...
Local Reasoning for Global Invariants, Part I: Region Logic
Dedicated to the memory of Stephen L. Bloom (1940--2010).
Shared mutable objects pose grave challenges in reasoning, especially for information hiding and modularity. This article presents a novel technique for reasoning about error-avoiding partial ...
Separation and information hiding
POPL '04We investigate proof rules for information hiding, using the recent formalism of separation logic. In essence, we use the separating conjunction to partition the internal resources of a module from those accessed by the module's clients. The use of a ...
Comments