Separation and information hiding

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.

REFERENCES

• 1: Amal Ahmed , Limin Jia , David Walker, Reasoning about Hierarchical Storage, Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, p.33, June 22-25, 2003
• 2: 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).
• 3: 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.
• 4: Benton, N. 2006. Abstracting allocation. In Proceedings of the 20th International Workshop on Computer Science Logic (CSL). 182--196.
• 5: Bodil Biering , Lars Birkedal , Noah Torp-Smith, BI-hyperdoctrines, higher-order separation logic, and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.5, p.24-es, August 2007 [doi>10.1145/1275497.1275499]
• 6: Hongseok Yang, Semantics of Separation-Logic Typing and Higher-Order Frame Rules, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, p.260-269, June 26-29, 2005 [doi>10.1109/LICS.2005.47]
• 7: 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).
• 8: Richard Bornat, Proving Pointer Programs in Hoare Logic, Proceedings of the 5th International Conference on Mathematics of Program Construction, p.102-126, July 03-05, 2000
• 9: Richard Bornat , Cristiano Calcagno , Peter O'Hearn , Matthew Parkinson, Permission accounting in separation logic, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.259-270, January 12-14, 2005, Long Beach, California, USA
• 10: Brinch Hansen, P., Ed. 2002. The Origin of Concurrent Programming. Springer-Verlag.
• 11: Stephen Brookes, A semantics for concurrent separation logic, Theoretical Computer Science, v.375 n.1-3, p.227-270, April, 2007 [doi>10.1016/j.tcs.2006.12.034]
• 12: David G. Clarke , James Noble , John Potter, Simple Ownership Types for Object Containment, Proceedings of the 15th European Conference on Object-Oriented Programming, p.53-76, June 18-22, 2001
• 13: Cook, S. A. 1978. Soundness and completeness of an axiomatic system for program verification. SIAM J. Comput. 7, 70--90.
• 14: Christian Grothoff , Jens Palsberg , Jan Vitek, Encapsulating objects with confined types, Proceedings of the 16th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.241-255, October 14-18, 2001, Tampa Bay, FL, USA
• 15: 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.
• 16: Hoare, C. A. R. 1972a. Proof of correctness of data representations. Acta Informatica 4, 271--281.
• 17: Hoare, C. A. R. 1972b. Towards a theory of parallel programming. In Operating Systems Techniques, Hoare and Perrot, Eds. Academic Press.
• 18: C. A. R. Hoare, Monitors: an operating system structuring concept, Communications of the ACM, v.17 n.10, p.549-557, Oct. 1974 [doi>10.1145/355620.361161]
• 19: John Hogg, Islands: aliasing protection in object-oriented languages, Conference proceedings on Object-oriented programming systems, languages, and applications, p.271-285, October 06-11, 1991, Phoenix, Arizona, United States
• 20: Samin S. Ishtiaq , Peter W. O'Hearn, BI as an assertion language for mutable data structures, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.14-26, January 2001, London, United Kingdom
• 21: Brian W. Kernighan , Dennis M. Ritchie, The C programming language, Prentice Hall Press, Upper Saddle River, NJ, 1989
• 22: 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.
• 23: Leino, K. and Müller, P. 2004. Object invariants in dynamic contexts. In Proceedings of the 18th European Conference on Object-Oriented Programming (ECOOP).
• 24: K. Rustan M. Leino , Greg Nelson, Data abstraction and information hiding, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.5, p.491-553, September 2002 [doi>10.1145/570886.570888]
• 25: John C. Mitchell , Gordon D. Plotkin, Abstract types have existential type, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.470-502, July 1988 [doi>10.1145/44501.45065]
• 26: Carroll Morgan, The specification statement, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.403-419, July 1988 [doi>10.1145/44501.44503]
• 27: Joseph M. Morris, A theoretical basis for stepwise refinement and the programming calculus, Science of Computer Programming, v.9 n.3, p.287-306, December 1, 1987 [doi>10.1016/0167-6423(87)90011-6]
• 28: Peter Müller , Arnd Poetzsch-Heffter, Modular specification and verification techniques for object-oriented software components, Foundations of component-based systems, Cambridge University Press, New York, NY, 2000
• 29: Aleksandar Nanevski , Greg Morrisett , Lars Birkedal, Polymorphism and separation in hoare type theory, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, September 16-21, 2006, Portland, Oregon, USA
• 30: David A. Naumann, On assertion-based encapsulation for object invariants and simulations, Formal Aspects of Computing, v.19 n.2, p.205-224, June 2007 [doi>10.1007/s00165-006-0020-5]
• 31: Naumann, D. A. and Barnett, M. 2004a. Friends need a bit more: Maintaining invariants over shared state. In Mathematics of Program Construction.
• 32: David A. Naumann , Mike Barnett, Towards Imperative Modules: Reasoning about Invariants and Sharing of Mutable State, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, p.313-323, July 13-17, 2004 [doi>10.1109/LICS.2004.49]
• 33: Peter W. O'Hearn , John C. Reynolds , Hongseok Yang, Local Reasoning about Programs that Alter Data Structures, Proceedings of the 15th International Workshop on Computer Science Logic, p.1-19, September 10-13, 2001
• 34: Peter W. OHearn, Resources, concurrency, and local reasoning, Theoretical Computer Science, v.375 n.1-3, p.271-307, April, 2007 [doi>10.1016/j.tcs.2006.12.035]
• 35: Peter W. O'Hearn , Hongseok Yang , John C. Reynolds, Separation and information hiding, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.268-280, January 14-16, 2004, Venice, Italy
• 36: Parkinson, M. 2005. Local reasoning for Java. Ph.D. thesis, Cambridge University, Cambridge, UK.
• 37: 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).
• 38: Matthew Parkinson , Gavin Bierman, Separation logic and abstraction, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.247-258, January 12-14, 2005, Long Beach, California, USA
• 39: Matthew Parkinson , Richard Bornat , Cristiano Calcagno, Variables as Resource in Hoare Logics, Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, p.137-146, August 12-15, 2006 [doi>10.1109/LICS.2006.52]
• 40: Parnas, D. 1972a. Information distribution aspects of design methodology. Proceedings of International Federation for Information Processing (IFIP) 1, 339--344.
• 41: D. L. Parnas, On the criteria to be used in decomposing systems into modules, Communications of the ACM, v.15 n.12, p.1053-1058, Dec. 1972 [doi>10.1145/361598.361623]
• 42: 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).
• 43: Plotkin, G. 1983. Pisa notes (on domain theory).
• 44: Reynolds, J. C. 1983. Types, abstraction and parametric polymorphism. Proceedings of International Federation for Information Processing (IFIP).
• 45: John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
• 46: Jerald Sydney Schwarz, Semantics of partial correctness formalisms., Syracuse University, Syracuse, NY, 1975
• 47: Schwarz, J. S. 1977. Generic commands—a tool for partial correctness formalisms. Comput. J. 20, 2, 151--155.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Class invariants

General Terms:
Languages, Theory, Verification

Keywords:
Separation logic, modularity, resource protection