автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Применение формальных методов для тестирования компиляторов

Институт Системного Программирования Российской Академии Наук

На правах рукописи

Посыпкин Михаил Анатольевич

ПРИМЕНЕНИЕ ФОРМАЛЬНЫХ МЕТОДОВ ДЛЯ ТЕСТИРОВАНИЯ КОМПИЛЯТОРОВ

Специальность 05.13.11 — Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

АВТОРЕФЕРАТ

диссертации на соискание учёной степени кандидата физико-математических наук

Москва - 2004

Работа выполнена в Институте системного программирования РАН

Научный руководитель: кандидат физико-математических наук,

Косачев Александр Сергеевич

Официальные оппоненты: доктор физико-математических наук,

профессор

Серебряков Владимир Сергеевич;

кандидат физико-математических наук, Эйсымонт Леонид Константинович.

Ведущая организация: Институт прикладной математики

им. М.В. Келдыша Российской академии наук

Защита состоится 2004 года в часов на засе-

дании диссертационного совета Д.002.087.01 в Институте Системного Программирования РАН по адресу: 109004, Москва, ул. В. Коммунистическая, д. 25

С диссертацией можно ознакомиться в библиотеке Института Системного Программирования РАН.

Автореферат разослан

Учёный секретарь

диссертационного совета

кандидат физико-математических наук

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность темы

Языки высокого уровня давно стали основным средством разработки программного обеспечения. Это явилось причиной широкого распространения программ, обеспечивающих процесс такой разработки и, в частности, компиляторов.

Компиляторы решают задачу перевода языка высокого уровня в представление, которое может быть выполнено ЭВМ. Ошибки в компиляторах приводят к тому, что программы на исходном языке транс -лируются в исполняемые модули, поведение которых отличается от поведения, определяемого семантикой исходной программы. Такого рода ошибки очень сложно выявлять и исправлять, их наличие ставит под сомнение качество компонент для генерации которых использовался компилятор. Можно с уверенностью утверждать, что корректность работы компилятора с языка программирования является необходимым условием надежной работы любого программного обеспечиния, реализованного с его помощью, а контроль правильности работы компиляторов -одной из важнейших мер по обеспечению надежности программного обеспечения.

Для компилятора, как и для любого другого вида программного обеспечения, одним из важнейших методов обеспечения надежности является тестирование. Традиционно, методы тестирования принято делить на две группы - методы белого" и "черного" ящика. В первом случае для создания тестов используется информация о реализации, исходный код тестируемого продукта. Во втором - единственным источником информации для создания тестов является описание функциональности, также называемое спецификацией.

Оба метода имеют достоинства и недостатки. Одним из недостатков метода черного ящика является необходимость в дополнительных усилиях по созданию спецификации продукта. Для случая компиляторов, этот недостаток не существенен, так как для языков программирования

РОС НАЦИОНАЛЬНАЯ

БИБЛИОТЕКА СП о»

У

как правило существует неформальное описание синтаксиса и семантики (стандарт языка) и формальное описание синтаксиса (грамматика). В некоторых случаях может присутствовать также и формальное (полное или частичное) описание семантики языка. Наличие таких спецификаций языка делает привлекательным использование методов черного ящика для тестирования компиляторов.

При тестировании по методу черного ящика обычно решаются следующие задачи:

• Генерация (написание) тестов.

• Вынесение вердикта о прохождении теста (тестовый оракул).

• Оценка качества тестов (критерий покрытия).

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

Анализ результатов научных исследований, посвященных тестированию компиляторов, позволяет сделать следующие выводы о существующих решениях для перечисленных задач и степени их автоматизации:

• Для синтаксиса языка разработан ряд критериев покрытия для которых решен вопрос достижимости, и разработаны алгоритмы, позволяющие автоматически генерировать тестовые наборы, удовлетворяющие этим критериям.

• Разработан ряд способов автоматического синтеза статически корректных программ по атрибутным грамматикам. Вопрос достижимости критериев покрытия, предложенных для атрибутных грамматик, не решен. Не разработаны критерии покрытия для тестов, нарушающих статическую семантику.

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

Цель и задачи работы

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

На различных этапах решения поставленной задачи применялись различные методы исследования. Для описания и обоснования корректности основных алгоритмов генерации тестов использовалось описание языка на основе индуктивно выводимых синтаксических категорий. Для формализации динамической семантики и доказательства ее свойств использовалась структурная операционная семантика (SOS). Для реализации интерпретатора динамической семантики использовался инструмент Gem-Мех, основанный на формализмах Montages и ASM описания операционной семантики программ. Также с использованием языков Perl и Shell были реализованы инструменты для измерения тестового покрытия для Montages-спецификаций.

Научная новизна

В диссертационной работе предложена новая методика генерации тестовых программ для проверки реализации динамической семантики в компиляторе. Существующие работы в этом направлении не предлагают целостного и общего подхода к генерации таких программ и либо ограничиваются простыми частными случаями, либо основываются на эвристиках. В диссертационной работе впервые сформулирован набор требований к программам для тестирования реализации динамической семантики и предложен алгоритм их автоматической генерации с ис-пользованиеми формального описания операционной семантики языка программирования или его подмножества.

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

В работе предложены новые алгоритмы генерации семантически корректных программ на основе индуктивного определения языка программирования .

Все алгоритмы, описанные в диссертационной работе, реализованы и прошли практическую апробацию.

Практическая значимость

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

Разработанные критерии покрытия дают возможность автоматиче-

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

С помощью реализованных в рамках работы над диссертацией инструментов для автоматизированной генерации тестов и измерения покрытия были получены тестовые наборы для подмножества языка Си, позволившие обнаружить две ошибки в интерпретаторе выражений отладчика Gnu Debugger (версия 3.0) и одну ошибку в промышленном компиляторе. Также эти инструменты были применены для полномасштабного тестирования компилятора с языка параллельного программирования mрС, в результате которого было выявлено большое число ошибок.

