Lazy contract checking for immutable data structures

Robert Bruce Findler, Shu Yu Guo, Anne Rogers

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

22 Scopus citations


Existing contract checkers for data structures force programmers to choose between poor alternatives. Contracts are either built into the functions that construct the data structure, meaning that each object can only be used with a single contract and that a data structure with an invariant cannot be viewed as a subtype of the data structure without the invariant (thus inhibiting abstraction) or contracts are checked eagerly when an operation on the data structure is invoked, meaning that many redundant checks are performed, potentially even changing the program's asymptotic complexity. We explore the idea of adding a small, controlled amount of laziness to contract checkers so that the contracts on a data structure are only checked as the program inspects the data structure. Unlike contracts on the constructors, our lazy contracts allow subtyping and thus preserve the potential for abstraction. Unlike eagerly-checked contracts, our contracts do not affect the asymptotic behavior of the program. This paper presents our implementation of these ideas, an optimization in our implementation, performance measurements, and a discussion of an extension to our implementation that admits more expressive contracts by loosening the strict asymptotic guarantees and only preserving the amortized asymptotic complexity.

Original languageEnglish (US)
Title of host publicationImplementation and Application of Functional Languages - 19th International Symposium, IFL 2007, Revised Selected Papers
Number of pages18
StatePublished - 2008
Event19th International Symposium on Implementation and Application of Functional Languages, IFL 2007 - Freiburg, Germany
Duration: Sep 27 2007Sep 29 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5083 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other19th International Symposium on Implementation and Application of Functional Languages, IFL 2007

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Lazy contract checking for immutable data structures'. Together they form a unique fingerprint.

Cite this