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.

Keywords

• program veri cation
• ast
• java
• compiler
• jsr269
• javac
• ecj
• eclipse ide
• netbeans ide