TY - GEN
T1 - Expressing heap-shape contracts in linear logic
AU - Perry, Frances
AU - Jia, Limin
AU - Walker, David
N1 - Copyright:
Copyright 2011 Elsevier B.V., All rights reserved.
PY - 2006
Y1 - 2006
N2 - 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.
AB - 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.
KW - Assertions
KW - Contracts
KW - Heap shape
KW - Linear logic
UR - http://www.scopus.com/inward/record.url?scp=34547468242&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=34547468242&partnerID=8YFLogxK
U2 - 10.1145/1173706.1173723
DO - 10.1145/1173706.1173723
M3 - Conference contribution
AN - SCOPUS:34547468242
SN - 1595932372
SN - 9781595932372
T3 - Proceedings of the 5th International Conference on Generative Programming and Component Engineering, GPCE'06
SP - 101
EP - 110
BT - Proceedings of the 5th Int. Conf. on Generative Programming and Component Eng., GPCE'06. Co-located with the 21st Int. Conf. on Object-Oriented Programm., Syst., Languages, and Applic.OOPSLA 2006
T2 - 5th International Conference on Generative Programming and Component Engineering, GPCE'06. Co-located with the 21st International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2006
Y2 - 22 October 2006 through 26 October 2006
ER -