More Web Proxy on the site http://driver.im/

Article

A logical analysis of aliasing in imperative higher-order functions

Authors:

Nobuko YoshidaAuthors Info & Claims

ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming

Pages 280 - 293

https://doi.org/10.1145/1086365.1086401

Published: 12 September 2005 Publication History

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]

Samson Abramsky, Kohei Honda, and Guy McCusker. A fully abstract game semantics for general references. In LICS'98, pages 334--344, 1998.

Digital Library

[4]

K R. Apt. Ten Years of Hoare Logic: a survey. TOPLAS, 3:431--483, 1981.

Digital Library

[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, and Yde Venema. Modal Logic. Cambridge University Press, 2001.

Digital Library

[7]

Richard Bornat. Proving pointer programs in hoare logic. In Conf. on Mathematics of Program Construction, LNCS. Springer-Verlag, 2000.

Digital Library

[8]

Cristiano Calcagno, Philippa Gardner, and Matthew Hague. From separation logic to first-order logic. In Proc. FoSSaCs'05, LNCS. Springer-Verlag.

Digital Library

[9]

Robert Cartwright and Derek C. Oppen. Unrestricted procedure calls in Hoare's logic. In POPL, pages 131--140, 1978.

Digital Library

[10]

Robert Cartwright and Derek C. Oppen. The logic of aliasing. Acta Inf., 15:365--384, 1981.

Digital Library

[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 and Albert R. Meyer. Specifying the Semantics of while Programs: A Tutorial and Critique of a Paper by Hoare and Lauer. ACM Trans. Program. Lang. Syst., 3(4), 1981.

Digital Library

[16]

David Gries and Gary Levin. Assignment and procedure call proof rules. ACM Trans. Program. Lang. Syst., 2(4):564--579, 1980.

Digital Library

[17]

Dan Grossman, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, and James Cheney. Region-based memory management in cyclone. In PLDI'02. ACM, 2002.

Digital Library

[18]

Carl A. Gunter. Semantics of Programming Languages. MIT Press, 1995.

Digital Library

[19]

Matthew Hennessy and Robin Milner. Algebraic Laws for Non-Determinism and Concurrency. JACM, 32(1), 1985.

Digital Library

[20]

Tony Hoare. An axiomatic basis of computer programming. CACM, 12, 1969.

Digital Library

[21]

Tony Hoare and He Jifeng. Unifying Theories of Programming. Prentice-Hall International, 1998.

[22]

Kohei Honda. From process logic to program logic. In ICFP'04, pages 163--174. ACM Press, 2004.

Digital Library

[23]

Kohei Honda and Nobuko Yoshida. A compositional logic for polymorphic higher-order functions. In PPDP'04, pages 191--202. ACM Press, 2004.

Digital Library

[24]

Kohei Honda, Nobuko Yoshida, and Martin Berger. An observationally complete program logic for imperative higher-order functions. In Proc. LICS'05, pages 270--279. IEEE, 2005.

Digital Library

[25]

T. M. V. Janssen and Peter van Emde Boas. On the proper treatment of referencing, dereferencing and assignment. In Proc. ICALP, pages 282--300, 1977.

Digital Library

[26]

Brian W. Kernighan and Dennis M. Ritchie. The C Programming Language, Second Edition. Prentice-Hall, Englewood Cliffs, New Jersey, 1988.

Digital Library

[27]

Thomas Kleymann. Hoare logic and auxiliary variables. Technical report, University of Edinburgh, LFCS ECS-LFCS-98-399, October 1998.

[28]

Etienne Lozes. Elimination of spatial connectives in static spatial logics. TCS, to appear.

Digital Library

[29]

David C. Luckham and Norihisa Suzuki. Verification of array, record, and pointer operations in pascal. ACM Trans. Program. Lang. Syst., 1(2):226--244, 1979.

Digital Library

[30]

John L. McCarthy. Towards a mathematical science of computation. In IFIP Congress, pages 21--28, 1962.

[31]

Elliot Mendelson. Introduction to Mathematical Logic. Wadsworth Inc., 1987.

Digital Library

[32]

Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, parts I and II. Info. & Comp., 100(1):1--77, 1992.

Digital Library

[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 O'Hearn, Hongseok Yang, and John C. Reynolds. Separation and information hiding. In POPL'04, 2004.

Digital Library

[35]

Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002.

Digital Library

[36]

Andrew Pitts and Ian Stark. Operational reasoning for functions with local state. In HOOTS'98, CUP, pages 227--273, 1998.

Digital Library

[37]

John C. Reynolds. Separation logic: a logic for shared mutable data structures. In LICS'02, 2002.

Digital Library

[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 Trakhtenbrot, Joseph Halpern, and Albert Meyer. From Denotational to Operational and Axiomatic Semantics for ALGOLlike languages: an overview. In Logic of Programs, volume 164 of LNCS, pages 474--500, 1984.

Cited By

Xia SZhao J(2023)Static Entanglement Analysis of Quantum Programs2023 IEEE/ACM 4th International Workshop on Quantum Software Engineering (Q-SE)10.1109/Q-SE59154.2023.00013(42-49)Online publication date: May-2023
https://doi.org/10.1109/Q-SE59154.2023.00013
Brown NAltadmri A(2017)Novice Java Programming MistakesACM Transactions on Computing Education10.1145/299415417:2(1-21)Online publication date: 3-May-2017
https://dl.acm.org/doi/10.1145/2994154
Margolis JRyoo JGoode J(2017)Seeing Myself through Someone Else's EyesACM Transactions on Computing Education10.1145/296761617:2(1-18)Online publication date: 3-May-2017
https://dl.acm.org/doi/10.1145/2967616
Show More Cited By

Index Terms

A logical analysis of aliasing in imperative higher-order functions
1. Theory of computation
  1. Logic
    1. Programming logic
  2. Semantics and reasoning
    1. Program reasoning
      1. Assertions
      2. Program specifications

Recommendations

A logical analysis of aliasing in imperative higher-order functions
Proceedings of the tenth ACM SIGPLAN international conference on Functional programming

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 ...
A logical analysis of aliasing in imperative higher-order functions

We present a compositional programme 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 ...
Derivation and inference of higher-order strictness types

We extend an existing first-order typing system for strictness analysis to the fully higher-order case, covering both the derivation system and the inference algorithm. The resulting strictness typing system has expressive capabilities far beyond that ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming

September 2005

342 pages

ISBN:1595930647

DOI:10.1145/1086365

General Chair:
Olivier Danvy
BRICS, University of Aarhus, Denmark
,
Program Chair:
Benjamin C. Pierce
University of Pennsylvania

ACM SIGPLAN Notices Volume 40, Issue 9
Proceedings of the tenth ACM SIGPLAN international conference on Functional programming
September 2005
330 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1090189
Issue’s Table of Contents

Copyright © 2005 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 September 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ICFP05

Sponsor:

ICFP05: ACM SIGPLAN International Conference on Functional Programming

September 26 - 28, 2005

Tallinn, Estonia

Acceptance Rates

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

47
Total Citations
View Citations
382
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)1

Reflects downloads up to 30 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Xia SZhao J(2023)Static Entanglement Analysis of Quantum Programs2023 IEEE/ACM 4th International Workshop on Quantum Software Engineering (Q-SE)10.1109/Q-SE59154.2023.00013(42-49)Online publication date: May-2023
https://doi.org/10.1109/Q-SE59154.2023.00013
Brown NAltadmri A(2017)Novice Java Programming MistakesACM Transactions on Computing Education10.1145/299415417:2(1-21)Online publication date: 3-May-2017
https://dl.acm.org/doi/10.1145/2994154
Margolis JRyoo JGoode J(2017)Seeing Myself through Someone Else's EyesACM Transactions on Computing Education10.1145/296761617:2(1-18)Online publication date: 3-May-2017
https://dl.acm.org/doi/10.1145/2967616
Charguéraud AChakravarty MHu ZDanvy O(2011)Characteristic formulae for the verification of imperative programsProceedings of the 16th ACM SIGPLAN international conference on Functional programming10.1145/2034773.2034828(418-430)Online publication date: 19-Sep-2011
https://dl.acm.org/doi/10.1145/2034773.2034828
Charguéraud A(2011)Characteristic formulae for the verification of imperative programsACM SIGPLAN Notices10.1145/2034574.203482846:9(418-430)Online publication date: 19-Sep-2011
https://dl.acm.org/doi/10.1145/2034574.2034828
Nordio MCalcagno CMeyer BMüller PTschannen J(2010)Reasoning about function objectsProceedings of the 48th international conference on Objects, models, components, patterns10.5555/1894386.1894391(79-96)Online publication date: 28-Jun-2010
https://dl.acm.org/doi/10.5555/1894386.1894391
Nordio MCalcagno CMeyer BMüller PTschannen J(2010)Reasoning about Function ObjectsObjects, Models, Components, Patterns10.1007/978-3-642-13953-6_5(79-96)Online publication date: 2010
https://doi.org/10.1007/978-3-642-13953-6_5
Arthan RMartin UMathiesen EOliva P(2009)A general framework for sound and complete Floyd-Hoare logicsACM Transactions on Computational Logic10.1145/1614431.161443811:1(1-31)Online publication date: 6-Nov-2009
https://dl.acm.org/doi/10.1145/1614431.1614438
Kanig JFilliâtre JRossberg A(2009)WhoProceedings of the 2009 ACM SIGPLAN workshop on ML10.1145/1596627.1596634(39-48)Online publication date: 30-Aug-2009
https://dl.acm.org/doi/10.1145/1596627.1596634
Nanevski AGovereau PMorrisett GKennedy AAhmed A(2009)Towards type-theoretic semantics for transactional concurrencyProceedings of the 4th international workshop on Types in language design and implementation10.1145/1481861.1481872(79-90)Online publication date: 24-Jan-2009
https://dl.acm.org/doi/10.1145/1481861.1481872
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents