×

Class invariants as abstract interpretation of trace semantics. (English) Zbl 1387.68052

Summary: We present a generic framework for the automatic and modular inference of sound class invariants for class-based object-oriented languages. We define a trace-based semantics for classes which considers all possible orderings, with all possible arguments, of invocations of all the methods of a class. We prove a correspondence theorem between such a semantics and a generic, trace-based, semantics for complete object-oriented programs. We express state-based class invariants in a fixpoint form by considering an abstraction of the class semantics, and we show how class invariants can be automatically inferred exploiting a static analysis of the methods. Furthermore, we address the problem of inferring a subclass invariant without accessing to the parent code, but just to its invariant.

MSC:

68N15 Theory of programming languages
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68Q55 Semantics in the theory of computing
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Meyer B. Object-oriented software construction, 2nd ed. Professional Technical Reference. Englewood Cliffs, NJ: Prentice-Hall; 1997. · Zbl 0987.68516
[2] Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X. A static analyzer for large safety-critical software. In: Proceedings of the 2003 ACM conference on programming language design and implementation (PLDI’03). June 2003. New York: ACM Press; p. 196-207. · Zbl 1026.68514
[3] Cousot P, Halbwachs N. Automatic discovery of linear restraints among variables of a program. In: Fifth ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL ’78). New York: ACM Press; 1978. p. 84-97.
[4] Handjieva M, Tzolovski S. Refining static analyses by trace-based partitioning using control flow. In: Proceedings of the static analysis symposium (SAS ’98). Lecture notes in computer science, vol. 1503. Berlin: Springer; 1998. p. 200-15.
[5] Tarski, A., A lattice-theoretical fixpoint theorem and its applications, Pacific journal of mathematics, 5, 285-309, (1955) · Zbl 0064.26004
[6] Cousot P, Cousot R. Systematic design of program analysis frameworks. In: Sixth ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL ’79). New York: ACM Press; 1979. p. 269-82.
[7] Cousot P, Cousot R. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Fourth ACM symposium on principles of programming languages (POPL ’77). January 1977, New York: ACM Press; 1977. p. 238-52.
[8] Cousot, P.; Cousot, R., Abstract interpretation frameworks, Journal of logic and computation, 2, 4, 511-547, (1992) · Zbl 0783.68073
[9] Lindholm T, Yellin F. The Java virtual machine specification, 2nd ed. The Java Series. Reading, MA: Addison-Wesley, Longman; 1999.
[10] Spoto, F.; Jensen, T., Class analyses as abstract interpretations of trace semantics, ACM transactions on programming languages and systems (TOPLAS), 25, 5, 578-630, (2003)
[11] Logozzo F. Separate compositional analysis of class-based object-oriented languages. In: Proceedings of the 10th international conference on algebraic methodology and software technology (AMAST’2004). Lecture notes in computer science, vol. 3116. Berlin: Springer; 2004. p. 332-46.
[12] Igarashi A, Pierce B, Wadler P. Featherweight Java: a minimal core calculus for Java and GJ. In: 14th ACM SIGPLAN conference on object-oriented programming, systems, languages & applications (OOPSLA’99). ACM SIGPLAN notices, vol. 34(10). New York: ACM Press; 1999. p. 132-46.
[13] Lewis J, Loftus W. Java software solutions, second ed. Update. Reading, MA: Addison-Wesley, Longman; 2001. · Zbl 0898.68009
[14] Gosling J, Joy B, Steele G, Bracha G. The Java language specification, 2nd ed. Sun Microsystems, 2001. · Zbl 0865.68001
[15] Granger P. Static analysis of linear congruence equalities among variables of a program. In: International joint conference on theory and practice of software development (TAPSOFT ’91). Lecture notes in computer science, vol. 464. Berlin: Springer, 1991. p. 169-92.
[16] Arnout K, Meyer B. Finding implicit contracts in .NET components. In: First international symposium on formal methods for components and objects (FMCO 2002). Lectures notes in computer science, vol. 2852. Berlin: Springer; 2002. p. 285-318.
[17] Cousot P. Asynchronous iterative methods for solving a fixed point system of monotone equations in a complete lattice. Research report R.R 88, Laboratoire IMAG, Université Scientifique et Médicale de Grenoble, Grenoble, France, September 1977.
[18] Bracha G, Cook WR. Mixin-based inheritance. In: Fifth ACM conference on object-oriented programming, systems, languages and applications (OOPSLA ’90). SIGPLAN notices, vol. 25(10). New York: ACM Press; 1990. p. 303-11.
[19] Cook, W.R.; Palsberg, J., A denotational semantics of inheritance and its correctness, Information and computation, 114, 2, 329-350, (1994)
[20] Palsberg, J.; Schwartzbach, M.I., Object-oriented type systems, (1994), Wiley Chichester · Zbl 0821.68023
[21] Palsberg J, Schwartzbach MI. Object-oriented type inference. In: Proceedings of the ACM SIGPLAN conference on object-oriented programming (OOPSLA’91). New York: ACM Press; 1991.
[22] Eckel B. Thinking in C++, 2nd ed., vol. 1. Englewood Cliffs, NJ: Prentice-Hall; 2000.
[23] Logozzo F. Automatic inference of class invariants. In: Proceedings of the fifth conference on verification, model checking and abstract interpretation (VMCAI ’04). Lectures notes in computer science, vol. 2937. Berlin: Springer; 2004. p. 211-22.
[24] Logozzo F. An approach to behavioral subtyping based on static analysis. In: Proceedings of the international workshop on test and analysis of component based systems (TACoS 2004), April 2004. Electronic Notes in Theoretical Computer Science. Amsterdam: Elsevier Science; 2004.
[25] Logozzo F. Modular static analysis of object-oriented Languages. PhD thesis, Ecole Polytechnique, June 2004. · Zbl 1108.68398
[26] Logozzo F. Class-level modular analysis for object oriented languages. In: Proceedings of the 10th static analysis symposium 2003 (SAS ’03). Lecture notes in computer science, vol. 2694. Berlin: Springer; 2003. p. 37-54. · Zbl 1067.68548
[27] Logozzo F, Cortesi A. Semantic class hierarchies by abstract interpretation. Research report CS-2004-7, Department of Computer Science, University Ca’ Foscari of Venice, Italy. · Zbl 1176.68046
[28] Genaim S, Codish M. Incremental refinement of semantic based program analysis for logic programs. In: Proceedings of the 22nd Australasian computer science conference. Berlin: Springer; January 1999. · Zbl 0959.68021
[29] Microsoft Inc. The component object model specification. Microsoft, 2003. .
[30] Leavens GT, Baker AL, Ruby C. Preliminary design of JML: a behavioral interface specification language for Java, November 2003. .
[31] Flanagan C, Leino KRM. Houdini, an annotation assistant for ESC/Java. In: Proceedings of the international symposium of formal methods Europe (FME 2001). Lecture notes in computer science, vol. 2021. Berlin: Springer; 2001. p. 500-17.
[32] Ernst M. Dynamically discovering likely program invariants. PhD thesis, University of Washington Department of Computer Science and Engineering, 2002.
[33] Flanagan C, Leino KRM, Lillibridge M, Nelson G, Saxe JB, Stata R. Extended static checking for Java. In: Proceedings of the 2002 ACM SIGPLAN conference on programming language design and implementation (PLDI’02). June 2002. New York: ACM Press; 2002. p. 234-45.
[34] Meyer, B., Eiffel the language, (1992), Prentice-Hall Englewood Cliffs, NJ · Zbl 0779.68013
[35] Free Software Foundation. Nana: improved support for assertions and logging. GNU, 2003. .
[36] Huizing K, Kuiper R. Verification of object oriented programs using class invariants. In: Fundamental approaches to software engineering, third international conference (FASE 2000), April 2000. Lecture notes in computer science, vol. 1783. Berlin: Springer; 2000. p. 208-21.
[37] Guttag JV, Horning SJ, Garland JJ, Jones KD, Modet A, Wing JM. Larch: languages and tools for formal specification. Texts and Monographs in Computer Science. Berlin: Springer; 1993.
[38] Jacobs B, van den Berg J, Huismann H, van Berkum M, Hensel U, Tews H. Reasoning about Java classes (preliminary report). In: 13th ACM SIGPLAN conference on object-oriented programming, systems, languages & applications (OOPSLA’98) October 1998. SIGPLAN notices, vol. 33(10). New York: ACM Press; 1998.
[39] Microsoft Inc. The .net framework. .
[40] Microsoft Inc. Microsoft C# Language Specifications. Microsoft Press, 2001.
[41] Microsoft Inc. Visual C++ .net. .
[42] Zee K, Rinard M. Write barrier removal by static analysis. In: 17th annual ACM conference on object-oriented programming, systems, languages and applications (OOPSLA ’02). SIGPLAN notices, vol. 37(11). New York: ACM Press; 2002. p. 191-210.
[43] Pollet I, Le Charlier B, Cortesi A. Distinctness and sharing domains for static analysis of Java programs. In: Proceedings of the European conference on object oriented programming (ECOOP ’01). Lecture notes in computer science, vol. 2072. Berlin: Springer; 2001. p. 77-98.
[44] Blanchet B. Escape analysis for object oriented languages. Application to Java. In: 14th ACM conference on object-oriented programming, systems, languages and applications (OOPSLA’99), Denver, Colorado, November 1999. p. 20-34.
[45] Chatterjee R, Ryder BG, Landi WA. Relevant context inference. In: 26th ACM SIGPLAN symposium on principles of programming languages (POPL ’99). New York, NY, USA: ACM Press; 1999. p. 133-46.
[46] Probst C. Modular control flow analysis for libraries. In: Proceedings of the static analysys symposium (SAS ’02). Lecture notes in computer science, vol. 2477. Berlin; Springer, 2002. p. 165-79. · Zbl 1015.68508
[47] Aggarwal A, Randall KH. Related field analysis. In: ACM SIGPLAN conference on programming language design and implementation (PLDI ’01). SIGPLAN notices, vol.36(5). New York: ACM Press; 2001. p. 214-20.
[48] Ghemawat S, Randall KH, Scales DJ. Field analysis: getting useful and low-cost interprocedural information. In: Proceedings of the 2000 ACM SIGPLAN conference on programming language design and implementation (PLDI’00). ACM SIGPLAN notices, vol. 35(5). New York: ACM Press, 2000. p. 334-44.
[49] Detlefs D. Automatic inference of reference-count invariants. In: Proceedings of the second ACM workshop on semantics, programme analysis, and computing environments for memory management. New York: ACM Press; 2004.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.