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

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

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

В настоящее время большой интерес представляет верификация программ, написанных на таких широко распространенных объектно-ориентированных языках программирования, как C++, C#, Java. Существенной предпосылкой к тому, чтобы язык программирования подходил для верификации, служит компактная обозримая формальная семантика. Наиболее широко используемым подходом к формализации семантики является операционный подход. Однако процесс верификации в терминах операционной семантики, как правило, намного более трудоемкий по сравнению с верификацией в аксиоматической семантике, основанной на логике Хоара. Сложности разработки компактной обозримой аксиоматической семантики объектно-ориентированных языков программирования связаны с такими конструкциями, как перегрузка, динамическое связывание методов, обработка исключений, статическая инициализация классов.

В лаборатории теоретического программирования ИСИ СО РАН разработан новый трехуровневый подход к верификации программ на языке C#-light [1,2], который является выразительным последовательным подмножеством языка C# [3]. На первом этапе этого подхода язык C#-light транслируется в промежуточный язык C#-kernel, для того, чтобы элиминировать сложные для аксиоматической семантики конструкции и построить аксиоматическую семантику в более компактной форме. На втором этапе с помощью аксиоматической семантики C#-kernel генерируются ленивые условия корректности, которые могут содержать особые функциональные символы, уточняемые на третьем этапе.

В данном докладе представлен эффективный алгоритм трансляции языка C#-light в язык C#-kernel. Разработанный рекурсивный алгоритм трансляции представлен в виде набора правил трансляции, полученных на основе спецификации языка C#. Но большинство практически используемых конструкций языка C# допускают более простые правила перевода, поэтому были предложены оптимизации алгоритма для уменьшения объема выходного кода трансляции.

Для реализации данных правил были предложены внутренние представления для языков C#-light и C#-kernel и был программно реализован перевод программ во внутреннее представление. Использование полиморфизма позволило естестественным образом реализовать рекурсивные правила трансляции. В дальнейшем программу планируется использовать в разрабатываемой в лаборатории теоретического программирования системе верификации программ на C#-light.

1.          Непомнящий В.А., Ануреев И.С., Промский А.В. На пути к верификации C#-программ: трехуровневый подход – // Программирование. — 2006. — № 4. — С. 4-20.

2.          А.В. Промский Применение трехуровневого подхода к верификации программ на языке C#-light — Новосибирск, 2006. — 56 с. – (Препр. РАН Сиб. Отд-ние. ИСИ; N 139.)

3.          C# Language specification. Standard ECMA-334. (2001) http://www.ecma-international.org /.

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

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

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

© 1996-2000, Институт вычислительных технологий СО РАН, Новосибирск
© 1996-2000, Сибирское отделение Российской академии наук, Новосибирск
    Дата последней модификации: 06-Jul-2012 (11:48:14)