Апробация работы и публикации

По материалам диссертации опубликовано четыре печатные работы.

Основные положения работы докладывались на следующих конференциях и семинарах:

• на секции LDTA'2003 (Third Workshop on Language Descriptions, Tools and Applications) международной конференции ETAPS'03 (European Joint Conferences on Theory and Practice of Software), Warsaw, Poland, 2003 r.

• на международной конференции ASM'03 (Abstract State Machines), Taormina, Italy, 2003 r.

• на секции AS'02 (Action Semantics Workshop) международной конференции FME'02 (Formal Methods Europe), Kopenhagen, Denmark, 2002 r.

• на семинарах Института Системного Программирования РАН, 2002 г. и 2003 г.

Структура и объем диссертации

Диссертация состоит из введения, пяти основных глав, заключения, одного приложения и списка литературы. Общий объем диссертации составляет 153 страницы. Список литературы включает 62 наименования.

КРАТКОЕ СОДЕРЖАНИЕ РАБОТЫ

Во введении обосновываются цели и задачи данной работы, ее актуальность, научная новизна и практическая значимость. Приводится краткий обзор работы.

В первой главе описывается текущее состояние исследований, связанных с тестированием компиляторов, и формулируется основная задача диссертационной работы.

В первой части главы рассматриваются основные понятия теории компиляции, необходимые для дальнейшего изложения. Приводится традиционная схема разбиения на фазы транслятора с языка программирования.

Далее формулируются основные задачи, которые решаются в процессе тестирования. В разделах 2-6 этой главы производится анализ существующих подходов к решению этих задач для перечисленных фаз компиляции, который показывает, что наименее изученными являются критерии покрытия для программ и способы генерации для тестов, ориентированных на динамическую семантику языка, а также критерии покрытия для тестов, нарушающих статическую семантику.

На основании проведенного анализа формулируется основная задача диссертации, которая состоит в разработке и реализации методов автоматизированной генерации тестов для проверки реализации статической и динамической семантики в компиляторах. При решении поставленной задачи основное внимание предполагалось уделить нерешенным проблемам: определению критериев покрытия для тестов, нарушающих статическую семантику, критериев покрытия, ориентированных на ди-

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

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

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

В этой главе предлагаются способ описания таких подмножеств языка и алгоритмы автоматической генерации тестовых наборов по этому описанию, основанные на индуктивном определении языка. Индуктивное определение языка состоит из набора правил вывода для элементов различных синтаксических категорий - множеств фраз, соответствующих нетерминальным символам языка. При этом каждому нетерминальному символу соответствует в точности одна синтаксическая категория. Синтаксическая категория, соответствующая стартовому символу грамматики, совпадает со множеством фраз языка.

Предлагаемый алгоритм генерации тестов состоит в последовательном построении фраз из различных категорий, начиная с некоторого множества предопределенных фраз (содержимого предопределенных синтаксических категорий), например, набора идентификаторов и констант. Новые фразы генерируются с помощью применения правил вывода к ранее сгенерированным фразам.

Процесс генерации управляется описанием некоторого подмноже-

ства языка, состоящим из множества правил вывода и множества предопределенных категорий. Содержимое предопределенных категорий и правила вывода определяются тестировщиком и не меняются в процессе генерации тестов. Меняя набор правил вывода и предопределенных категорий, тестировщик может управлять структурой генерируемых тестовых программ. Например, если целью тестирования является проверка генерации кода или оптимизации для циклов, то содержимое всех других категорий (переменные, константы, простейшие выражения) может быть задано в виде перечисления. При этом полученный набор тестов будет содержать всевозможные комбинации различных видов циклов, что позволит максимально полно проверить корректность их реализации в генераторе кода или на фазе оптимизации.

В первом разделе главы приводится общее описание подхода, которое иллюстрируется на примере языка калькулятора.

Во втором разделе формально определяется понятие синтаксической категории и рассматривается индуктивный способ описания языка программирования. Далее описываются алгоритмы автоматической генерации фраз по набору правил вывода и предопределенных синтаксических категорий. Рассматриваются два основных алгоритма: Generaíe5?/níaa:Гesís и Сепегс^еЗ'етапйсзГез^.

Алгоритм генерирует по заданным

множествам правил вывода Р, предопределенных синтаксических категорий РЫ, их содержимых РМ и целому числу i множество программ из синтаксической категории для стартового символа, вывод которых состоит из не более чем % применений правил вывода.

Алгоритм предназначен для генерации се-

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

Алгоритм генерирует по задан-

ным множествам правил вывода Р, предопределенных синтаксических категорий PN, их содержимых РК и целому числу i множество семантически корректных программ из множества

Далее рассматриваются способы оптимизации алгоритма C?eneraíe5emafгfícs7'esí5 для двух распространенных случаев задания семантики. В первом случае предполагается, что помимо процедуры проверки семантической корректности программ существует также процедура, позволяющая установить, что фраза, принадлежащая синтаксической категории, отличной от категории стартового символа, не может быть частью семантически корректной программы. Для этого случая предлагается оптимизированная версия алгоритма генерации семантически корректных тестов, существенно сокращающая количество программ, для которых проверяется корректность семантики, и тем самым ускоряющая выполнение алгоритма.

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

Результаты практических экспериментов, приведенные в главе, показывают что предложенные оптимизации позволяют существенно (суммарно более чем в 10 раз) ускорить работу базового алгоритма генерации семантически корректных программ.

В конце раздела формулируется и доказывается теорема, показывающая возможность построения тестового набора, удовлетворяющего произвольному достижимому критерию покрытия, за конечное число шагов предлагаемым алгоритмом генерации семантически корректных тестов.

