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. © Springer-Verlag 2012.
CITATION STYLE
Bouaziz, M., Logozzo, F., & Fähndrich, M. (2012). Inference of necessary field conditions with abstract interpretation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7705 LNCS, pp. 173–189). https://doi.org/10.1007/978-3-642-35182-2_13
Mendeley helps you to discover research relevant for your work.