Публикации

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

Препринт 141

Р.Н. Арапбаев, В.А. Евстигнеев, Р.А. Осмонов

Сравнительный анализ тестов на зависимость по данным

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

Препринт 140

И.В. Дубрановский

На пути к верификации C#-программ: алгоритмы перевода из C#-light в C#-kernel

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

Препринт 139

А.В. Промский

Применение трехуровневого подхода к верификации программ на языке C#-light

В работе дается описание применения нового трехуровневого подхода к верификации программ на языке C#-light, который включает все основные последовательные конструкции языка C#. На первом этапе язык C#-light транслируется в промежуточный язык C#-kernel. На втором этапе, посредством аксиоматической семантики языка C#-kernel, порождаются "ленивые" условия корректности, включающие специальные функциональные символы, представляющие отложенное уточнение инвариантов меток и отложенные вызовы методов и делегатов. На третьем этапе эти условия уточняются с использованием алгоритмов операционной семантики. Цель работы - применить этот подход к верификации некоторых программ (изначально написанных на языке Java), вызвавших проблемы в системе ESC/Java. Также затронут вопрос упрощения условий корректности.

Препринт 138

Е.В. Бодин, Н.А. Калинина, Н.В. Шилов

Проект верифицирующего компилятора F@BOOL@ Часть II: Логические аннотации в языке Mini-NIL, их статическая семантика и семантика времени исполнения

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

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

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

Препринт 137

А.В. Быстров

Структурный анализ поведения непрерывно-временных сетей Петри

В данной работе выделяются подклассы непрерывно-временных сетей Петри, для которых разрабатываются эффективные структурные алгоритмы анализа таких поведенческих свойств, как живости, дивергентности, ограниченности, безопасности. Разработанные алгоритмы реализованы в рамках экспериментальной системы RT-MEC (Real Time Model and Equivalence Checker), поддерживающей спецификацию, анализ, валидацию и верификацию распределенных систем реального времени, представленных различными моделями временных сетей Петри.

Препринт 136

Н.С. Водопьянова, Н.В. Соседкина, Т.И. Тихонова, А.В. Лысцов

Лого-программирование для младших школьников

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

Препринт 135

Д. Пономарев

Проблема разложимости при формальном описании знаний

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

Препринт 134

Д. Пономарев

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

В данной работе мы рассматриваем декларативные базы знаний как (элементарные) теории в логике первого порядка. Мы исследуем операцию последовательной выборки данных, которая тесно свзяана с переформулированием запросов при информационном поиске и интеграции разнородных источников данных. Мы вводим формальное определение данной операции и определяем ее семанитку в терминах решеток, используя основную теорему метода анализа формальных понятий (Formal Concept Analysis).

Препринт 133

Н.С. Усоцкая

Исследование эквивалентностей на гибридно-временных структурах событий

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

Препринт 132

А.П. Стасенко, А.И. Синяков

Базовые средства языка Sisal 3.1

В работе описывается синтаксис и семантика новой версии потокового языка программирования Sisal 3.1, являющегося входным языком системы функционального программирования, разрабатываемой в рамках проекта ПРОГРЕСС. Язык Sisal 3.1 получен путем упрощения, улучшения, расширения и уточнения пользовательского описания языка Sisal 90, а также использования идей языка Sisal 3.0 и элементов объектно-ориентированного подхода. К элементам объектно-ориентированного подхода в языке Sisal 3.1 относятся пользовательские типы, переопределение операций и перегрузка функций.