Теорема 1. Если критерий покрытия достижим для множества семантически корректных программ языка, определенного индуктивно с данным множеством продукционных правил Р и набором PN предопределенных синтаксических категорий, то существует такое

натуральное число I, что множество

Сепе^еБетаЫлсвТ^Б (Р, РИ, Ш, I)

удовлетворяет этому критерию покрытия.

Эта теорема может быть применена на практике следующим образом: тестировщик задает множество правил вывода и предопределенных категорий таким образом, чтобы критерий покрытия достигался для языка, индуктивно определенного с помощью этих множеств. После чего алгоритм GeneratesemanticsTests выполняется для этих множеств с максимально возможным (допустимым по ресурсам) параметром г. В процессе генерации тестов происходит отслеживание критерия покрытия и к тестовому набору добавляются только тесты, увеличивающие покрытие. Алгоритм останавливается в случае, когда полученное множество удовлетворяет критерию покрытия или выполнено i итераций.

В последнем разделе подводится итог и перечисляются результаты главы, которые состоят в следующем:

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

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

3. Доказана теорема, показывающая возможность построения тестового набора, удовлетворяющего произвольному достижимому критерию покрытия, за конечное число шагов предлагаемым алгоритмом генерации семантически корректных тестов.

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

Для тестирования реализации динамической семантики в компиляторе используются программы, которые могут быть откомпилированы тестируемым компилятором и выполнены для последующего сравнения наблюдаемого поведения с эталонным (определяемым семантикой программы) и вынесения вердикта о корректности работы кодогенератора на них.

Можно сформулировать ряд требований, предъявляемых к таким тестам:

1. В процессе выполнения теста не должны производится действия, поведение для которых не определяется в стандарте языка. Действия, для которых поведение не определено, иногда называют ошибками времени выполнения. Примерами такого рода действий могут быть деление на ноль или попытка обращения к памяти, находящейся за пределами адресного пространства процесса, выполняющего программу. Тесты, выполнение которых вызывает неопределенное поведение, очевидно не пригодны для тестирования, т.к. для таких тестов любой вариант наблюдаемого поведения будет правильным и вынесение вердикта о корректности теряет смысл. Программы, удовлетворяющие сформулированному условию, будем называть динамически корректными.

2. Наблюдаемое поведение теста не должно зависеть от неспецифи-цированных параметров семантики. Действительно, если выполнение теста зависит от таких параметров, то наблюдаемое поведение может варьироваться в зависимости от реализации, что делает затруднительным тестирование различных компиляторов с помощью одного набора тестов. Программы, удовлетворяющие этому

свойству, назовем переносимыми.

3. Тесты должны быть, детерминированы: наблюдаемое поведение теста должно однозначно определяться входными данными. Если этой свойство не выполнено, то реализация тестового оракула является нетривиальной задачей, т.к. необходимо выявить все источники неоднозначности поведения и перебрать все возможные варианты поведения программы.

Программы, удовлетворяющие всем трем условиям, называются строго конформными (термин заимствован из стандарта языка Си).

Способы автоматической генерации строго конформных и просто динамически корректных программ сложнее и изучены в гораздо меньшей степени, чем способы генерации синтаксически и статически корректных программ. Можно сказать, что работы, в которых затрагиваются вопросы автоматической генерации тестов для генератора кода, не предлагают целостного подхода к проверке того, что генерируемые программы обладают детерминированным поведением, выполняются без ошибок и не зависят от определяемых реализацией особенностей семантики.

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

В первом разделе данной главы приводится общая схема генератора тестовых программ и формулируются требования к семантике подмножества языка, позволяющие использовать ее для генерации строго конформных программ в этом языке: семантика, которую можно использо-

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

Второй раздел иллюстрирует применение предложенной в первом разделе методики на примере генерации тестов для языка Си. Для этого формально задается операционная семантика подмножества языка Си, для которой показывается выполнимость свойств, которым должна удовлетворять семантика, подходящая для генерации строго конформных программ.

Сначала последовательно строятся три вложенных подмножества языка Си: Сих С Сиг С CHSimPie.- Язык Си<атр1е достаточно сложен и включает в себя арифметические операции, операции адресной арифметики и преобразования типов. Для этих подмножеств определяется формальная семантика, для которой выполняются свойства сохранения типов и состояния памяти, которые формулируется в виде двух теорем.

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

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

Неформально, эти теоремы означают, что динамически корректная программа из не приводит к ошибочным ситуациям с точки зре-

ния семантики Си, т.к. отсутствие возможных источников ошибок - выхода за границы целого типа и использование в вычислениях некорректных адресов гарантируется свойством сохранения типов. Это означает, что любая динамически корректная программа из Си^р],, является динамически корректной Си программой. Также показывается выполне-

ние свойств детерминизма и независимости от неспецифицированных параметров динамической семантики для программ из Си^р^.

Апробация предлагаемого подхода к автоматической генерации тестов рассматривается в третьем разделе главы. Было сгенерировано два набора программ, направленных на тестирования двух новых возможностей языка Си, введенных последним стандартом: арифметики с комплексными числами и адресной арифметики для случая динамических массивов. Сгенерированные наборы строго конформных программ позволили найти ошибки в отладчике Gnu Debugger (GDB) и в промышленном компиляторе.

В третьей главе получены следующие результаты:

1. Предложена методика генерации тестовых программ для языка программирования, основанная на использовании формальных спецификаций динамической семантики языка. Сгенерированные таким образом программы без ошибок выполняются любой конформной реализацией языка, при этом результат их работы не зависит от неопределенных или определяемых реализацией параметров семантики и однозначно определяется входными данными.

