Близкие работы
Формальные методы применяются для построения компиляторов и теоретического доказательства корректности их поведения. Проект Verifix[] содержит теоретические разработки схем построения надежных компиляторов, основанных на применении серии промежуточных языков. Кроме того, имеются различные попытки реализации надежных компиляторов с использованием логических исчислений [,,]. Это также чисто теоретические работы. Обычно здесь предлагается простой модельный компилятор, для него строится логическое исчисление и демонстрируется метод доказательства корректности предложенного компилятора.
В работе [], предложены идеи построения спецификации оптимизирующих трансформаций с помощью системы перерисовки графа (Graph Rewrite Systems). Автор утверждает, что данная технология спецификации применима ко многим алгоритмам оптимизации и анализа программ. Такой подход к специфицированию трансформаций, несомненно, является очень интересным и может быть использован для построения оракулов. Однако практическое использование систем перерисовки графов требует большой технической поддержки, создание которой является отдельной сложной задачей.
Существуют также подходы к тестированию компиляторов, не использующие формальные методы. В работах [,,] содержатся идеи реализации оракула, проверяющего сохранение семантики программы во время трансформаций, при отсутствии каких-либо спецификаций выполняемых оптимизаций. Следует заметить, что общим изъяном этих подходов является отсутствие способа выбора входных тестовых данных. Кроме того, подход, изложенный в [] требует вмешательства в работу компилятора, что является неприемлемым при тестировании промышленных коммерческих продуктов.
Работа [] описывает основанную на идеях моделирования методологию автоматического построения тестов для парсеров формальных языков. В качестве описания модели в работе используется BNF-грамматика входного языка. В работе [] содержится методика ручного создания тестов для семантического анализатора программ по описанию модели языка.
В работе [] описан подход к автоматизации тестирования семантического анализа и кодогенерации. Спецификации для векторных и многопроцессорных выражений языка mpC были разработаны на языке XASM. Спецификации использовались для фильтрации программ, генерируемых относительно несложным итератором, и для получения эталонных результатов. Кроме того на их основе генерировались критерии тестового покрытия и инструменты его оценки.
Итак, тестирование компиляторов является очень перспективным направлением, в этой области имеется много интересных исследований. Однако, до сих пор не предложено никакого решения, подходящего для широкого использования в промышленных процессах тестирования оптимизирующих компиляторов.
