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

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

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

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

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

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

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

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

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

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

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

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

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