2. Формально описан абстрактный синтаксис и семантика подмножества языка Си для которого доказаны теоремы сохранения типов и состояния памяти, с помощью которых обоснован тот факт, что любая корректная программа из этого подмножества является строго конформной. Для этого подмножества сгенерирован набор тестов.

Во второй и третьей главах были рассмотрены подходы к решению двух традиционных задач тестирования: задача генерации тестовых программ и задача построения тестового оракула. Четвертая глава диссертации посвящена решению третьей основной задачи тестирования: измерению тестового покрытия. Информация о покрытии необходима для оценки качества тестового набора и управления генерацией тестов.

В первом разделе главы приводится краткое описание формализма Montages. Каждой конструкции языка программирования соответствует отдельный элемент в спецификации, называемый монтажем. Этот элемент представляет собой диаграмму состояний с приписанными к ее элементам действиями, соответствующими правилам вычисления статической и динамической семантики. Для описания этих действий используется формализм Машин Абстрактных Состояний (ASM). С помощью инструмента Gem-Мех спецификация может быть откомпилирована в исполняемый файл, реализующий интерпретатор с описанного языка.

Выполнение динамической семантики программы определяется как последовательность переходов между различными состояниями, в каждом из которых выполняется набор ASM правил. В начале второго раздела главы определяются критерии покрытия для динамической семантики, основанные на комбинации критериев покрытия для автоматных и ASM-спецификаций. Приведем наиболее сильный из этих критериев: Определение 1. Последовательность {s/i{Ti),s^ï^)» • • • >stn(Tn)} называется выполнимым п-путем, если существует программа, выполнение динамической семантики для которой последовательно проходит по состояниям sti,..., stn и в состоянии st i происходит выполнение правил из для всех

Определение 2. (Критерий покрытия по п-путям) Тестовый набор удовлетворяет критерию покрытия по п-путям, если для любого выполнимого n-пути существует программа из набора, выполнение динамической семантики для которой последовательно проходит по состояниям sti,...,stn и в состоянии sti происходит выполнение правил из 7} для всех

Определение 3. (Сильный критерий покрытия по п-путям) Тестовый набор удовлетворяет сильному критерию покрытия по п-путям для множества монтажей если для любого т, такого что тестовый набор удовлетворяет критерию покрытия по m-путям.

Далее в разделе определяется критерий покрытия для семантических ограничений Montage-спецификаций. В большинстве случаев, се-

