Integration of semantic verication into Java compilers
Abstract
This paper introduces a method for static semantic analysis of source codes at com-
pilation time directly within standard compilers. The method is implemented via unied
integration with Java compilers to get the full access to Abstract Syntax Tree (AST)
of compiled les after the semantic analysis stage of compilation process. The unied
integration is implemented by common AST interfaces and adapters to AST implemen-
tations 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 verication rules are presented to demon-
strate the method.
pilation time directly within standard compilers. The method is implemented via unied
integration with Java compilers to get the full access to Abstract Syntax Tree (AST)
of compiled les after the semantic analysis stage of compilation process. The unied
integration is implemented by common AST interfaces and adapters to AST implemen-
tations 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 verication rules are presented to demon-
strate the method.
About the Authors
A. V. Klepinin
Уральский Государственный Университет им.А.М.Горького
Russian Federation
Russian Federation
A. A. Melentyev
Уральский Государственный Университет им.А.М.Горького
Russian Federation
Russian Federation
References
1. PMD, java source code verificator. [Электрон. ресурс]. Режим доступа: http://pmd.sourceforge.net/.
2. Findbugs, java byte code verificator. [Электрон. ресурс]. Режим доступа: http://findbugs.sourceforge.net/.
3. Ayewah N., Pugh W., Morgenthaler J. D., Penix J., and Zhou Y. Using findbugs on production software // OOPSLA '07: Companion to the 22nd ACM SIGPLAN conference on Object-oriented programming systems and applications companion, (New York, NY, USA). ACM, 2007. P. 805-806.
4. Klaus H. and Grigore R. An overview of the runtime verification tool Java PathExplorer // Formal Methods in System Design. 2004. Vol. 24, No. 2. P. 189-215.
5. JSR269: Pluggable Annotation Processing API. [Электрон. ресурс]. Режим доступа: http://jcp.org/en/jsr/detail?id=269.
6. Project lombok. [Электрон. ресурс]. Режим доступа: http://projectlombok.org/.
7. Papi M. M., Ali M., Correa Jr. T. L., Perkins J. H., and Ernst M. D. , Practical pluggable types for Java // ISSTA 2008, Proceedings of the 2008 International Symposium on Software Testing and Analysis, (Seattle,WA, USA). 2008. July 22-24. P. 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.
Review
For citations:
Klepinin A.V., Melentyev A.A. Integration of semantic verication into Java compilers. Modeling and Analysis of Information Systems. 2010;17(4):70-77. (In Russ.)
Views:
550
Email this article 