УДК 004

Средство проверки состояния типов Java, поддерживающее наследование

Бобылев Денис Юрьевич – студент Саратовского национального исследовательского государственного университета им. Н. Г. Чернышевского.

Бобылева Анна Романовна – студентка Саратовского национального исследовательского государственного университета им. Н. Г. Чернышевского.

Аннотация: Обнаружение программных ошибок в программном обеспечении становится все более важным, и создание инструментов, помогающих разработчикам справиться с этой задачей, является важнейшей областью исследований, от которой зависит отрасль. Основываясь на наблюдении, что в объектно-ориентированном программировании (ООП) естественно определять объекты с отслеживанием состояния, где безопасное использование методов зависит от их внутреннего состояния, мы представляем Java Typestate Checker (JATYC), инструмент, который проверяет исходный код Java на соответствие состояниям типов.

Ключевые слова: Поведенческие типы, объектно-ориентированное программирование, проверка типов, состояния типов.

Ошибки программирования, такие как отмена ссылок на нулевые указатели [1], неправильное использование объектов (например, чтение из закрытого файла; закрытие сокета, время ожидания которого истекло) или забывание освободить ресурсы (например, не закрытие программы чтения файлов), приводят к сбоям в работе программ или ненужной трате памяти. Поэтому крайне важно разработать инструменты, которые помогают процессу разработки.

В языках программирования некоторые распространенные ошибки обнаруживаются благодаря системам типов, встроенным в компиляторы [3]. К сожалению, подмножество ошибок, обнаруживаемых во время компиляции в основных языках, все еще ограничено, и небезопасный код, который нарушает логику программы или может привести к сбою во время выполнения, все еще может быть скомпилирован (и запущен) в большинстве технологий программирования. Более подробно, наш подход позволяет избежать некоторых неучтенных ошибок и мотивирован следующими наблюдениями за практикой объектно-ориентированного программирования (ООП).

Большинство языков ООП, включая Java, статически не гарантируют, что методы вызываются в соответствии с указанным протоколом, например, вызов hasNext перед вызовом next в итераторе. Обычно протокол указывается в документации, но не применяется статически: это является источником многих ошибок, таких как доступ к переменной, которая не была инициализирована [2]. Хотя некоторые языковые фреймворки поддерживают усовершенствованный анализ, они требуют от опытных пользователей предоставления сложных спецификаций, например, в логике разделения. Крайне важно разрабатывать и корректировать общую стратегию компании при увеличении масштабов и продаж компании. Разработку и корректировку можно разделить на несколько этапов [2]:

Чтобы преодолеть это ограничение, такие инструменты, как Mungo, расширяют классы Java определениями typestate, которые определяют поведение экземпляров этих классов в терминах конечного автомата и проверяют, выполняются ли последовательности вызовов методов в порядке, предписанном в typestate.

Чтобы еще больше улучшить статический анализ и избежать исключений с нулевым указателем во время выполнения, можно использовать плагин Nullness Checker2 из Checker Framework, фреймворк, который поддерживает добавление систем типов в язык Java. Этот плагин расширяет систему типов Java, так что типы по умолчанию не могут быть обнулены, за исключением случаев, когда они объявлены с аннотацией Nullable. Некоторые современные языки, такие как Kotlin, также отличают ненулевые типы от типов, допускающих обнуление, таким образом избегая этих исключений. Тем не менее, такой подход может выдавать ложные срабатывания, даже если код безопасен, требуя от программиста дополнительной проверки того, что значение не равно null, следуя стилю, известному как защитное программирование, или ряду аннотаций.

В этой статье представлен Java Typestate Checker (JATYC), инструмент, который проверяет тип исходного кода Java, где объекты связаны с typestates. Классы Java аннотируются состояниями типов, которые определяют поведение экземпляров класса в терминах доступных методов и переходов состояний. С помощью JATYC хорошо типизированные программы обладают следующими свойствами: объекты используются в соответствии с их протоколами (typestates); протоколы достигают конечного состояния (если программа завершается); исключения с нулевым указателем не вызываются (в коде, который мы можем проверить). Чтобы обеспечить эти свойства, мы следуем обычному подходу типа сеанса и принудительно используем линейные объекты, связанные с протоколами.

JATYC - это новая реализация Mungo, которая поддерживает наследование, добавляет критические функции и исправляет известные проблемы, например, предполагает, что оператор continue переходит к началу тела цикла, таким образом пропуская выражение условия, что может привести к ложноотрицательным результатам. Он свободно распространяется6 и реализован в Kotlin в качестве плагина для Checker Framework, который активно поддерживается и хорошо интегрирован с языком Java и набором инструментов.

