URSS.ru - Издательская группа URSS. Научная и учебная литература
Об издательстве Интернет-магазин Контакты Оптовикам и библиотекам Вакансии Пишите нам
КНИГИ НА РУССКОМ ЯЗЫКЕ


 
Вернуться в: Каталог  
Обложка Бабичев А.В. Распознавание и спецификация структур данных
Id: 78383
 
468 руб.

Распознавание и спецификация структур данных

URSS. 2008. 192 с. Мягкая обложка. ISBN 978-5-9710-0215-4.

 Аннотация

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

Идеологически представленный аппарат спецификации и анализа графов аналогичен технике использования теории конечных автоматов для распознавания текстов.

Для специалистов в области теории алгоритмов и основ программирования, а также для аспирантов и студентов старших курсов соответствующих специальностей.


 Содержание

Введение
1. Формальное представление структур данных
 1.1.Функциональные сети
 1.2.Раскрашенные автоматы
2. Типы данных и их спецификация
 2.1.Спецификация уровня функциональных схем
 2.2.Спецификация автоматного уровня
3. Распознавание итерационных типов данных
 3.1.Итерационные автоматы
 3.2.Неразличимые и идеальные структуры данных
 3.3."Регулярные" свойства итерационных автоматов
 3.4.Типы данных, распознаваемые итерационными автоматами
 3.5.О распознавании расширенных итерационных типов
 3.6. Язык моделирования Model-100
  Краткая характеристика языка
  Архитектура машины Model-100
  Использование итерационных автоматов для реализации Model-100
4. Распознавание монадических типов данных
 4.1.Функциональные автоматы
 4.2.Задача согласования и стратегия Киссинджера
  Постановка задачи
  Стратегия Киссинджера
  Комбинаторные алгебры
 4.3.Объектно-ориентированные итерационные автоматы
 4.4.Свойства объектно-ориентированных автоматов
Заключение
Приложения
 Приложение 1. Используемые понятия и обозначения
  Неопределяемые понятия
  Отношения и отображения [1, 2, 5]
  Строки и последовательности [5]
  Метрические пространства [1]
  Универсальные алгебры и термы
  Хорновские дизъюнкты, модели и резолюции
  Обозначения
 Приложение 2. Монадические теории (раздел 2.2)
  Синтаксис
  Классическая интерпретация монадического языка
  Жесткая интерпретация монадического языка
  Мягкая интерпретация монадического языка
 Приложение 3. Итерационные автоматы (разделы 3.1, 3.2)
  Доказательство леммы 1 и теоремы 5 (раздел 3.1)
  Автоматы Скотта (раздел 3.1)
  Рациональные деревья (раздел 3.2, Теоремы 2, 3)
  Доказательство теоремы 4 (раздел 3.1)
  Свойство компактности и анализ на деревьях
  Функциональный гомоморфизм
 Приложение 4. Спецификация и распознавание итерационных типов данных (разделы 2.1, 3.1, 3.4, 3.5, 3.6)
  Определения (раздел 2.1)
  Алгоритм компиляции простых спецификаций (разделы 2.1, 3.1, 3.4, 3.5, 3.6)
  Обоснование алгоритма компиляции (разделы 2.1, 3.1, 3.4)
  Классическая монадическая теория и итерационные автоматы (раздел 3.4)
  Мягкая монадическая теория и итерационные автоматы (раздел 3.4)
 Приложение 5. Объектно-ориентированные автоматы
  Доказательство леммы 4
  Обоснование стратегии Киссинджера
  Итерационные ++ автоматы
  Итерационные++ автоматы и жесткие монадические теории
 Приложение 6. Задача идентификации различий в структурах данных
  Техника идентификации различий в текстах
  Задача поиска пути в лабиринте
  Задача оценки длины идентификатора позиции
Предметный указатель
  A
  F
  А
  Г
  И
  О
  Т
  Х
Список литературы
Содержание

 Из введения

Настоящая работа посвящена решению следующей задачи. Имеется граф. Требуется узнать, содержит или нет этот граф подграфы определенного вида, и если содержит, то указать в каких местах. При этом техника решения должна быть такова, чтобы вид графов, вхождения которых ищутся, мог задаваться в качестве параметра. Более точно, класс решаемых задач можно описать следующим образом: имеется набор графов и набор правил, с помощью которых более крупные графы можно конструировать из более мелких. Требуется узнать, можно ли сконструировать заданный граф. Рассматриваемая постановка исходно возникла как попытка развить сложившуюся к настоящему времени технику верификации и контроля типов данных в языках программирования.

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

С практической точки зрения предлагается технология анализа структур данных (размеченных ориентированных графов), подобная технологии лексических анализаторов.

Основные компоненты подобной технологии представлены на рис.1.

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

Современные средства контроля типов данных также работают по схеме, представленной на рис.1. Например, в C++ (или в Java) в качестве языка спецификаций используется усеченный вариант регулярных выражений над деревьями (с помощью аппарата наследования классов реализуется объединение множеств, а конкатенация и итерация, хотя и не в полной мере, имитируется ссылками на типы членов описываемых классов), а в качестве программы анализа используется конечный автомат над деревьями (этот автомат строится по исходной спецификации).

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

  •  процедуры проверки конкретной структуры данных или программы, которая со структурой данных работает, на соответствие спецификации;
  •  процедуры проверки непротиворечивости самого описания.

    Под непротиворечивостью описания подразумевается факт существования хотя бы одной структуры данных, которая удовлетворяет требованиям, заданным в описании.

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

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

    1. по любому описанию можно автоматически построить программу, которая допускает ровно те графы, которые соответствуют описанию;

    2. выразительные возможности языка спецификаций при жесткой интерпретации довольно высоки (например, на нем можно совершенно точно описать, что такое двунаправленный список).

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

    На рисунке 2 представлена схема информационных зависимостей между разделами.

    Кратчайшая последовательность для освоения основного теоретического результата (раздел 4.3) помечена на рисунке жирными стрелками.

    В главе 1 рассматривается три способа формального представления понятия "структура данных":

  •  функциональные сети (1.1) -- обычные функциональные схемы собранные из функциональных блоков, например схема системы автоматического регулирования;
  •  раскрашенные автоматы (1.2) -- обычные конечные автоматы, состояния которых раскрашены;
  •  раскрашенные автоматы Мура (1.3) -- обычные автоматы Мура, выходные сигналы которых раскрашены -- и описывается тривиальная процедура перевода с языка автоматов (либо автоматов Мура) на язык функциональных схем и обратно.

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

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


     Об авторе

    Андрей Владимирович БАБИЧЕВ

    Кандидат технических наук, старший научный сотрудник. В 1976 г. закончил МИИТ по специальности "прикладная математика". С тех пор работает в Институте проблем управления РАН. Кандидатская диссертация (1982) посвящена вопросам организации беспереборного синтаксического анализа контекстно-свободных языков.

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

    В настоящее время занимается вопросами создания логического языка спецификации технических конструкций.

    В качестве разработчика участвовал в крупных проектах по созданию компиляторов (Fortran77, Pascal, С/С++ , Prolog), систем тестирования/верификации, систем моделирования и систем резервного копирования данных.

  •  
    © URSS 2016.

    Информация о Продавце