Article

Expressing heap-shape contracts in linear logic

Authors:

David WalkerAuthors Info & Claims

GPCE '06: Proceedings of the 5th international conference on Generative programming and component engineering

Pages 101 - 110

https://doi.org/10.1145/1173706.1173723

Published: 22 October 2006 Publication History

Abstract

Contracts (dynamically checked programmer assertions) are a widely accepted mechanism for specifying, checking and documenting properties of software components. Most, if not all, contract systems expect programmers to use the native programming language to express their program invariants. While this is most effective for many simple invariants, expressing properties of data structures and aliasing patterns can be extremely complicated. If written in the native language in an unstructured way, such contracts are bound to be unclear and ineffective as documentation. In this paper, we show how to use linear logic as a language of contracts for an imperative programming language. The high-level nature of our linear logical contracts makes specifying memory shape and aliasing properties of complex recursive data structures easy. Moreover, since we give our logic a clear, compositional semantics, the contracts serve as effective, executable documentation for programmer expectations. In order to evaluate the truth of our linear logical contracts at run time, we use a modified version of LolliMon, a linear logic programming language.

References

[1]

A. Ahmed and D. Walker. The logical approach to stack typing. In ACM SIGPLAN Workshop on Types in Language Design and Implementation, New Orleans, Jan. 2003.]]

Digital Library

[2]

A. W. Appel and D. A. McAllester. An indexed model of recursive types for foundational proof-carrying code. Programming Languages and Systems, 23(5):657--683, 2001.]]

Digital Library

[3]

L. Birkedal, N. Torp-Smith, and J. Reynolds. Local reasoning about a copying garbage collector. In ACM Symposium on Principles of Programming Languages, pages 220--231, Venice, Italy, Jan. 2004.]]

Digital Library

[4]

R. B. Findler and M. Felleisen. Contracts for higher-order functions. In ICFP '02: Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, pages 48--59, New York, NY, USA, 2002. ACM Press.]]

Digital Library

[5]

R. Hastings and B. Joyce. Fast detection of memory leaks and access errors. In Proceedings of the Winter '92 USENIX conference, pages 125--136. USENIX Association, 1992.]]

[6]

M. Hauswirth and T. M. Chilimbi. Low-overhead memory leak detection using adaptive statistical profiling. In ASPLOS, pages 156--164, 2004.]]

Digital Library

[7]

J. S. Hodas and D. Miller. Logic programming in a fragment of intuitionistic linear logic. In Papers presented at the IEEE symposium on Logic in computer science, pages 327--365, Orlando, FL, USA, 1994. Academic Press, Inc.]]

Digital Library

[8]

R. C. Holt and J. R. Cordy. The Turing programming language. Commun. ACM, 31(12):1410--1423, 1988.]]

Digital Library

[9]

S. Ishtiaq and P. O'Hearn. BI as an assertion language for mutable data structures. In Twenty-Eighth ACM Symposium on Principles of Programming Languages, pages 14--26, London, UK, Jan. 2001.]]

Digital Library

[10]

L. Jia, F. Spalding, D. Walker, and N. Glew. Certifying compilation for a language with stack allocation. In Proceedings of the Twentieth Annual IEEE Symp. on Logic in Computer Science, LICS 2005, 2005.]]

Digital Library

[11]

L. Jia and D. Walker. ILC: A foundation for automated reasoning about pointer programs. In European Symposium on Programming Languages, Apr. 2006.]]

Digital Library

[12]

P. López, F. Pfenning, J. Polakow, and K. Watkins. Monadic concurrent linear logic programming. In PPDP '05, pages 35--46, New York, NY, USA, 2005. ACM Press.]]

Digital Library

[13]

P. López and J. Polakow. Implementing efficient resource management for linear logic programming. In Logic for Programming Artificial Intelligence and Reasoning (LPAR), pages 528--543, 2004.]]

[14]

D. C. Luckham. Programming with Specifications: An Introduction to Anna, a Language for Specifying ADA Programs. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 1990.]]

Digital Library

[15]

B. Meyer. Eiffel: programming for reusability and extendibility. SIGPLAN Not., 22(2):85--94, 1987.]]

Digital Library

[16]

B. Meyer. Eiffel: the language. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1992.]]

Digital Library

[17]

G. Morrisett, A. Ahmed, and M. Fluet. L3: A linear language with locations. In Seventh International Conference on Typed Lambda Calculi and Applications, Apr. 2005.]]

Digital Library

[18]