Основными вкладами в текущую версию Mungo являются:

- проверка отсутствия ошибок с нулевым указателем, что крайне важно для предотвращения “Ошибки на миллиард долларов”;

- проверка того, что протоколы объектов завершены, т.е. протоколы достигают конечного состояния, если программа завершается;

- поддержка подтипирования благодаря алгоритму синхронного подтипирования.

Чтобы обосновать необходимость JATYC, рассмотрим Java-класс BaseIterator, который позволяет выполнять итерацию по элементам массива. Далее показана реализация BaseIterator:

Предполагаемый протокол определяется неявно последовательностями вызовов методов, которые поддерживаются, и состояниями, достигаемыми с помощью этих вызовов. Чтобы использовать BaseIterator, необходимо вызвать метод hasNext перед вызовом next, чтобы убедиться, что есть оставшиеся элементы для извлечения. Если этот контракт не соблюдается, будет выдано исключение IndexOutOfBoundsException.

Хотя компилятор Java принимает код, который не соответствует этому контракту, в следующем разделе мы покажем, как обогатить классы Java аннотациями typestate, которые позволяют отклонять программы, содержащие такого рода поведенческие ошибки во время компиляции.

Что позволяет сделать JATYC, чтобы дополнить код спецификациями протокола и статически убедиться, что они соблюдаются и выполняются до завершения (если программа завершается). Кроме того, это гарантирует отсутствие ошибок с нулевым указателем и проверяет соответствие подтипов.

Все экземпляры класса Java, имеющие typestate, проверяются для обеспечения соблюдения требований.

Чтобы связать протокол с классом Java, необходимо включить аннотацию Typestate, содержащую (относительный) путь к файлу протокола. Расширение .protocol необязательно.

JATYC гарантирует, что экземпляры классов Java, связанные с typestate, подчиняются соответствующему протоколу и достигают конечного состояния, так что потенциально важные вызовы методов не забываются и ресурсы освобождаются.

Ошибки с нулевым указателем являются причиной большинства исключений во время выполнения в Java-программах [3]: поэтому способность обнаруживать эти ошибки во время компиляции имеет решающее значение. В этом направлении JATYC предлагает следующие гарантии:

Типы по умолчанию ненулевые (в отличие от системы типов по умолчанию в Java 9), вызовы методов и доступ к полям выполняются только для ненулевых типов, так как в средстве проверки nullable помечены аннотацией Nullable.

Ложные срабатывания, касающиеся доступа к инициализированным полям с возможностью обнуления (в классах, связанных с протоколами), исключаются, принимая во внимание, что методы вызываются только в определенном порядке. Например, представьте, что базовая коллекция итератора была предоставлена не в конструкторе, а вместо этого с помощью метода init, который инициализирует поле items (изначально помеченное как nullable). Если в протоколе указано, что init должен вызываться перед любым методом, инструмент может гарантировать, что последующие обращения к полям не приведут к ошибкам с нулевым указателем, без необходимости защитного программирования (т.е. проверки того, что items != null) или дополнительных аннотаций.

Чтобы добавить поддержку наследования, JATYC должен быть наделен алгоритмом подтипирования для обеспечения соответствия протокола подклассов протоколу суперклассов. Помимо реализации такого алгоритма, поддержка этих концепций также требует правильного обращения с переопределением методов и приведением к ним.

Алгоритм поддержки подтипирования протоколов основан на синхронном подтипировании для типов сеансов. Он строит графики из проверяемых протоколов, обходит их, запуская общие операции ввода/вывода, и помечает каждую встреченную пару состояний. Обратите внимание, что в нашей настройке операции ввода представлены вызовами методов, в то время как операции вывода - возвращаемыми ими значениями. Мы отмечаем пары состояний, если: (i) оба являются входными состояниями b подтип может выполнять набор операций ввода, больший или равный набору операций супертипа, оба являются выходными состояниями и супертип может выполнять набор операций вывода, больший или равный набору операций супертипа. равно одному из подтипов, оба состояния являются конечными состояниями. Алгоритм останавливается, когда либо все доступные пары помечены (подтипирование выполняется), либо пара состояний не удовлетворяет ни одному из вышеуказанных условий (подтипирование не выполняется).

Наследование позволяет повторно использовать методы из суперклассов, переопределять некоторые или добавлять новые.

Список литературы

1. Hoare. Null references: the billion dollar mistake.
2. Tan, C. Liu, Z. Li, X. Wang, Y. Zhou, C. Zhai. Bug characteristics in open source software/ Empir. Softw. Eng., 19 (2014), pp. 1665-1705
3. Cardelli. Type systems/ ACM Comput. Surv., 28 (1996), pp. 263-264