Языки высокого уровня являются основным

Языки высокого уровня являются основным средством разработки программных систем. Спецификация языка высокого уровня задаёт класс текстов, принадлежащих этому языку, и определяет семантику исполнения программ, написанных на этом языке. Задача перевода текстов с языка высокого уровня в представление, выполнимое на вычислительной системе, решается комплексами программ, которые по традиции называют компиляторами. Ошибки в компиляторах приводят к тому, что выполнение результирующих исполнимых модулей отличается от поведения, определяемого спецификацией языка. Дефекты исполнимых модулей, вызванные ошибками в компиляторе, очень сложно выявлять и исправлять, и в целом корректность исполнимых модулей, построенных некорректным компилятором, вызывает сомнения. Корректность компилятора является необходимым требованием корректной и надёжной работы программного обеспечения, разработанного на соответствующем языке высокого уровня. Тем самым, задачу верификации компилятора можно считать одним из важнейших средств обеспечения надёжности программного обеспечения. Основной источник трудностей при верификации компилятора заключается в том, что компилятор принимает на вход данные со сложной структурой, большим количеством внутренних связей и обладающие очень сложной семантикой времени исполнения. Для снижения сложности задачи верификации компилятора мы предлагаем декомпозировать её на отдельные подзадачи, которые в совокупности покрывают всю функциональность компилятора . Функциональность, типичную для большинства компиляторов, можно условно декомпозировать на следующие задачи:

Анализ синтаксической корректности исходного теста программы.
Анализ выполнения контекстных условий в исходном тексте .
Оптимизация внутреннего представления и генерация выходных данных.

Результатом работы компилятора является объектный модуль на машинном языке или модуль на исполнимом промежуточном языке, таком как байт-код Java и Python или Intermediate Language платформы .NET. Для большинства компиляторов языков программирования, используемых на практике, генерируемый код исполняется в специализированном окружении, которое обобщённо называется run time support.
В рамках данной статьи мы будем пользоваться термином «подсистема поддержки исполнения». Подсистема поддержки исполнения тесно связана с компилятором. Например, каждый компилятор Си и Си++ поставляется со своим набором стандартных библиотек, причём библиотеки одного компилятора нельзя использовать для построения исполнимых файлов другим компилятором. Даже в тех случаях, когда промежуточный язык и стандартные библиотеки стандартизированы, существуют тесные зависимости между компилятором и средой исполнения. Например, для исполнения байт-кода Java в виртуальной машине Java компании IBM лучше всего для компиляции использовать компилятор Java именно этой фирмы; аналогично для исполнения байт-кода в виртуальной машине компании Sun следует компилировать исходные тексты компилятором Java, разработанным в Sun. В настоящей работе представлен подход к верификации компиляторов, основанный на технологии автоматизированного тестирования UniTESK[]. Методы, составляющие представленный подход, построены по единому шаблону формализации требований [].

Содержание раздела