Информационная система "Конференции"

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

Красноярск, Академгородок, 3-5 ноября 2003 года

Тезисы докладов

Информационные технологии

Трансляция синтаксических конструкций языка C#-light в USL выражения как этап верификации C#-light программ

Запреев И.С.

Институт систем информатики СО РАН (Новосибирск,
Россия)

    Unified Semantic Language (USL) был создан в результате обобщения различных подходов к описанию формальных семантик языков программирования.
    Основными конструкциями языка USL являются имена и выражения.
    Язык C#-light является подмножеством языка C#, позволяющим писать последовательные программы. Он содержит все конструкции языка C# за исключением потоков, атрибутов, незащищенного кода, деструкторов, lock и resource операторов, а так же checked и unchecked блоков.
    Описание операционной семантики языка C#-light требует задания абстрактной машины, что в свою очередь влечет необходимость определения состояний абстрактной машины, а так же ее поведения. Каждое состояние задается в терминах языковой сущности и языкового объекта.
    Языковая сущность - это синтаксическая конструкция языка, например, переменная, оператор, описание класса и так далее. Языковая сущность задается типом и набором атрибутов. К примеру, сущность “описание класса” в языке C#-light имеет тип class-declaration и набор следующих атрибутов:
    attribute-sections, modifiers, name, inherited-class,
implemented-interfaces, members.
    Языковой объект является экземпляром языковой сущности, то есть конкретным описанием класса, переменной и так далее. Значения языковых объектов представляются в виде USL выражений вида:
    <[name-type, t], [a1, e1], …, [an, en]>
где t это тип соответствующей языковой сущности, a1, …, an имена ее атрибутов, а e1, …, en соответствующие значения этих атрибутов.
    Правила перевода синтаксических конструкций языка C#-light (языковых сущностей) в USL выражения задаются на основе синтаксиса языка C#, описанного в его спецификации.
    Пример трансляции синтаксической конструкции C#-light в USL выражение:
    описание локальной переменной
      int i = 0;
    транслируется в следующее USL выражение
    <[name-type,
      local-variable-declaration],
     [type,
      int],
     [declarators,
      [<[name-type,
         local-variable-declarator],
        [name,
         i],
        [initializer,
         0]>]]>],
    В рамках создаваемой системы верификации C#-light программ были разработаны:

Общий подход к трансляции C#-light программы в USL выражение;
Библиотека классов USL выражений;
Синтаксический анализатор USL выражений;
Прототип компоненты перевода C#-light программы в USL выражение на основе open source компилятора Mono фирмы Ximian.

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

Ваши комментарии
Обратная связь

[Головная страница]
[Конференции]