Препринты Института систем информатики СО РАН 2005 г.

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

Кроме того, работа фиксирует формальный синтаксис и операционную семантику модельного и учебного языка программирования Mini-NIL, который является прототипом языка виртуальной машины проекта F@BOOL@, на котором будут апробированы основные идеи системы F@BOOL@. Вынесенное в название работы указание "Часть I" подразумевает, что данная публикация является первой частью документации по проекту F@BOOL@ и что по мере проработки проекта будет опубликованы следующие части документации.

Работа поддержана грантом РФФИ № 05-07-90162.

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

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

В последние годы все большее распространение получают системы XML-баз данных. Наиболее перспективным языком запросов для них считается XQuery. Предлагаемая работа содержит обзор различных алгебр для XML-баз данных и дается оценка их применимости для поддержки XQuery.

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

Предложена XML-алгебра, поддерживающая язык запросов Xquery и представляющая собой ряд операторов конструирования выражений. Введение таких операторов вместо операций высокого уровня, использующих функции в качестве аргументов, позволило остаться в рамках структур первого порядка, примером которых являются многоосновные алгебры. Предложенный набор операторов существенно отличается по составу от набора операторов реляционной алгебры. Различие объясняется более сложной структурой XML-документа по сравнению с отношением. Фактически только выбор по предикату похож на соответствующую операцию реляционной алгебры, но в то же время имеется возможность выбора узлов дерева по их типу. Операция проекции заменена на путевое выражение и ряд навигационных функций, позволяющих выбирать различные части дерева документа. Операция соединения заменена на выражение раскрывающего соединения, позволяющего сформировать поток плоских кортежей на базе нескольких, возможно вложенных друг в друга частей дерева документа. В дополнение ко всему этому определен ряд конструирующих выражений, служащих для создания новых узлов дерева.

В работе рассматриваются SDL-спецификации распределенных систем с динамическим порождением и уничтожением экземпляров процессов. Для них предложен метод трансляции в модифицированные раскрашенные сети Петри - иерархические временные типизированные сети (ИВТ-сети), в которых используются предложенная Мерлином концепция интервального времени, приоритеты и содержатся специальные места, представляющие очереди фишек. Описана реализация метода трансляции и приведены оценки размера сети. Эта работа частично поддержана грантом РФФИ 03-07-90331.

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