Peter W. O'Hearn
Skip Abstract Section
Abstract
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 connective gives rise to a form of dynamic partitioning, where we track the transfer of ownership of portions of heap storage between program components. It also enables us to enforce separation in the presence of mutable data structures with embedded addresses that may be aliased.
- Ahmed, A., Jia, L., and Walker, D. 2003. Reasoning about hierarchical storage. In Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science (LICS). 33--44. Google Scholar
Digital Library
- Banerjee, A. and Naumann, D. A. 2005. State based ownership, reentrance, and encapsulation. In Proceedings of the 19th European Conference on Object-Oriented Programming (ECOOP). Google ScholarDigital Library
- Barnett, M., DeLine, R., Fahndrich, M., Leino, K., and Schulte, W. 2004. Verification of object-oriented programs with invariants. J. Obj. Techn. 3, 6, 27--56.Google ScholarCross Ref
- Benton, N. 2006. Abstracting allocation. In Proceedings of the 20th International Workshop on Computer Science Logic (CSL). 182--196. Google ScholarDigital Library
- Biering, B., Birkedal, L., and Torp-Smith, N. 2007. BI-hyperdoctrines, higher-order separation logic, and abstraction. ACM Trans. Program. Lang. Syst. 29, 5. 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 20th Annual IEEE Symposium on Logic in Computer Science (LICS). Google ScholarDigital Library
- Birkedal, L. and Yang, H. 2007. Relational parametricity and separation logic. In Proceedings of the 10th International Conference on Foundations of Software Science and Computation Structures (FOSSACS). Google ScholarDigital Library
- Bornat, R. 2000. Proving pointer programs in Hoare logic. Mathematics of Program Construction. Google ScholarDigital Library
- Bornat, R., Calcagno, C., O'Hearn, P., and Parkinson, M. 2005. Permission accounting in separation logic. In Proceedings of the 32nd ACM Symposium on Principles of Programming Languages (POPL). 59--70. Google ScholarDigital Library
- Brinch Hansen, P., Ed. 2002. The Origin of Concurrent Programming. Springer-Verlag. Google ScholarDigital Library
- Brookes, S. D. 2007. A semantics of concurrent separation logic. Theoretical Computer Science 375, 1--3, 227--270. (Preliminary version appeared in CONCUR'04, LNCS 3170, pp. 16--34). Google ScholarDigital Library
- Clarke, D., Noble, J., and Potter, J. 2001. Simple ownership types for object containment. Proceedings of the 15th European Conference on Object-Oriented Programming (ECOOP). Lecture Notes in Computer Science, vol. 2072, Springer. 53--76. Google ScholarDigital Library
- Cook, S. A. 1978. Soundness and completeness of an axiomatic system for program verification. SIAM J. Comput. 7, 70--90.Google ScholarCross Ref
- Grothoff, C., Palsberg, J., and Vitek, J. 2001. Encapsulating objects with confined types. In Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA). 241--253. Google ScholarDigital Library
- Hoare, C. A. R. 1971. Procedures and parameters: An axiomatic approach. In Proceedings of the Symposium on the Semantics of Algebraic Languages, E. Engler, Ed. Springer, 102--116. Lecture Notes in Math. 188.Google ScholarCross Ref
- Hoare, C. A. R. 1972a. Proof of correctness of data representations. Acta Informatica 4, 271--281.Google ScholarDigital Library
- Hoare, C. A. R. 1972b. Towards a theory of parallel programming. In Operating Systems Techniques, Hoare and Perrot, Eds. Academic Press.Google Scholar
- Hoare, C. A. R. 1974. Monitors: An operating system structuring concept. Comm. ACM 17, 10, 549--557. Reprinted in {Brinch Hansen 2002}. Google ScholarDigital Library
- Hogg, J. 1991. Islands: aliasing protection in object-oriented languages. In Proceedings of the 6th Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA). Google ScholarDigital Library
- Isthiaq, S. and O'Hearn, P. W. 2001. BI as an assertion language for mutable data structures. In Proceedings of the 28th ACM Symposium on Principles of Programming Languages (POPL). 36--49. Google ScholarDigital Library
- Kernighan, B. and Ritchie, D. 1988. The C Programming Language. Prentice Hall. Second edition. Google ScholarDigital Library
- Krishnaswami, N., Aldrich, J., and Birkedal, L. 2007. A modular verification of the subject-observer pattern via higher-order separation logic. In Proceedings of the 9th Workshop on Formal Techniques for Java-like Programs.Google Scholar
- Leino, K. and Müller, P. 2004. Object invariants in dynamic contexts. In Proceedings of the 18th European Conference on Object-Oriented Programming (ECOOP).Google Scholar
- Leino, K. R. M. and Nelson, G. 2002. Data abstraction and information hiding. ACM Trans. Program. Lang. Syst. 24, 5, 491--553. Google ScholarDigital Library
- Mitchell, J. C. and Plotkin, G. D. 1988. Abstract types have existential types. ACM Trans. Program. Lang. Syst. 10, 3, 470--502. Google ScholarDigital Library
- Morgan, C. 1988. The specification statement. ACM Trans. Program. Lang. Syst. 10, 3, 403--419. Google ScholarDigital Library
- Morris, J. 1987. A theoretical basis for stepwise refinement and the programming calculus. Sci. Comput. Program. 9, 3, 287--306. Google ScholarDigital Library
- Müller, P. and Poetzsch-Heffter, A. 2000. Modular specification and verification techniques for object-oriented software components. In Foundations of Component-Based Systems. Cambridge University Press. Google ScholarDigital Library
- Nanevski, A., Morrisett, G., and Birkedal, L. 2006. Polymorphism and separation in Hoare type theory. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP). 62--73. Google ScholarDigital Library
- Naumann, D. 2007. On assertion-based encapsulation for object invariants and simulations. Formal Asp. Comput. 19, 2, 205--224. Google ScholarCross Ref
- Naumann, D. A. and Barnett, M. 2004a. Friends need a bit more: Maintaining invariants over shared state. In Mathematics of Program Construction.Google Scholar
- Naumann, D. A. and Barnett, M. 2004b. Towards imperative modules: Reasoning about invariants and shared of mutable state. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS). Google ScholarDigital Library
- O'Hearn, P., Reynolds, J., and Yang, H. 2001. Local reasoning about programs that alter data structures. In Proceedings of the 15th International Workshop on Computer Science Logic (CSL). 1--19. Google ScholarDigital Library
- O'Hearn, P. W. 2007. Resources, concurrency and local reasoning. Theoretical Computer Science 375, 1--3, 271--307. (Preliminary version appeared in CONCUR'04, Lecture Notes in Computer Science, vol. 3170, 49--67). Google ScholarDigital Library
- O'Hearn, P. W., Yang, H., and Reynolds, J. C. 2004. Separation and information hiding. In Proceedings of the 31st ACM Symposium on Principles of Programming Languages (POPL). 268-- 280. Google ScholarDigital Library
- Parkinson, M. 2005. Local reasoning for Java. Ph.D. thesis, Cambridge University, Cambridge, UK.Google Scholar
- Parkinson, M. 2007. Class invariants: the end of the road? Position paper presented at 3rd International Workshop on Aliasing, Confinement, and Ownership in Object-Oriented Programming (IWACO).Google Scholar
- Parkinson, M. and Bierman, G. 2005. Separation logic and abstraction. In Proceedings of the 32nd ACM Symposium on Principles of Programming Languages (POPL), 59--70. Google ScholarDigital Library
- Parkinson, M., Bornat, R., and Calcagno, C. 2006. Variables as resource in Hoare logics. In Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science (LICS). Google ScholarDigital Library
- Parnas, D. 1972a. Information distribution aspects of design methodology. Proceedings of International Federation for Information Processing (IFIP) 1, 339--344.Google Scholar
- Parnas, D. 1972b. On the criteria to be used in decomposing systems into modules. Comm. ACM 15, 12, 1053--1058. Google ScholarDigital Library
- Peterson, R., Birkedal, L., Nanevski, A., and Morrisett, G. 2008. A realizability model of impredicative Hoare type theory. In Proceedings of the 17th European Symposium on Programming (ESOP). Google ScholarDigital Library
- Plotkin, G. 1983. Pisa notes (on domain theory).Google Scholar
- Reynolds, J. C. 1983. Types, abstraction and parametric polymorphism. Proceedings of International Federation for Information Processing (IFIP).Google Scholar
- Reynolds, J. C. 2002. Separation logic: A logic for shared mutable data structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS). 55--74. Google ScholarDigital Library
- Schwarz, J. S. 1974. Semantics of partial correctness formalisms. Ph.D. thesis, Syracuse University, Syracuse, NY. Google ScholarDigital Library
- Schwarz, J. S. 1977. Generic commands—a tool for partial correctness formalisms. Comput. J. 20, 2, 151--155.Google ScholarCross Ref
Index Terms
- Separation and information hiding
Recommendations
Separation and information hiding
POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe 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 ...
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 ...
Interactive proofs in higher-order concurrent separation logic
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesWhen using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...
Comments