ПРОГРАММИРОВАНИЕ, 2012, No 4, с. 3-16
ТЕСТИРОВАНИЕ, ВЕРИФИКАЦИЯ И ВАЛИДАЦИЯ ПРОГРАММ
УДК 681.3.06
СТАТИЧЕСКАЯ ФОРМАЛЬНАЯ СЕМАНТИКА СТАНДАРТА
ЕСМА-335
© 2012 г. В.А. Васенин*, М.А. Кривчиков**,
*Научно-исследовательский институт механики МГУ имени М. В. Ломоносова
119192 Москва, Мичуринский просп., 1 **Механико-математический факультет МГУ, Москва 119991 Москва, Ленинские Горы мкр., 1 E-mail: vasenin@msu.ru, maxim.krivchikov@gmail.com Поступила в редакцию 31.10.2011
Одним из эффективных подходов к созданию доверенного программного обеспечения является построение формальной модели, отражающей его семантику и последующая верификация кода с использованием этой модели. В настоящей статье представлены результаты работы, целью которой являлось построение общей модели для описания статической формальной семантики программ, которые представлены в виде высокоуровневого промежуточного кода, соответствующего стандарту ECMA-335.
1. ВВЕДЕНИЕ
Важное значение в последние годы придается вопросам верификации программных средств автоматизированных систем управления объектами и процессами, имеющими высокий уровень практической значимости. К числу таких, в первую очередь, относятся объекты критически важных инфраструктур [1, 2], частичная или полная утрата функциональных свойств которых способна прямо повлиять на состояние национальной безопасности. Отмеченные обстоятельства указывают на необходимость поиска доказательно строгих методов и средств анализа программных средств автоматизированных систем управления такими объектами и процессами на предмет их соответствия заранее определенным требованиям и свойствам, специфицирующим их функциональные возможности, качество реализации функций и уровень защищенности от различных внешних воздействий.
Для того, чтобы некоторые свойства программного продукта (программы) или требования к нему выполнялись, необходимо доказать, что эти свойства (требования),
сохраняются при представлении его исходного кода на языке программирования и при компиляции. На настоящее время существуют сотни языков программирования, несколько десятков из которых активно используется. Построение формальной модели каждого из таких языков - достаточно трудоемкий и наукоемкий процесс. Однако зачастую он оправдан, так как позволяет эффективно контролировать код программы на всех этапах ее жизненного цикла. Вместе с тем, формальная модель определенного языка программирования позволяет анализировать код только тех программ, которые написаны на данном языке. Статический анализ машинного кода универсален, однако из-за низкого уровня абстракции и большой зависимости от аппаратного обеспечения он, как правило, не дает необходимых результатов. Существует компромиссный подход, когда производится статический анализ некоторого промежуточного кода, в который транслируется исходный код программы. Далее промежуточный код может быть выполнен с помощью интерпретатора, либо скомпилирован в машинный код.
В настоящей публикации представлена
разработанная авторами общая модель для описания статической формальной семантики программ, которые представлены в виде высокоуровневого промежуточного кода, соответствующего стандарту ЕСМА-335 [3]. Одной из главных целей работы, результаты которой представлены далее, являлось установление соответствия структуры модели статической формальной семантики этому стандарту.
2. ФОРМАЛЬНАЯ СЕМАНТИКА
Формальная семантика языка программирования представляет собой математическую модель, которая описывает работу различных конструкций языка. С помощью формальной семантики возможно решение целого ряда задач, а именно:
• доказательство различных свойств языка;
• формальная верификация компилятора языка [4];
• построение математической модели программы, написанной на этом языке, и ее последующая формальная верификация на основе этой модели.
Известны работы [5], в которых формальная семантика рассматривается в качестве исходной базы для автоматического построения компиляторов.
Кроме применения для решения различных прикладных задач, формальная семантика в сочетании с формальным синтаксисом дает строгую спецификацию языка программирования, на основе которой могут быть выявлены и устранены неоднозначности, которые, как правило, присутствуют в специикации этого языка, представленной на вербальном или других менее формализованных уровнях описания семантики.
Как уже отмечалось ранее, объектом, семантика которого требует формального описания, может быть не только язык программирования, но и любой программный продукт (средство, система, комплекс), реализующий некоторые функции. Однако формальное доказательство свойств и строгая верификация такого продукта в любом случае потребует
знания формальной семантики языка (или языков), на котором он написан. Принимая во внимание отмеченное обстоятельство, далее будем рассматривать понятие формальной семантики более широко, чем только применительно к языку.
Выделяют три основных подхода к построению формальной семантики, а именно -операционный, денотационный и аксиоматический [6].
Подход на основе операционной семантики описывает значение конструкций языка программирования с помощью непосредственного указания способа вычисления каждой конструкции в терминах абстрактного вычислителя. Один из главных недостатков операционной семантики состоит в том, что абстрактный вычислитель для нетривиальных языков, как правило, имеет сложную структуру. Это влечет за собой сложность доказательства свойств программ.
Подход с использованием аксиоматической семантики не определяет непосредственно значения, как некоторого заданного числа, промежуточного или конечного результата вычисления отдельных конструкций или программы в целом. Вместо этого задается определенный набор свойств отдельных ее конструкций. Свойства описываются как аксиомы и правила вывода некоторой формальной системы. Свойства программы строятся как выводы из аксиом и правил вывода данной системы.
Денотационная семантика описывает значение программы с помощью специальных объектов, называемых денотациями. В роли денотаций могут выступать числа, функции, или некоторые конструкции, такие как домены Д. Скотта. Денотационная семантика не определяет последовательность шагов, которые необходимы для вычисления выражений языка. С одной стороны, это является преимуществом, так как позволяет исследовать семантику программы как некоторый цельный объект, а не как последовательность шагов, что происходит в случае операционной семантики. С другой стороны, для императивных языков, в которых порядок выполнения действий имеет значение, это обстоятельство усложняет модель.
Три перечисленных подхода следует рассматривать как взаимно дополняющие. Например, распространенным на практике для описания семантики языка программирования на настоящее время является следующий подход. С целью абстракции от конкретной реализации языка, его семантика в целом задается с помощью денотационного подхода. Для верификации процесса компиляции может быть построена операционная семантика языка, в терминах которой проще описывается преобразование программы в машинный код. Доказательство полноты операционной семантики относительно денотационной позволяет обосновать сохранение свойств программы, полученных для высокоуровневого денотационного способа ее описания. С примерами реализации такого подхода на практике для модифицированного языка PCF и для нетипизированного А-исчисления можно ознакомиться в [7].
Формальную семантику языка программирования можно разделить на две составные части - статическую и динамическую. Статическая семантика дополняет описание синтаксиса языка, сужая класс допустимых программ с помощью введения областей видимости идентификаторов и правил типизации. Основным результатом построения статической семантики является окружение - объект, который описывает статическую структуру функций и типов данных программы. С помощью анализа окружений статической семантики могут быть выделены некоторые некорректно типизированные программы. Динамическая семантика описывает непосредственно значение конструкций языка в процессе выполнения программы.
3. СТАНДАРТ ECMA-335
Стандарт ECMA-335 (Common Language Infrastructure) [3] определяет систему типов, метаданные, виртуальную машину и систему команд для нее (Common Intermediate Language, далее - код CIL), а также задает ограничения для используемых библиотек. Все перечисленные положения в совокупности составляют инфраструктуру взаимодействия
произвольных языков программирования, удовлетворяющих стандарту Common Language Infrastructure (CLI). Они обеспечивают возможность выполнения удовлетворяющих этому стандарту программ на любой реализации стандарта, независимо от аппаратных и низкоуровневых системных особенностей платформы.
Существует несколько реализаций CLI, в частности: Microsoft .NET; Mono; Portable.NET; Sil-verlight. На настоящее время поддерживающие CLI компиляторы разработаны для достаточно большого количества языков. Примерами могут служить: С#; IronPython; несколько реализаций Lisp (L#, IronLisp, #S); реализация виртуальной машины Java IKVM.NET. На Wikipedia представлен неофициальный список компиляторов, поддерживающих CLI, в котором на момент написания данной работы их было более 50.
Программы, соответствующие стандарту ECMA-335, распространяются и разворачиваются в пакетах, называемых сборками. Согласно стандарту, сборка представляет собой набор файлов в совокупности с метаданными -структурой, которая описывает файлы, входящие в сборку, типы данных, определяемые данной сборкой и некоторый дополнительный набор информации. В сборку могут входить как файлы, содержащие код CIL, так и файлы ресурсов, на содержание которых не накладывается никаких ограничений. Файл, содержащий код CIL и/или метаданные, называют модулем. Сборка обязательно включает хотя бы один файл, в котором и содержатся определяющие сборку метаданные. Сборки идентифицируются по имени, версии, региональным параметрам и, опционально, по открытому ключу издателя. Стандарт не запрещает динамическую подгрузку сборки версии, отли
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.