Precondition inference from intermittent assertions and application to contracts on collections

Patrick Cousot, Radhia Cousot, Francesco Logozzo

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

Abstract

Programmers often insert assertions in their code to be optionally checked at runtime, at least during the debugging phase. In the context of design by contracts, these assertions would better be given as a precondition of the method/procedure which can detect that a caller has violated the procedure's contract in a way which definitely leads to an assertion violation (e.g., for separate static analysis). We define precisely and formally the contract inference problem from intermittent assertions inserted in the code by the programmer. Our definition excludes no good run even when a non-deterministic choice (e.g., an interactive input) could lead to a bad one (so this is not the weakest precondition, nor its strengthening by abduction, since a terminating successful execution is not guaranteed). We then introduce new abstract interpretation-based methods to automatically infer both the static contract precondition of a method/procedure and the code to check it at runtime on scalar and collection variables.

Original languageEnglish (US)
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Proceedings
Pages150-168
Number of pages19
DOIs
StatePublished - 2011
Event12th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2011 - Austin, TX, United States
Duration: Jan 23 2011Jan 25 2011

Publication series

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

Other

Other12th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2011
CountryUnited States
CityAustin, TX
Period1/23/111/25/11

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Precondition inference from intermittent assertions and application to contracts on collections'. Together they form a unique fingerprint.

  • Cite this

    Cousot, P., Cousot, R., & Logozzo, F. (2011). Precondition inference from intermittent assertions and application to contracts on collections. In Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Proceedings (pp. 150-168). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6538 LNCS). https://doi.org/10.1007/978-3-642-18275-4_12