Geodesic
Integration of semantic verification into Java compilers
Modelirovanie i analiz informacionnyh sistem, Tome 17 (2010) no. 4, pp. 70-77 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice de l'article

This paper introduces a method for static semantic analysis of source codes at compilation time directly within standard compilers. The method is implemented via unified integration with Java compilers to get the full access to Abstract Syntax Tree (AST) of compiled files after the semantic analysis stage of compilation process. The unified integration is implemented by common AST interfaces and adapters to AST implementations of Sun/Oracle javac and Eclipse Compiler for Java (ecj) compilers. This method provides transparent integration with Eclipse and Netbeans IDE without a need for any special plugins. Several examples of program verification rules are presented to demonstrate the method.
Keywords: program verification, AST, Eclipse IDE, Netbeans IDE.
Mots-clés : Java, compiler, JSR269, javac, ecj 
@article{MAIS_2010_17_4_a7,
     author = {A. V. Klepinin and A. A. Melent'ev},
     title = {Integration of semantic verification into {Java} compilers},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {70--77},
     year = {2010},
     volume = {17},
     number = {4},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a7/}
}
TY  - JOUR
AU  - A. V. Klepinin
AU  - A. A. Melent'ev
TI  - Integration of semantic verification into Java compilers
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2010
SP  - 70
EP  - 77
VL  - 17
IS  - 4
UR  - http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a7/
LA  - ru
ID  - MAIS_2010_17_4_a7
ER  - 
%0 Journal Article
%A A. V. Klepinin
%A A. A. Melent'ev
%T Integration of semantic verification into Java compilers
%J Modelirovanie i analiz informacionnyh sistem
%D 2010
%P 70-77
%V 17
%N 4
%U http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a7/
%G ru
%F MAIS_2010_17_4_a7
A. V. Klepinin; A. A. Melent'ev. Integration of semantic verification into Java compilers. Modelirovanie i analiz informacionnyh sistem, Tome 17 (2010) no. 4, pp. 70-77. http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a7/

[1] PMD, Java source code verificator, http://pmd.sourceforge.net/

[2] Findbugs, Java byte code verificator, http://findbugs.sourceforge.net/

[3] N. Ayewah, W. Pugh, J. D. Morgenthaler, J. Penix, Y. Zhou, “Using FindBugs on production software”, OOPSLA '07: Companion to the 22nd ACM SIGPLAN conference on Object-oriented programming systems and applications companion, ACM, New York, NY, USA, 2007, 805–806

[4] H. Klaus, R. Grigore, “An Overview of the Runtime Verification Tool Java PathExplorer”, Formal Methods in System Design, 24:2 (2004), 189–215 | DOI | MR | Zbl

[5] JSR269: Pluggable Annotation Processing API, http://jcp.org/en/jsr/detail?id=269

[6] Project Lombok, http://projectlombok.org/

[7] M. M. Papi, M. Ali, T. L. Jr. Correa, J. H. Perkins, M. D. Ernst, “Practical pluggable types for Java”, ISSTA 2008, Proceedings of the 2008 International Symposium on Software Testing and Analysis (July 22–24), Seattle, WA, USA, 2008, 201–212

[8] Universal AST project for Checker Framework, http://code.google.com/p/checker-framework/wiki/Ideas#Universal_AST

[9] Java Unified Abstract Syntax Tree project, http://bitbucket.org/amelentev/juast/

[10] java.util.ServiceLoader, http://java.sun.com/javase/6/docs/api/java/util/ServiceLoader.html