мантическое ограничение может быть сформулировано как одновременное выполнение нескольких условий Cj,...(Cn, называемых базовыми условиями для данного ограничения. В этом случае, соответствующее логическое выражение имеет следующий вид: Ci&... &СП. Определение 4. Критерий покрытия ограничений для ограничения Сук.... &С„ выполнен, если для любого к, 1 < к < тг, существует программа из тестового набора, такая что Ск = false иС, = true для всех г, 1 < г < 7г, г ф к.

Для этого критерия доказывается теорема, в соответствии с которой введенный критерий покрытия всегда достижим, если спецификация не содержит избыточных ограничений.

Теорема 2. Пусть Ci&...&Cn - семантическое ограничение в одном из монтажей спецификации семантики языка £. Тогда одно из следующих утверждений верно:

1. Язык £ содержит программу, такую что Сп = false и С\ =

2. C\h... &Cn_i&C„ = Ci&...fcC„_i для любой программы из £ (условие Сп избыточно).

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

В четвертой главе получены следующие результаты:

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

ошибки статической семантики. Доказана теорема о том, что введенный критерий покрытия всегда достижим, если спецификация не содержит избыточных ограничений.

2. Разработан критерий покрытия динамической семантики Montage-спецификаций, являющийся комбинацией критерия покрытия для ASM-спецификаций и спецификаций, основанных на конечных автоматах.

В пятой главе рассматривается опыт практического применения методики, предложенной в предыдущих главах.

Первый пример посвящен генерации тестов для языка Си. Основной задачей этого эксперимента была проверка теоретических результатов, изложенных в главе 3. Было сгенерировано два набора программ, направленных на тестирования двух новых возможностей языка Си, введенных последним стандартом (С99): арифметики с комплексными числами и адресной арифметики для случая динамических массивов. С помощью этих наборов удалось выявить 2 ошибки в текущей реализации отладчика Gnu Debugger (GDB): в первом случае неверно вычислялось значение разности между указателями на соседние элементы двумерного динамического массива, а во втором отладчик зависал при вычислении разности двух указателей на один и тот же динамический массив. Также была обнаружена ошибка в реализации адресной арифметики в промышленном компиляторе.

Второй пример - это применение предложенной методики для тестирования генератора кода в компиляторе с языка программирования mрС. Эта работа была выполнена в рамках промышленного проекта по созданию интегрированной среды разработки mpC-приложений гарС Workshop. В результате этой работы удалось существенно повысить надежность компилятора, что подтверждает высокую практическую ценность предлагаемой технологии генерации тестов и целесообразность ее применения в процессе промышленной разработки компилятора.

В первом разделе главы рассматривается общая структура генератора тестов. Во втором и третьем разделах описывается опыт генерации

тестовых наборов и тестирования компиляторов для языков Си и трС соответственно.

Результаты пятой главы состоят в следующем:.

1. Реализован интерпретатор динамической и статической семантики для строго конформного подмножества Си ¡impie языка Си, описанного в третьей главе, и для подмножества языка трС и построен интерпретатор для этого подмножества языка с помощью инструмента Gem-Mex.

2. Реализованы компоненты для генерации тестов и измерения покрытия по формальным спецификациям языка, заданным с помощью формализма Montages. С их помощью сгенерированы тестовые наборы для языков Си и трС. На полученных тестовых наборах были выявлены ошибки в компиляторах с этих языков.

В результате работы над спецификацией семантики языка трС были устранены противоречия и неточности в описании языка, в результате чего была создано новое описание семантики параллельных и векторных выражений трС, приведенное в приложении к диссертации.

ОСНОВНЫЕ РЕЗУЛЬТАТЫ РАБОТЫ

Основные новые научные результаты, полученные в диссертационной работе и выносимые на защиту, состоят в следующем:

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

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

3. Для определения качества набора тестов для компилятора разработан ряд критериев покрытия, основанных на формальных спецификациях языка программирования. Проведены эксперименты, доказывающие их практическую ценность. Реализованы инструменты, предназначенные для измерения покрытия в соответствии с этими критериями.

4. Реализованы генераторы тестовых программ, основанные на разработанных методиках. Для них написаны формальные спецификации подмножеств языков Си и mрС. На сгенерированных тестовых наборах удалось выявить ошибки в тестируемых программных системах, что подтверждает практическую ценность предложенной методики.

По теме диссертации опубликованы следующие работы:

[1] М.А. Посыпкин. Применение формальных методов для тестирования компиляторов. Препринт ИСП РАН, 12 стр., 2004.

[2] A. Kalinov, A. Kossatchev, A. Petrenko, M. Posypkin, V. Shishkov. Coverage-driven automated compiler test suite generation. In Proceedings of LDTA'2003, volume 82 of ENTCS. Elsevier, 2003.

[3] A. Kalinov, A. Kossatchev, A. Petrenko, M. Posypkin, V. Shishkov. Using ASM Specifications for Compiler Testing. In Proceedings of ASM 2003, volume 2589 of LNCS, page 415. Springer-Verlag, 2003.

[4] A. Kalinov, A. Kossatchev, M. Posypkin, V. Shishkov. Using ASM specification for automatic test suite generation for mpC parallel programming language compiler. In Proceedings of the Fourth International Workshop on Action Semantics, AS 2002, pages 96-106, 2002.

р-втвв"

Напечатано с готоаого орнгшвл-нахета

Издатепегао ООО "МАКС Пресс" Лппя ВД N 00510 от 01.12.99 г. Подлвсаш к петля 24.032004 г. Формат <0x90 1/16. Усжлеч-л. 1,3. Тарах «О эю. Заказ 143. Тел. 939-3890,939-3891,928-1042. Телефакс 939-3891. 119992, ГСП-2, Мосгаа, Ленжнспю горы, МГУ ш. МЗ. Ломоносов», 2-й учебный корпус, 6271-

Введение

1 Обзор методов тестирования компиляторов. Постановка задачи.

1.1 Основные понятия теории компиляции

1.2 Тестирование синтаксического анализатора.

1.3 Тестирования фазы анализа статической семантики.

1.4 Тестирование оптимизирующих преобразований в компиляторе

1.5 Тесты для проверки динамической семантики

1.6 Тестовые оракулы для фаз оптимизирующих преобразований и генерации кода.

1.7 Постановка задачи.

2 Базовые алгоритмы генерации тестовых программ для языка программирования

2.1 Описание подхода.

2.2 Алгоритмы генерации тестов.

2.3 Результаты главы

3 Генерация тестов для проверки реализации динамической семантики

3.1 Генерация строго конформных программ.

3.2 Синтаксис и семантика языка CHSimpie.

3.2.1 ЯзыкСи!.

3.2.2 Язык Сиг: Chi + указатели.

3.2.3 Язык CHSimpie = Си2 + адресная арифметика, массивы и преобразования типов.

3.3 Практическая апробация методики.

3.4 Основные результаты главы.

4 Критерии покрытия спецификаций семантики языка программирования

4.1 Система "Montages" описания семантики языков программирования

4.1.1 Формализм ASM.

4.1.2 Монтажи как средство описания семантики языков программирования.

4.2 Критерии покрытия Montage-спецификаций

4.2.1 Покрытие ASM-спецификаций.

4.2.2 Комбинированный критерий покрытия

4.2.3 Критерий покрытия для семантических ограничений

4.3 Основные результаты главы.

5 Опыт практического применения предложенной методики генерации тестов

5.1 Прототипная реализация генератора тестов и системы прогона тестов.

5.2 Набор тестов для проверки реализации динамической семантики расширений, введенных стандартом Си 99 . 101 5.3 Тестирование компилятора с языка программирования шрС

5.3.1 Векторные и параллельные возможности языка трС

5.3.2 Использование формализма Montages для определения семантики выражений трС.

5.3.3 Результаты тестирования.

5.3.4 Набор негативных тестов.

5.4 Основные результаты главы.

Общая характеристика работы

Языки высокого уровня давно стали основным средством разработки программного обеспечения. Это явилось причиной широкого распространения программ, обеспечивающих процесс такой разработки и, в частности, компиляторов.

Компиляторы решают задачу перевода языка высокого уровня в представление, которое может быть выполнено ЭВМ. Ошибки в компиляторах приводят к тому, что программы на исходном языке транслируются в исполняемые модули, поведение которых отличается от поведения, определяемого семантикой исходной программы. Такого рода ошибки очень сложно выявлять и исправлять, их наличие ставит под сомнение качество компонент для генерации которых использовался компилятор. Можно с уверенностью утверждать, что корректность работы компилятора с языка программирования является необходимым условием надежной работы любого программного обеспечения, реализованного с его помощью, а контроль правильности работы компиляторов - одной из важнейших мер по обеспечению надежности программного обеспечения.

Для компилятора, как и для любого другого вида программного обеспечения, одним из важнейших методов обеспечения надежности является тестирование. Процесс тестирования включает в себя три основные задачи

• Генерация (написание) тестов.

• Вынесение вердикта о прохождении теста (тестовый оракул).

• Оценка качества тестов (критерий покрытия).

Для решения этих задач применяются различные методы, которые можно разделить на две группы - методы "черного" и "белого" ящика. В первом случае, единственным источником информации для создания тестов является описание функциональности тестируемого продукта, также называемое спецификацией. Во втором, для создания тестов также используется информация о реализации, йсходный код тестируемого продукта.

В случае компиляторов, метод черного ящика состоит в получении тестовых наборов по описанию синтаксиса и семантики языка. Такие тестовые наборы предназначены для проверки того, что компилятор работает в соответствии с синтаксисом и семантикой поддерживаемого им языка. Метод белого ящика позволяет учитывать особенности конкретной реализации компилятора. Созданные этим методом тесты позволяют более тщательно проверять части компилятора, специфичные для тестируемой реализации компилятора.

Для тестирования компиляторов важны как методы "черного ящика", так и методы "белого ящика". Эти методы взаимно дополняют друг друга и могут использоваться совместно. Диссертационная работа посвящена тестированию компиляторов на основе формальных спецификаций синтаксиса и семантики языка программирования, т.е. методам "черного ящика".

Язык программирования определяется синтаксисом, статической семантикой и динамической семантикой. Спецификация каждого из этих аспектов языка может быть основой для создания тестов.

Синтаксис языка задается контекстно-свободной грамматикой. Цепочки терминальных символов, выводимые из стартового символа грамматики, называются синтаксически корректными программами. Множество синтаксически корректных программ является подмножеством множества всех цепочек терминальных символов. Они используются для тестирования того, что фаза синтаксического анализа распознает тест как корректный и генерирует внутреннее представление. Цепочки, не выводимые из стартового символа, используются для проверки способности компилятора распознавать синтаксическую ошибку.

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

Интерес с точки зрения тестирования представляют как программы, удовлетворяющие контекстным условиям, так и программы, нарушающие их. Программы, удовлетворяющие контекстным условиям, называются статически корректными. Статически корректные программы являются подмножеством множества синтаксически корректных программ. Они используются для тестирования того, что фаза статического анализа в компиляторе правильно распознает корректные программы. Синтаксически корректные программы, нарушающие контекстные условия, используются для проверки способности компилятора распознавать статические ошибки. Такие фразы в дальнейшем также будем называть негативными тестами.

Динамическая семантика определяет смысл выполнения статически корректных программ языка. Для тестирования ее реализации в компиляторе используются статически корректные программы, которые компилируются тестируемым компилятором, полученные в результате загрузочные модули выполняются, после чего их наблюдаемое поведение сравнивается с эталонным, определяемым динамической семантикой языка. Очевидно, что такое сравнение осмысленно только, если программы обладают однозначно определенным наблюдаемым поведением. Такие программы составляют подмножество во множестве всех статически корректных программ и далее в статье называются позитивными тестами.

Подробный обзор исследований, посвященных задаче тестирования на основе описания синтаксиса и семантики языка программирования, приводится в главе 1. На основании этого обзора можно сделать выводы о степени решенности основных задач тестирования, приведенные в таблице 1. Строки таблицы соответствуют задачам тестирования, а столбцы - составляющим описания языка программирования. Жирным шрифтом выделены нерешенные проблемы.

Синтаксис Статическая семантика Динамическая семантика

Генерация тестов Предложены алгоритмы генерации синтакс. корректных и некорректных тестов. Предложены алгоритмы генерации статически корректных тестов. Нет алгоритмов генерации тестов, содержащих ошибки. Решена для ряда частных случаев. Отсутствуют алгоритмы генерации программ с однозначным наблюдаемым поведением.

Тестовый оракул Проверяет способность компилятора воспринимать корректные тесты и обнаруживать ошибки в некорректных тестах. Подходы, основанные на сравнении наблюдаемого поведения.

Критерий покрытия Предложен ряд критериев для синтаксически корректных и некорректных тестов. Предложен ряд критериев для статически корректных тестов. Нет критериев для тестов, содержащих ошибку. Отсутствуют какие-либо критерии покрытия.

Таблица 1: Степень решенности

На основании проведенного анализа состояния проблемы были сформулированы цель и задачи работы. Целью работы являлась разработка и реализация методов автоматизированной генерации тестов проверки статической и динамической семантики в компиляторах. Для достижения этой цели предполагалось решить следующие основные задачи:

• Разработка и реализация алгоритмов генерации тестов, нарушающих контекстные условия (негативные тесты).

• Разработка и реализация алгоритмов генерации тестов, предназначенных для проверки реализации динамической семантики в компиляторе1, которые представляют собой статически корректные программы с однозначно определенным поведением (позитивные тесты).

• Разработка и реализация критериев покрытия для негативных и позитивных тестов.

На различных этапах решения поставленной задачи применялись различные методы исследования. Для формализации динамической семантики и доказательства ее свойств использовалась структурная операционная семантика (SOS) [53]. Для реализации контекстного анализатора и интерпретатора динамической семантики использовался инструмент Gem-Mex [9], основанный на формализмах Montages [44] и ASM [33] описания операционной семантики программ. Инструменты для генерации тестов и измерения тестового покрытия были реализованы с использованием языков Perl и Shell.

Научная новизна

В диссертационной работе предлагаются новые алгоритмы автоматизированной генерации тестов для проверки реализации статической (негативные тесты) и динамической семантики (позитивные тесты) в компиляторе.

В диссертационной работе впервые сформулирован набор требований к позитивным тестам на основе понятия однозначно определенного наблюдаемого поведения и предложен алгоритм их автоматической генерации с использованием формального описания операционной семантики языка программирования или его подмножества.

Также разработаны критерии новые критерии покрытия для негативных и позитивных тестов. Предложены алгоритмы генерации те

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

Все алгоритмы, описанные в диссертационной работе, реализованы и прошли практическую апробацию.

Практическая значимость

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

Разработанные критерии покрытия дают возможность автоматически измерять качество создаваемых тестовых наборов. Такая методика предпочтительнее "интуитивной" оценки качества тестов, производимой тестировщиком, т.к., во-первых, экономит его усилия, а во-вторых, является более точной.

С помощью реализованных в рамках работы над диссертацией инструментов для автоматизированной генерации тестов и измерения покрытия были получены тестовые наборы для подмножества языка Си, позволившие обнаружить две ошибки в интерпретаторе выражений отладчика Gnu Debugger (версия 3.0) и одну ошибку в промышленном компиляторе. Также эти инструменты были применены для полномасштабного тестирования компилятора с языка параллельного программирования трС, в результате которого было выявлено большое число ошибок.

Апробация работы и публикации

По материалам диссертации опубликовано пять печатных работ.

Основные положения работы докладывались на следующих конференциях и семинарах:

• на секции LDTA'2003 (Third Workshop on Language Descriptions, Tools and Applications) международной конференции ETAPS'03 (European Joint Conferences on Theory and Practice of Software), Warsaw, Poland, 2003 r.

• на международной конференции ASM'03 (Abstract State Machines), Taormina, Italy, 2003 r.

• на секции AS'02 (Action Semantics Workshop) международной конференции FME'02 (Formal Methods Europe), Kopenhagen, Denmark, 2002 r.

• на семинарах Института Системного Программирования РАН, 2002 г. и 2003 г.

Структура и объем диссертации

Диссертация состоит из введения, пяти основных глав, заключения, одного приложения и списка литературы. Общий объем диссертации составляет 156 страницы. Список литературы включает 62 наименования.

5.4 Основные результаты главы

В этой главе описаны следующие результаты практического применения предлагаемого в работе подхода к тестированию компиляторов:

1. Реализован интерпретатор динамической и статической семантики для подмножества Си simple языка Си, описанного в третьей главе, и для подмножества языка шрС и построен интерпретатор программ из этого подмножества с помощью инструмента Gem-Mex.

2. Реализованы компоненты для генерации тестов и измерения покрытия по формальным спецификациям языка, заданным с помощью формализма Montages. С их помощью сгенерированы тестовые наборы для языков Си и трС. На полученных тестовых наборах были выявлены ошибки в компиляторах с этих языков.

Результаты этой главы опубликованы в работах [20, 19].

1. М.А. Посыпкин. Применение формальных методов для тестирования компиляторов. Препринт ИСП РАН, 12 стр., 2004.

2. Зеленов С.А., Зеленова С.В., Косачев А.С., Петренко А.К. Применение модельного подхода для автоматического тестирования оптимизирующих компиляторов, http://www.citforrnn.ru.

3. Петренко А.К. Чацкина Т.А. Борисова М.В., Морозова Т.А. Тестирование компиляторов на основе формальной модели языка. Москва. Институт Прикладной Математики им. М.В. Келдыша Российской Академии Наук, 1992.

4. Зеленова С.В. Демаков А.В., Зеленов С.А. Тестирование парсеров текстов на формальных языках. Программные системы и инструменты, 2, 2001.

5. А.Я. Калинов, A.JI. Ластовецкий, И.Н. Ледовских, М.А. Посыпкин. Пересмотренное сообщение о языке программирования С]. Программирование, б, 2002.

