Расширенная статическая проверка Java: ESC/Java и OpenJML
ESC/Java
ESC/Java – инструмент статического анализа Java, выявляющий ошибки компиляции. Проверка корректности кода, границ массивов и условий с помощью теоремного решателя.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Введение
ESC/Java (и позднее ESC/Java2), "Extended Static Checker for Java" – это инструмент программирования, предназначенный для обнаружения типичных ошибок времени выполнения в программах на Java на этапе компиляции. Базовый подход, используемый в ESC/Java, называется расширенной статической проверкой, которая объединяет ряд методов для статической проверки корректности различных ограничений программы. Например, проверка того, что целочисленная переменная больше нуля или находится в пределах границ массива. Эта техника была впервые реализована в ESC/Java (и его предшественнике, ESC/Modula 3) и может рассматриваться как расширенная форма проверки типов. Расширенная статическая проверка обычно предполагает использование автоматического решателя теорем, и в ESC/Java использовался решатель теорем Simplify. ESC/Java не является ни корректным, ни полным. Это было сделано намеренно, чтобы уменьшить количество ошибок и/или предупреждений, выдаваемых программисту, и сделать инструмент более практичным. Однако это означает, что, во-первых, существуют программы, которые ESC/Java ошибочно считает некорректными (так называемые ложные срабатывания), а во-вторых, существуют некорректные программы, которые он считает корректными (так называемые ложные пропуски). Примеры последней категории включают ошибки, возникающие в результате модульной арифметики и/или многопоточности. ESC/Java был первоначально разработан в Исследовательском центре Compaq Systems Research Center (SRC). SRC начал проект в 1997 году после завершения работы над их оригинальным расширенным статическим контроллером ESC/Modula 3 в 1996 году. В 2002 году SRC опубликовал исходный код ESC/Java и связанных инструментов. Современные версии ESC/Java основаны на Языке моделирования Java (JML). Пользователи могут контролировать объем и виды проверки, добавляя в свои программы аннотации в виде специально отформатированных комментариев или прагм. Группа безопасности систем Университета Неймегена выпустила альфа-версии ESC/Java2, расширенной версии ESC/Java, которая обрабатывает язык спецификаций JML, вплоть до 2004 года. С 2004 по 2009 год разработкой ESC/Java2 занималась исследовательская группа KindSoftware в Университетском колледже Дублина, которая в 2009 году переехала в IT-университет Копенгагена, а в 2012 году – в Технический университет Дании. За годы существования ESC/Java2 приобрел множество новых функций, включая возможность работы с несколькими решателями теорем и интеграцию с Eclipse. OpenJML, преемник ESC/Java2, доступен для Java 1.8. Исходный код доступен по адресу https://github. com/OpenJML
ESC/Java (and more recently ESC/Java2), the "Extended Static Checker for Java," is a programming tool that attempts to find common run time errors in Java programs at compile time. The underlying approach used in ESC/Java is referred to as extended static checking, which is a collective name referring to a range of techniques for statically checking the correctness of various program constraints. For example, that an integer variable is greater than zero, or lies between the bounds of an array. This technique was pioneered in ESC/Java (and its predecessor, ESC/Modula 3) and can be thought of as an extended form of type checking. Extended static checking usually involves the use of an automated theorem prover and, in ESC/Java, the Simplify theorem prover was used. ESC/Java is neither sound nor complete. This was intentional and aims to reduce the number of errors and/or warnings reported to the programmer, in order to make the tool more useful in practice. However, it does mean that: firstly, there are programs that ESC/Java will erroneously consider to be incorrect (known as false positives); secondly, there are incorrect programs it will consider to be correct (known as false negatives). Examples in the latter category include errors arising from modular arithmetic and/or multithreading. ESC/Java was originally developed at the Compaq Systems Research Center (SRC). SRC launched the project in 1997, after work on their original extended static checker, ESC/Modula 3, ended in 1996. In 2002, SRC released the source code for ESC/Java and related tools. Recent versions of ESC/Java are based around the Java Modeling Language (JML). Users can control the amount and kinds of checking by annotating their programs with specially formatted comments or pragmas. The University of Nijmegen's Security of Systems group released alpha versions of ESC/Java2, an extended version of ESC/Java that processes the JML specification language through 2004. From 2004 to 2009, ESC/Java2 development was managed by the KindSoftware Research Group at University College Dublin, which in 2009 moved to the IT University of Copenhagen, and in 2012 to the Technical University of Denmark. Over the years, ESC/Java2 has gained many new features including the ability to reason with multiple theorem provers and integration with Eclipse. OpenJML, the successor of ESC/Java2, is available for Java 1.8. The source is available at https://github. com/OpenJML