Precondition Inference from Intermittent Assertions and Application to Contracts on Collections

Patrick Cousot 1, 2 Radhia Cousot 1, 2 Logozzo Francesco 3
2 ABSTRACTION - Abstract Interpretation and Static Analysis
DI-ENS - Département d'informatique de l'École normale supérieure, ENS Paris - École normale supérieure - Paris, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
Abstract : In the context of program design by contracts, programmers often insert assertions in their code to be optionally checked at runtime, at least during the debugging phase. These assertions would better be given as a precondition of the method/procedure in which they appear. Potential errors would be discovered earlier and, more importantly, the precondition could be used in the context of separate static program analysis as part of the abstract semantics of the code. However in the case of collections (data structures such as arrays, lists, etc) checking both the precondition and the assertions at runtime appears superfluous and costly. So the precondition is often omitted since it is checked anyway at runtime by the assertions. It follows that the static analysis can be much less precise, a fact that can be difficult to understand since ''the precondition and assertions are equivalent'' (i.e. at runtime, up to the time at which warnings are produced, but not statically) e.g. for separate static analysis. We define precisely and formally the contract inference problem from intermittent assertions on scalar variables and elements of collections 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. 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.
Type de document :
Communication dans un congrès
Ranjit Jhala and David Schmidt. Proceedings of the 12th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'11), Jan 2011, Austin, Texas, United States. Springer-Verlag, 2011, Lecture Notes in Computer Science
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00543881
Contributeur : Patrick Cousot <>
Soumis le : lundi 6 décembre 2010 - 18:11:08
Dernière modification le : jeudi 11 janvier 2018 - 06:22:10
Document(s) archivé(s) le : vendredi 2 décembre 2016 - 21:01:22

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00543881, version 1

Collections

Citation

Patrick Cousot, Radhia Cousot, Logozzo Francesco. Precondition Inference from Intermittent Assertions and Application to Contracts on Collections. Ranjit Jhala and David Schmidt. Proceedings of the 12th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'11), Jan 2011, Austin, Texas, United States. Springer-Verlag, 2011, Lecture Notes in Computer Science. 〈inria-00543881〉

Partager

Métriques

Consultations de la notice

289

Téléchargements de fichiers

232