maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State Universitymais-1053Research ArticleОригинальные статьиArticlesИнтеграция семантических верификаторов в компиляторы языка JavaIntegration of semantic verication into Java compilersКлепининА. В.KlepininA. V.alklepin@mail.utnet.ruМелентьевА. А.MelentyevA. A.amelentev@gmail.comУральский Государственный Университет им.А.М.ГорькогоRussian Federation2010201220101747077Copyright © Клепинин А.В., Мелентьев А.А., 20102010Клепинин А.В., Мелентьев А.А.Klepinin A.V., Melentyev A.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1053

Рассматривается способ статического семантического анализа исходных кодов программы на стадии ее компиляции с целью повышения качества исходного кода. В качестве способа реализации такого семантического анализа предлагается унифицированная интеграция в компиляторы языка Java для получения полного доступа к синтаксическому дереву (AST) компилируемых программ после этапа семантического анализа. Для обеспечения унификации реализованы общие интерфейсы для работы с синтаксическим деревом и адаптеры к реализациям синтаксических деревьев в компиляторах Sun/Oracle javac и Eclipse Compiler for Java (ecj). Выбранный способ обеспечил прозрачную интеграцию со средами разработки Eclipse и Netbeans без необходимости установки каких-либо расширений данных сред. Разработанный метод демонстрируется на некоторых примерах верификации программ.

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.

верификация программабстрактное синтаксическое деревоJavaкомпиляторJSR269javacecjEclipse IDENetbeans IDEprogram veri cationASTJavacompilerJSR269javacecjEclipse IDENetbeans IDEReferencesPMD, java source code verificator. [Электрон. ресурс]. Режим доступа: http://pmd.sourceforge.net/.PMD, java source code verificator. [Электрон. ресурс]. Режим доступа: http://pmd.sourceforge.net/.Findbugs, java byte code verificator. [Электрон. ресурс]. Режим доступа: http://findbugs.sourceforge.net/.Findbugs, java byte code verificator. [Электрон. ресурс]. Режим доступа: http://findbugs.sourceforge.net/.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.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.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.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.JSR269: Pluggable Annotation Processing API. [Электрон. ресурс]. Режим доступа: http://jcp.org/en/jsr/detail?id=269.JSR269: Pluggable Annotation Processing API. [Электрон. ресурс]. Режим доступа: http://jcp.org/en/jsr/detail?id=269.Project lombok. [Электрон. ресурс]. Режим доступа: http://projectlombok.org/.Project lombok. [Электрон. ресурс]. Режим доступа: http://projectlombok.org/.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.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.Universal AST project for Checker Framework. [Электрон. ресурс]. Режим доступа: http://code.google.com/p/checker-framework/wiki/Ideas#Universal_AST.Universal AST project for Checker Framework. [Электрон. ресурс]. Режим доступа: http://code.google.com/p/checker-framework/wiki/Ideas#Universal_AST.Java Unified Abstract Syntax Tree project. [Электрон. ресурс]. Режим доступа: http://bitbucket.org/amelentev/juast/.Java Unified Abstract Syntax Tree project. [Электрон. ресурс]. Режим доступа: http://bitbucket.org/amelentev/juast/.java.util.ServiceLoader. [Электрон. ресурс]. Режим доступа: http://java.sun.com/javase/6/docs/api/java/util/ServiceLoader.html.java.util.ServiceLoader. [Электрон. ресурс]. Режим доступа: http://java.sun.com/javase/6/docs/api/java/util/ServiceLoader.html.

The authors declare that there are no conflicts of interest present.