Expressing heap-shape contracts in linear logic

Frances Perry, Limin Jia, David Walker

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationProceedings 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
Pages101-110
Number of pages10
DOIs
StatePublished - 2006
Event5th 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 - Portland, OR, United States
Duration: Oct 22 2006Oct 26 2006

Publication series

NameProceedings of the 5th International Conference on Generative Programming and Component Engineering, GPCE'06

Other

Other5th 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
CountryUnited States
CityPortland, OR
Period10/22/0610/26/06

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Information Systems
  • Software

Keywords

  • Assertions
  • Contracts
  • Heap shape
  • Linear logic

Fingerprint Dive into the research topics of 'Expressing heap-shape contracts in linear logic'. Together they form a unique fingerprint.

Cite this