Mehdi Bouaziz, Francesco Logozzo, and Manuel Fähndrich
Inference of Necessary Field Conditions with Abstract Interpretation
in 10th Asian Symposium on Programming Languages and Systems (APLAS 2012), Springer, December 2012
- PDF, 16 pages, 358 KB
- Abstract: We present a new static analysis to infer necessary field conditions for object-oriented programs. A necessary field condition is a property that should hold on the fields of a given object, for otherwise there exists a calling context leading to a failure due to bad object state. Our analysis also infers the provenance of the necessary condition, so that if a necessary field condition is violated then an explanation containing the sequence of method calls leading to a failing assertion can be produced.
When the analysis is restricted to readonly fields, i.e., fields that can only be set in the initialization phase of an object, it infers object invariants. We provide empirical evidence on the usefulness of necessary field conditions by integrating the analysis into cccheck, our static analyzer for .NET. Robust inference of readonly object field invariants was the #1 request from cccheck users. - @inproceedings{BouazizLogozzoFahndrich-APLAS12,
author = {Bouaziz, Mehdi and Francesco Logozzo and Manuel Fähndrich},
title = {Inference of Necessary Field Conditions with Abstract Interpretation},
year = {2012},
month = {December},
booktitle = {10th Asian Symposium on Programming Languages and Systems (APLAS 2012)},
series = {Lecture Notes in Computer Science},
volume = {7705},
pages = {173--189},
publisher = {Springer},
url = {http://www.bouaziz.me/p/BouazizLogozzoFahndrich-APLAS12.pdf},
doi = {10.1007/978-3-642-35182-2_13}
}
Last update: January 24, 2014