6. G. С. С. Гайсарян, А. Л. Ластовецкий . Расширение ANSI С для векторных и суперскалярных компьютеров. Программирование, 1, 1995.

7. А.С. Косачев, Ф. Куттер, М.А. Посыпкин. Автоматическая генерация строго конформных тестов по формальной спецификации динамической семантики языка программирования. Программирование (в печати), 2004.

8. Automated syntax testing using JSynTest™. http: //software. qip. us/j syntest. htm.9. extensible Abstract State Machines, http: //www. xasm. org.10. mpC Workshop for Windows, http://mpcw.ispras.ru.

9. Б. Керниган, Д. Ритчи. Язык программирования Си. Невский Диалект, 2001.

10. Кауфман В.Ш. Стандартизация и контроль трансляторов. Различные аспекты системного программирования, pages 47-85, 1984.

11. Серебряков В.А. Лекции по конструированию компиляторов. Москва, 1993.

12. Ластовецикий A.JI. Язык и система параллельного программирования для разработки программ, эффективно переносимых в классе распределенных вычислительных систем. Диссертация на соискание ученой степени д.ф.м.н. Москва, 1997.

13. Сухомлин В.А. Система программирования тройного стандарта ЗС++. 4~я международная конференция "Развитие и применение открытых систем". Тезисы докладов., pages 37-47, 1997.

