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

Описывается язык предикатного программирования P (Predicate programming language). Предикатная программа есть рекурсивно определяемая система вычислимых логических утверждений. На языке P можно запрограммировать любое алгоритмическое решение задачи, спецификация которой представима в виде математического предиката. Методология предикатного программирования ориентирована на построение предикатной программы, из которой можно получить эффективную императивную программу применением системы оптимизирующих трансформаций. Возможности языка P существенно шире известных языков функционального программирования. Наряду с функциональным стилем программирования применяется предикатный (операторный) стиль. Удобство и гибкость программирования обеспечивается за счет использования аппарата гиперфункций. Язык определяет развитую систему типов данных. Массивы определяются конструктором forAll (имеющим сходство с циклом forAll в FORTRAN-90) и его производными формами. Параллелизм программы естественным и явным образом определяется конструкциями параллельного оператора и конструктора forAll.

Для класса программ, спецификация которых представима в виде математического предиката, предлагается формализация понятия программы в виде исчисления вычислимых предикатов. На базе исчиcления строится язык предикатного программирования, продолжающий линию языков функционального программирования. Предикатная программа может быть преобразована в эффективную императивную применением последовательности трансформаций. Обычный цикл императивной программы есть результат трансформации хвостовой рекурсии в предикатной программе. Чтобы преобразовать рекурсию к хвостовому виду, применяется универсальный метод обобщения исходной задачи. Трансформация рекурсии в цикл открывает возможность применения серии трансформаций: подстановку определения предиката на место вызова, склеивание переменных и др. Гиперфункция оказывается адекватной формой спецификации для многих программ. Оператор расщепления, конструируемый на базе гиперфункции, определяет гибкие формы записи алгоритмов большой выразительнойсилы. В частности, с помощью расщеплений естественным образом реализуется обработка исключений. Как следствие, появляются процедуры с несколькими равноправными выходами. Гиперфункции и расщеплению нет аналогов ни в одном языке программирования.

В данной работе исследуется временное расширение трассовой эквивалентности, дается ее теоретико-категорная характеризация и решается проблема разрешимости этого вида эквивалентности для подкласса конечных временных структур событий. Данная работа выполнена при поддержке программы РАН "Н аучные проекты молодых ученых" (грант N 114) и ФЦП "Интеграция" ("Учебные научные центры").

В общем случае семантики исследованы выразительная сила, сложность проверки на модели и разрешимость для следующих программных логик: (1) Элементарной Пропозициональной Динамической Логики (EPDL), Ветвящейся Логики, расширенной действиями (Act-CTL), и Пропозиционального mu-исчисления (muC), обогащенных средствами (2) Пропозициональной Логики Знаний или Пропозициональной Логики Общих Знаний. Основным в статье является изучение задачи проверки на модели для вышеперечисленных комбинированных логик в забыва- ющей асинхронной семантике и синхронной семантике с абсолютной памятью.

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

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

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

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

Работа представляет собой обзор двух объектно-ориентированных технологий создания современных распределенных систем - CORBA и RMI. Архитектура RMI (Remote Method Invocation, т.e. вызов удаленного метода), которая интегрирована с JDK, является продуктом компании JavaSoft и реализует распределенную модель вычислений. RMI позволяет клиентским и серверным приложениям через сеть вызывать методы клиентов/серверов, выполняющихся в Java Virtual Machine, и также предоставляет возможность пересылать сами объекты от машине к машине. Технология CORBA (Common Object Request Broker Architecture), разрабатываемая OMG (Object Managment Group) с 1990-го года, позволяет вызывать методы у объектов, находящихся в сети где угодно, так, как если бы все они были локальными объектами. Одним из основных принципов CORBA является интероперабельность, возможность использования в одной системе различных приложений, реализованных на разных языках и выполняющихся на разных платформах. Целью данной работы является показать масштабность и преимущества технологии CORBA по сравнению с RMI. Кроме того, так как еще нет реализации компонентной модели CORBA, в работе рассматривается технология создания серверных объектов EJB (Enterpise JavaBeans), предложенная фирмой Sun. В компонентной модели EJB используются сильные стороны как CORBA, так и RMI. В приложении приводятся с подробными комментариями два примера применения CORBA и EJB.

В работе описаны основные схемы трансляции, разработанные для конвертора с существенного расширения языка Паскаль в С++. Конвертор был написан по заказу крупной телекоммуникационной корпорации и должен был не только транслировать исходный M-Pascal код в функционально эквивалентный С++ код, но и отвечать ряду требований. Совокупность расширений Паскаля и требований к конвертору значительно повлияла на разработку схем трансляции.

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

Настоящая публикация основана на материалах Координационного Комитета по вычислительной технике АН СССР, связанных с заседанием его Комиссии по системному математическому обеспечению. Это заседание было посвящено обсуждениюи тога работ новосибирской школы системного и теоретического программирования за более, чем двадцатилетнюю историю ее существования. При рассмотрении итогов работы школы затрагивалась и вся ее история, но главное внимание уделялось результатам 70-х и планам на 80-е. Перспективы, намеченные на 80-е годы, в общем были верными. Эта публикация очень хорошо дает срез состояния работ новосибирской школы на начало 80-х годов и в этом отношении является хорошим и естественным дополнением к издаваемому сборнику "Становление новосибирской школы программирования (мозаика воспоминаний)". Работа поддержана грантом РГНФ N 02-05-12010в и издается на средства этого фонда.