A logical analysis of aliasing in imperative higher-order functions

ABSTRACT

We present a compositional program logic for call-by-value imperative higher-order functions with general forms of aliasing, which can arise from the use of reference names as function parameters, return values, content of references and parts of data structures. The program logic extends our earlier logic for alias-free imperative higher-order functions with new modal operators which serve as building blocks for clean structural reasoning about programs and data structures in the presence of aliasing. This has been an open issue since the pioneering work by Cartwright-Oppen and Morris twenty-five years ago. We illustrate usage of the logic for description and reasoning through concrete examples including a higher-order polymorphic Quicksort. The logical status of the new operators is clarified by translating them into (in)equalities of reference names. The logic is observationally complete in the sense that two programs are observationally indistinguishable if they satisfy the same set of assertions.

REFERENCES

• 1: C- home page. http://www.cminusminus.org.
• 2: A full version of the present paper. Available for download at www.dcs.qmul.ac.uk/~kohei/logics.
• 3: S. Abramsky , K. Honda , G. McCusker, A Fully Abstract Game Semantics for General References, Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, p.334, June 21-24, 1998
• 4: Krzysztof R. Apt, Ten Years of Hoare's Logic: A Survey—Part I, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.4, p.431-483, Oct. 1981 [doi>10.1145/357146.357150]
• 5: Friedrich L. Bauer, Edsger W. Dijkstra, and Tony Hoare, editors. Theoretical Foundations of Programming Methodology, Lecture Notes of an International Summer School. Reidel, 1982.
• 6: Patrick Blackburn , Maarten de Rijke , Yde Venema, Modal logic, Cambridge University Press, New York, NY, 2001
• 7: 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
• 8: Cristiano Calcagno, Philippa Gardner, and Matthew Hague. From separation logic to first-order logic. In Proc. FoSSaCs'05, LNCS. Springer-Verlag.
• 9: Robert Cartwright , Derek Oppen, Unrestricted procedure calls in Hoare's logic, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.131-140, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512774]
• 10: Robert Cartwright and Derek C. Oppen. The logic of aliasing. Acta Inf., 15:365--384, 1981.
• 11: Patrick Cousot. Methods and logics for proving programs. In Handbook of Theoretical Computer Science, volume B, pages 843--993. Elsevier, 1999.
• 12: G. W. Kulczycki et al. Reasoning about procedure calls with repeated arguments and the reference-value distinction. Technical Report TR#02-13a, Dept. of Comp. Sci., Iowa State Univ., December 2003.
• 13: Jean-Christophe Filliâtre and Nicolas Magaud. Certification of sorting algorithms in the system Coq. In Theorem Proving in Higher Order Logics: Emerging Trends, 1999.
• 14: Robert W. Floyd. Assigning meaning to programs. In Symp. in Applied Mathematics, volume 19, 1967.
• 15: Irene Greif , Albert R. Meyer, Specifying the Semantics of while Programs: A Tutorial and Critique of a Paper by Hoare and Lauer, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.4, p.484-507, Oct. 1981 [doi>10.1145/357146.357151]
• 16: David Gries , Gary Levin, Assignment and Procedure Call Proof Rules, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.4, p.564-579, Oct. 1980 [doi>10.1145/357114.357119]
• 17: Dan Grossman , Greg Morrisett , Trevor Jim , Michael Hicks , Yanling Wang , James Cheney, Region-based memory management in cyclone, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 18: Carl A. Gunter, Semantics of programming languages: structures and techniques, MIT Press, Cambridge, MA, 1992
• 19: Matthew Hennessy , Robin Milner, Algebraic laws for nondeterminism and concurrency, Journal of the ACM (JACM), v.32 n.1, p.137-161, Jan. 1985 [doi>10.1145/2455.2460]
• 20: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 21: Tony Hoare and He Jifeng. Unifying Theories of Programming. Prentice-Hall International, 1998.
• 22: Kohei Honda, From process logic to program logic, Proceedings of the ninth ACM SIGPLAN international conference on Functional programming, September 19-21, 2004, Snow Bird, UT, USA
• 23: Kohei Honda , Nobuko Yoshida, A compositional logic for polymorphic higher-order functions, Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.191-202, August 24-26, 2004, Verona, Italy [doi>10.1145/1013963.1013985]
• 24: An Observationally Complete Program Logic for Imperative Higher-Order Frame Rules, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), p.260-279, June 26-29, 2005 [doi>10.1109/LICS.2005.5]
• 25: T. M. V. Janssen , Peter van Emde Boas, On the Proper Treatment or Referencing, Dereferencing and Assignment, Proceedings of the Fourth Colloquium on Automata, Languages and Programming, p.282-300, July 18-22, 1977
• 26: Brian W. Kernighan , Dennis M. Ritchie, The C programming language, Prentice Hall Press, Upper Saddle River, NJ, 1989
• 27: Thomas Kleymann. Hoare logic and auxiliary variables. Technical report, University of Edinburgh, LFCS ECS-LFCS-98-399, October 1998.
• 28: Étienne Lozes, Elimination of spatial connectives in static spatial logics, Theoretical Computer Science, v.330 n.3, p.475-499, 9 February 2005 [doi>10.1016/j.tcs.2004.10.006]
• 29: David C. Luckham , Norihisa Suzuki, Verification of Array, Record, and Pointer Operations in Pascal, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.226-244, Oct. 1979 [doi>10.1145/357073.357078]
• 30: John L. McCarthy. Towards a mathematical science of computation. In IFIP Congress, pages 21--28, 1962.
• 31: Elliott Mendelson, Introduction to mathematical logic (3rd ed.), Wadsworth Publ. Co., Belmont, CA, 1987
• 32: Robin Milner , Joachim Parrow , David Walker, A calculus of mobile processes, II, Information and Computation, v.100 n.1, p.41-77, Sept. 1992 [doi>10.1016/0890-5401(92)90009-5]
• 33: Joseph M. Morris. A general axiom of assignment/ assignment and linked data structures/ a proof of the Schorr-Wait algorithm. In {5}, pages 25--52. Reidel, 1982.
• 34: 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
• 35: Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002
• 36: A. M. Pitts , I. D. B. Stark, Operational reasoning for functions with local state, Higher order operational techniques in semantics, Cambridge University Press, New York, NY, 1999
• 37: 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
• 38: Zhong Shao. An overview of the FLINT/ML compiler. In 1997 ACM SIGPLAN Workshop on Types in Compilation (TIC'97), Amsterdam, The Netherlands, June 1997.
• 39: Boris A. Trakhtenbrot , Joseph Y. Halpern , Albert R. Meyer, From Denotational to Operational and Axiomatic Semantics for ALGOL-like Languages: an Overview, Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.474-500, June 06-08, 1983

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Assertions

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs; Specification techniques

General Terms:
Languages, Reliability, Security, Theory, Verification

Keywords:
π-calculus, aliasing, functional programming, hoare-logics, modalities, pointers, typing