14. Баскаков Ю.В. Принципы построения тестовых комплектов для тестирования конформности компиляторов стандартам языков программирования. Теоретические и прикладные проблемы информационных технологий: Сборник трудов, под ред. проф. Сухомлина В.А., 2001.

15. A. Gargantini and Е. Riccobene. ASM-based testing: coverage criteria and automatic tests generation. In Formal Methods and Tools for Computer Science (Proceedings of Eurocast 2001), pages 262-265, February 2001.

16. A. Kalinov, A. Kossatchev, A. Petrenko, М. Posypkin, V. Shishkov. Coverage-driven automated compiler test suite generation. In Proceedings of LDTA'2003, volume 82 of ENTCS. Elsevier, 2003.

17. A. Kalinov, A. Kossatchev, A. Petrenko, M. Posypkin, V. Shishkov. Using ASM Specifications for Compiler Testing. In Abstract State Machines Advances in Theory and Applications 10th International Workshop, ASM 2003, volume 2589 of LNCS, 2003.

18. A.G. Duncan and J.S. Hutchison. Using attributed grammars to test design and implementations. In Proceedings of the 5th international conference on Software engineering , pages 170 178, 1981.

19. A.S. Boujarwah, K. Saleh, J. Al-Dallal. Testing syntax and semantics coverage of Java language compilers. Information and Software Technology, 41:15-28, 1999.

