P. Cousot, R. Cousot, and F. Logozzo, Contract Precondition Inference from Intermittent Assertions on Collections

Patrick Cousot
Contract Precondition Inference from Intermittent Assertions on Collections
(work with Radhia Cousot and Francesco Logozzo), The Future of Software Engineering (FOSE) Symposium, ETH Zürich, Switzerland, 22-23 November 2010.
Abstract:
In the context of 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 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. 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.
Slides of the 45 mn presentation (to be used with Acrobat Reader):
- .pdf, 4 slide per page (31.9 Mb)

Bibliographic reference:

\bibitem{CousotPRLogozzo-FOSE-2010-11-23}
P.~Cousot, R.~Cousot, and F.~Logozzo.
\newblock Contract Precondition Inference from Intermittent Assertions on Collections.
\newblock The Future of Software Engineering (FOSE) Symposium, ETH Z\"urich, Switzerland,
           23 November 2010.

@inProceedings{CousotPRLogozzo-FOSE-2010-11-23,
   author =    {P.~Cousot and R.~Cousot and F.~Logozzo},
   title =     {Contract Precondition Inference from Intermittent Assertions on Collections},
   booktitle = {The Future of Software Engineering (FOSE) Symposium},
   address =   {ETH Z\"urich, Switzerland},
   month =     {23 November },
   year =      {2010},
}

Copyright notice
Last modified: Saturday, 27-Nov-2010 17:06:21 CET