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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Arnout, K., Meyer, B.: Uncovering hidden contracts: The. NET example. IEEE Computer 36(11), 48–55 (2003)
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)
Barnett, M., Fähndrich, M., Garbervetsky, D., Logozzo, F.: Annotations for (more) precise points-to analysis. In: IWACO 2007, Stockholm U. and KTH (2007)
Barnett, M., Fähndrich, M., Logozzo, F.: Embedded contract languages. In: SAC 2010, pp. 2103–2110. ACM, New York (2010)
Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers 58, 118–149 (2003)
Bourdoncle, F.: Abstract debugging of higher-order imperative languages. In: PLDI 1993, pp. 46–55. ACM, New York (1993)
Calcagno, C., Distefano, D., O’Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: 36th POPL, pp. 289–300. ACM, New York (2009)
Chandra, S., Fink, S., Sridharan, M.: Snugglebug: a powerful approach to weakest preconditions. In: PLDI, pp. 363–374. ACM, New York (2009)
Cousot, P.: Méthodes itératives de construction et d’approximation de points fixes d’opérateurs monotones sur un treillis, analyse sémantique de programmes (in French). Thèse d’État ès sciences mathématiques, Université scientifique et médicale de Grenoble (1978)
Cousot, P.: Semantic foundations of program analysis. In: Muchnick, S., Jones, N. (eds.) Program Flow Analysis: Theory and Applications, ch. 10, pp. 303–342. Prentice-Hall, Englewood Cliffs (1981)
Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. TCS 277(1-2), 47–103 (2002)
Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: Neuhold, E. (ed.) IFIP Conf. on Formal Description of Programming Concepts, pp. 237–277. North-Holland, Amsterdam (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: 6th POPL, pp. 269–282. ACM, New York (1979)
Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. Journal of Logic Programming 13(2-3), 103–179 (1992)
Cousot, P., Cousot, R.: Modular static program analysis. In: CC 2002. LNCS, vol. 2304, pp. 159–178. Springer, Heidelberg (2002)
Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: POPL 2011. ACM, New York (2011)
Dijkstra, E.: Guarded commands, nondeterminacy and formal derivation of programs. CACM 18(8), 453–457 (1975)
Fähndrich, M., Logozzo, F.: Clousot: Static contract checking with abstract interpretation. In: FoVeOOS. Springer, Heidelberg (2010)
Flanagan, C., Leino, K., Lillibridge, M., Nelson, G., Saxe, J., Stata, R.: Extended Static Checking for Java. In: PLDI, pp. 234–245. ACM, New York (2002)
Gulwani, S., Tiwari, A.: Computing procedure summaries for interprocedural analysis. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 253–267. Springer, Heidelberg (2007)
Hecht, M.: Flow Analysis of Computer Programs. Elsevier, North-Holland (1977)
King, J.: Symbolic execution and program testing. CACM 19(7), 385–394 (1976)
Meyer, B.: Eiffel: The Language. Prentice-Hall, Englewood Cliffs (1991)
Meyer, B.: Applying “Design by Contract”. IEEE Computer 25(10), 40–51 (1992)
Moy, Y.: Sufficient preconditions for modular assertion checking. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 188–202. Springer, Heidelberg (2008)
Park, D.: Fixpoint induction and proofs of program properties. In: Meltzer, B., Michie, D. (eds.) Machine Intelligences, vol. 5, pp. 59–78. Edinburgh University Press, Edinburgh (1969)
Rival, X.: Understanding the origin of alarms in astrée. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 303–319. Springer, Heidelberg (2005)
Lev-Ami, T., Sagiv, M., Reps, T., Gulwani, S.: Backward analysis for inferring quantified preconditions. Tr-2007-12-01, Tel Aviv University (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cousot, P., Cousot, R., Logozzo, F. (2011). Precondition Inference from Intermittent Assertions and Application to Contracts on Collections. In: Jhala, R., Schmidt, D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2011. Lecture Notes in Computer Science, vol 6538. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-18275-4_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-18275-4_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-18274-7
Online ISBN: 978-3-642-18275-4
eBook Packages: Computer ScienceComputer Science (R0)