20. B. DiFranco. Specification of ISO SQL using Montages. Master's thesis, Universita di l'Aquila, 1997.

21. E. Borger and W. Schulte. Programmer friendly modular definition of the semantics of Java. In Formal Syntax and Semantics of Java, number 1523 in LNCS. Springer, 1998.

22. Brian A. Malloy and James F. Power. An interpretation of Purdom's algorithm for automatic generation of test cases. In Proceedings of1.IS'Ol, 2001.

23. C.J. Burgess, M. Saidi. The automatic generation of test cases for optimizing Fortran compilers. Information and Software Technology, 38:111-119, 1996.

24. E. Borger. Abstract state machines at the cusp of the millenium. In Y. Gurevich and P. Kutter and M. Odersky and L. Thiele, editor, Abstract State Machines: Theory and Applications, volume 1912 of LNCS, pages 1-8. Springer-Verlag, 2000.

25. E. Sirer and B. Bershad. Using production grammars in software testing. In Proceeding of Second Conference on Domain-Specific Languages, October 1999.

26. Ronald F. Guilmette. Personal communications.

27. Ronald F. Guilmette. TGGS: A flexible system for generating efficient test case generators, 1999.

28. Y. Gurevich. Evolving algebras, a tutorial introduction. Bulletin of EATCS, 43:264-284, 1991.

29. Y. Gurevich. Evolving algebras 1993: Lipari guide. In E. Borger, editor, Specification and Validation Methods, pages 9-36. Oxford University Press, 1995.

30. Y. Gurevich and J. Huggins. The semantics of the С programming language. In E. Borger, H. Kleine Btining, G. Jager, S. Martini, and M. M. Richter, editors, Computer Science Logic, volume 702 of LNCS, pages 274-309. Springer, 1993.

31. J. Harm. Automatic test program generation from formal language specifications. Rostocker Informatik-Berishte(1997), 20:33-56, 1997.

32. J. Harm and R. Lammel. Testing attribute grammars. In Proceedings of Third Workshop on Attribute Grammars and their Applications, pages 79-98, 2000.

33. J. Harm and R. Lammel. Two-dimensional approximation coverage. Informatica, 24(3), 2000.

34. Robert Harper. Programming languages: Theory and practice, http: //www-2. cs. emu. edu/~rwh/plbook/.

35. J. Huggins and W. Shen. The static and dynamic semantics of C. Technical Report CPSC-2000-4, Kettering University, Computer Science Program, 2000.

36. O & IEC. Programming Language C. WG14/N843 Committee Draft, 1998.

37. A. Kossatchev. Personal communications.

38. P. Kutter. The formal definition of Anlauff's extensible Abstract State Machines. TIK-Report 136, Swiss Federal Institute of Technology (ETH) Zurich, June 2002.

39. P. Kutter and A. Pierantonio. The formal specification of Oberon. Journal of Universal Computer Science, 3(5):443-503, 1997.

40. P. Kutter and A. Pierantonio. Montages: Specifications of realistic programming languages. Journal of Universal Computer Science, 3(5):416-442, 1997.

41. Ralf Lammel. Grammar testing. In Proc. of Fundamental Approaches to Software Engineering (FASE) 2001, volume 2029 of LNCS, pages 201-216. Springer-Verlag, 2001.

42. Alexey Lastovetsky. mpC a multi-paradigm programming language for massively parallel computers. ACM SIGPLAN Notices, 31 (5): 13 -20, 1996.

43. Maurer P.M. Generating test data with enhanced context-free grammars. IEEE Software, pages 50-55, 1990.

44. Maurer P.M. The design and implementation of a grammar-based data generator. Software Practice and Experience, 22(3):223—244, 1992.

45. George C. Necula, Scott McPeak, and Westley Weimer. CCured: type-safe retrofitting of legacy code. In Symposium on Principles of Programming Languages, pages 128-139, 2002.

46. M. Norrish. С formalised in HOL. Technical Report UCAM-CL-TR-453, University of Cambridge, Computer Laboratory.

47. Jukka Paaki. Attribute grammar paradigms. ACM Computing Surveys, 27(2):196-255, June 1995.

48. Nikolaos S. Papaspyrou. A Formal Semantics for the С Programming Language. PhD thesis, National Technical University of Athens, 1998.

49. Gordon Plotkin. A structural approach to operational semantics. Lecture Notes DAIMI FN-19, Dept. of Computer Science, Univ. of Aarhus, 1981.

50. Purdom P. A sentence generator for testing parsers. BIT, 2:336-375, April 1972.

51. P.W. Kutter. Montages Engineering of Computer Languages. PhD thesis, ETH Zurich, 2003.

52. John C. Reynolds. Theories of Programming Languages. Cambridge Universisty Press, 1998.

53. S. Zelenov, S. Zelenova, S. Kossatchev. Test generation for compilers and other text processors. Programming and Computer Software, (1), 2003.

54. H. ter Doest. Stochastic languages and stochastic grammars. In H. M. Groenbaum, H. W. Kleijn-Hesselink, and M. M. Lankhast, editors, GRONICS-94; Proceedings of the 1994 Groningen Student Conference on Computer Science, pages 51-59, 1994.

55. Jan Tretmans. Testing techniques, 2002.

56. W. McKeeman. Differential testing for software. Digital Technical Journal, 10(1):100 107, 1998.

57. C. Wallace. The semantics of the С++ programming language. In E. Borger, editor, Specification and Validation Methods, pages 131164. Oxford University Press, 1995.

58. C. Wallace. The semantics of the Java programming language: Preliminary version. Technical Report CSE-TR-355-97, EECS Dept., University of Michigan, December 1997.