Верификация подсистемы поддержки исполнения (runtime support)
Рассмотрим несколько примеров подсистем поддержки исполнения. Для низкоуровневых языков, таких как Си и Си++, поддержка исполнения ограничивается тем, что в состав поставки компилятора включаются стандартные библиотеки этих языков.
Компилятор Java переводит исходный текст на языке Java в байт-код. Система поддержки времени исполнения включает в себя виртуальную машину Java, стандартную библиотеку классов Java SDK, в том числе, внутренние классы, обеспечивающие доступ к ресурсам операционной системы (ввод-вывод, потоки, и т.д.), набор средств взаимодействия Java-среды с окружением через JNI.
Другой пример относится к языку спецификации тестов TTCN3. Все известные в настоящее компиляторы TTCN3 построены как трансляторы - исходный текст на языке TTCN3 преобразуется в набор файлов на целевом языке (Си или Java), которые затем компилируются соответствующими компиляторами. Система поддержки времени выполнения представляет собой набор библиотек на целевом языке (Си или Java), которые реализуют встроенные возможности языка (таймеры, порты обмена сообщениями, стандартные функции и т.п.), предоставляют интерфейсы расширения (TCI и TRI) как сгенерированному коду, так и окружению, и, в зависимости от поставщика, различные дополнительные возможности.
Задачу верификации подсистемы поддержки исполнения можно разделить на следующие подзадачи:
- Верификация программного интерфейса, предоставляемого сгенерированному коду.
- Верификация встроенных возможностей языка и динамической семантики операций, предоставляемых подсистемой поддержки исполнения.
- Верификация интерфейсов взаимодействия с окружением. Эта задача может быть разделена на две подзадачи:
- Верификация интерфейсов, предоставляемых окружению для взаимодействия с исполняемой системой.
- Верификация интерфейса, который предоставляет подсистема поддержки исполнения в исходном языке.
Рассмотрим эти задачи на примере транслятора TTCN3, который преобразует исходный текст TTCN3 в набор файлов на языке Си. В этом случае задачи верификации можно сформулировать следующим образом:
- Верифицировать библиотеки непосредственно через предоставляемый ими интерфейс Си/Си++.
- Верификация встроенных возможностей языка заключается в том, чтобы проверить выполнение требований динамической семантики TTCN3 в той части, которая реализована в подсистеме поддержки исполнения - проверка требований к передаче сообщений через порты обмена сообщениями, обработке событий в инструкциях выбора alt, запуску и остановке компонентов и т.д.
- Верификация интерфейсов расширения заключается в проверке выполнения требований к стандартным интерфейсам расширения:
- Обращения к «скомпилированному тестовому набору» (Compiled Test Suite) извне через стандартные интерфейсы TCI и TRI, представленные в виде набора функциональных вызовов в программе на Си.
- Обращения к окружению скомпилированного тестового набора, представленные инструкциями и выражениями в исходных текстах на TTCN3, через стандартные интерфейсы TTCN3.
Аналогичные задачи можно сформулировать и для подсистем поддержки времени исполнения языка Java.
- Верификация библиотеки поддержки исполнения. Необходимо учитывать, что почти все сервисы, предоставляемые поддержкой времени исполнения, представлены как классы Java, поэтому в данном случае верификация представляет собой тестирование Java-классов.
- Верификация встроенных возможностей языка (например, синхронизации доступа) и динамической семантики (например, создания и уничтожения объектов).
- Верификация интерфейсов расширения:
- Обращения из Java-кода к ресурсам операционной системы через специализированные классы (потоки ввода-вывода, потоки исполнения Thread, класс System и т.д.), обращения из Java к внешним библиотекам, разработанным на других языках (JNI).
- Верификация программного интерфейса виртуальной машины Java и доступа к объектам Java через JNI из программ на Си.