P. O'Hearn and D. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215--244, 1999.]]

[19]

P. O'Hearn, J. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In Computer Science Logic, number 2142 in LNCS, pages 1--19, Paris, 2001.]]

Digital Library

[20]

D. L. Parnas. A technique for software module specification with examples. Commun. ACM, 15(5):330--336, 1972.]]

Digital Library

[21]

Programming with assertions. http://java.sun.com/j2se/1.4.2/docs /guide/lang/assert.html.]]

[22]

J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, pages 55--74. 2002.]]

Digital Library

Cited By

Banerjee RMemarian KMakwana DPulte CKrishnaswami NSewell P(2025)Fulminate: Testing CN Separation-Logic Specifications in CProceedings of the ACM on Programming Languages10.1145/37048799:POPL(1260-1292)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704879
Nguyen HKuncak VChin W(2008)Runtime checking for separation logicProceedings of the 9th international conference on Verification, model checking, and abstract interpretation10.5555/1787526.1787545(203-217)Online publication date: 7-Jan-2008
https://dl.acm.org/doi/10.5555/1787526.1787545
Nguyen HKuncak VChin W(2008)Runtime Checking for Separation LogicVerification, Model Checking, and Abstract Interpretation10.1007/978-3-540-78163-9_19(203-217)Online publication date: 2008
https://doi.org/10.1007/978-3-540-78163-9_19
Show More Cited By

Index Terms

Expressing heap-shape contracts in linear logic
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
2. Theory of computation

Recommendations

The decidability of the intensional fragment of classical linear logic

Intensional classical linear logic (MELL) is proved decidable.Intensional interlinear logic (RLL) is proved decidable.We adapt Kripke's method used to prove decidability for some relevance logics.The semi-relevant RLL emerges as a logic superior to MELL ...
Linear and temporal logic programming language
ACS'06: Proceedings of the 6th WSEAS international conference on Applied computer science

Recent logic calculi open new possibilities for logic programming. Apparently the most important of them is a linear logic which makes possible to solve problems by resources treatment. The linear logic has already been used for several proposals of ...
Monadic concurrent linear logic programming
PPDP '05: Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming

Lolli is a logic programming language based on the asynchronous propositions of intuitionistic linear logic. It uses a backward chaining, backtracking operational semantics. In this paper we extend Lolli with the remaining connectives of intuitionistic ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

GPCE '06: Proceedings of the 5th international conference on Generative programming and component engineering

October 2006

310 pages

ISBN:1595932372

DOI:10.1145/1173706

General Chair:
Stan Jarzabek
National University of Singapore, Singapore
,
Program Chairs:
Douglas Schmidt
Vanderbilt University, USA
,
Todd Veldhuizen
University of Waterloo, Canada

Copyright © 2006 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: 22 October 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

GPCE06

Sponsor:

GPCE06: Generative Programming and Component Engineering 2006

October 22 - 26, 2006

Oregon, Portland, USA

Acceptance Rates

Overall Acceptance Rate 56 of 180 submissions, 31%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
126
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)0

Reflects downloads up to 25 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Banerjee RMemarian KMakwana DPulte CKrishnaswami NSewell P(2025)Fulminate: Testing CN Separation-Logic Specifications in CProceedings of the ACM on Programming Languages10.1145/37048799:POPL(1260-1292)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704879
Nguyen HKuncak VChin W(2008)Runtime checking for separation logicProceedings of the 9th international conference on Verification, model checking, and abstract interpretation10.5555/1787526.1787545(203-217)Online publication date: 7-Jan-2008
https://dl.acm.org/doi/10.5555/1787526.1787545
Nguyen HKuncak VChin W(2008)Runtime Checking for Separation LogicVerification, Model Checking, and Abstract Interpretation10.1007/978-3-540-78163-9_19(203-217)Online publication date: 2008
https://doi.org/10.1007/978-3-540-78163-9_19
Chang BRival XNecula G(2007)Shape analysis with structural invariant checkersProceedings of the 14th international conference on Static Analysis10.5555/2391451.2391477(384-401)Online publication date: 22-Aug-2007
https://dl.acm.org/doi/10.5555/2391451.2391477
Chang BRival XNecula G(2007)Shape Analysis with Structural Invariant CheckersStatic Analysis10.1007/978-3-540-74061-2_24(384-401)Online publication date: 2007
https://doi.org/10.1007/978-3-540-74061-2_24

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.

Figures

Tables

Media

View Table of Conten