автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.18, диссертация на тему:Математический аппарат и программные средства концептуального проектирования

кандидата физико-математических наук
Пономарёв, Иван Николаевич
город
Москва
год
2007
специальность ВАК РФ
05.13.18
Диссертация по информатике, вычислительной технике и управлению на тему «Математический аппарат и программные средства концептуального проектирования»

Автореферат диссертации по теме "Математический аппарат и программные средства концептуального проектирования"

На правах рукописи

Пономарёв Иван Николаевич

МАТЕМАТИЧЕСКИЙ АППАРАТ И ПРОГРАММНЫЕ СРЕДСТВА КОНЦЕПТУАЛЬНОГО ПРОЕКТИРОВАНИЯ

Специальность 05.13.18 — Математическое моделирование, численные методы и комплексы программ

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук

11111111111111»

003161720

Москва - 2007

Работа выполнена на кафедре концептуального анализа и проектирования Московского физико-технического института (государственного университета)

Научный руководитель

доктор технических наук, доктор экономических наук, профессор КУЧКАРОВ Захирджан Анварович

Официальные оппоненты доктор физико-математических наук,

профессор, член-корреспондент РАН ПАВЛОВСКИЙ Юрий Николаевич, доктор технических наук, профессор ВОДЬФЕНГАГЕН Вячеслав Эрнстович

Ведущая организация Институт системного анализа РАН

д

Защита диссертации состоится*«/ ноября 2007 года в*/ ч на заседании диссертационного совета К212 156 02 в Московском физико-техническом институте (государственном университете) по адресу 141700, Московская область, г Долгопрудный, Институтский пер , д 9, ауд 903 КПМ

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

Автореферат разослан 0 октября 2007 года

Ученый секретарь диссертационного совета К212 156 02 к ф-м н

О С Федько

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ Актуальность работы

Аппарат родов структур был разработан группой французских математиков под коллективным псевдонимом Н Бурбаки в 40-х годах XX в Цель, поставленная Бурбаки, заключалась в создании универсального способа описания (экспликации) математических объектов средствами теории множеств Большая часть современных на тот момент разделов анализа, абстрактной алгебры и топологии была изложена в родах структур в многотомном трактате Н Бурбаки «Начала математики»

Метод концептуального анализа и проектирования систем организационного управления (КАиП СОУ) разрабатывается в нашей стране с 1970-х гг Основная идея метода (предложенная С П Никаноровым и Д Б Персицем) заключается в использовании аппарата родов структур для описания нематематических предметных областей Такое описание производится в виде родо-структурных моделей (или концептуальных моделей, или концептуальных схем) —• родов структур, снабженных комментариями, указывающими на соответствие между термами модели и объектами описываемой предметной области К главным приложениям концептуальных методов относятся создание систем организационного управления и автоматизированных систем управления предприятиями с использованием родоструктурных моделей исследуемой области

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

С некоторой точки зрения, описание предметной области, данное в концептуальных схемах, занимает промежуточное положение между исходным кодом программного обеспечения (полностью формальным, но содержащим избыток технических подробностей) и описанием предметной области на естественном языке (простым, но, вероятно, содержащим двусмысленности, пробелы и противоречия) В этом плане концептуальная схема близка по своей сути к описанию организации, выполненному в виде диаграммы на каком-либо языке графического моделирования (иМЬ, ГОЕР и т п ), но имеет более высо-

кую выразительную способность (мы не ограничены заранее заготовленными «шаблонами», диктующими взгляд на систему в языках, подобных UML) и возможности в каждый момент времени работать с небольшими, обозримыми аспектами предметной области с тем, чтобы провести синтез описывающих их схем в результирующую схему

В настоящее время широкое применение получили автоматизированные системы бизнес-моделирования, к которым относятся и так называемые CASE-средства (сокр Computer Aided Software Engineering) Наличие подобной системы для метода КАиП позволило бы значительно повысить эффективность его применения на практике В связи с этим необходима четкая формализация аппарата концептуальных методов и его исследование с позиций автоматизации работы с концептуальными схемами

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

На основании изложенного тема диссертации является актуальной

Цель и задачи работы

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

1 исследовать синтаксические и семантические ограничения, накладываемые, по определению, на тексты родов структур, и разработать метод автоматического контроля выполнения этих ограничений,

2 исследовать свойства и область применимости наиболее востребованных в практике концептуального проектирования операций над родами структур и разработать методы, позволяющие производить эти операции автоматически,

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

4 на основе разработанных методов создать программный комплекс, автоматизирующий концептуальный анализ и проектирование

Научная новизна

1 Показано, что аппарат родов структур Бурбаки может быть построен не только на основе предложенного Бурбаки синтаксиса математических теорий и аксиоматики теории множеств, но также на основе аксиоматической теории множеств Цермело-Френкеля с помощью языка исчисления предикатов первого порядка, что обосновало использование в концептуальном анализе и моделировании более распространенных на сегодня и привычных для специалистов теории Цермело-Френкеля и языка этой теории

2 Исследованы и доказаны в виде теорем свойства классов Е-объектов родов структур, полученных с помощью операций порождения множества структур данного рода и синтеза, выявлен и доказан в виде теоремы критерий непротиворичивости синтезированных родов структур, состоящий в том, что род структуры, полученный синтезом, непротиворечив тогда и только тогда, когда у каждого из синтезируемых родов структур имеется по Е-объекту, причем эти объекты таковы, что каждый терм, соответствующий конкретизируемому базисному множеству первого рода структуры, равномощен терму, соответствующему конкретизирующему терму второго рода структуры

3 Установлено, что выявленные Бурбаки критерии биективной переносимости термов и соотношений могут быть описаны в виде семантических правил атрибутной формальной грамматики, что дало возможность осуществлять автоматический контроль биективной переносимости с помощью известных методов реализации языков программирования

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

Практическая ценность

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

2 Реализованы алгоритмы автоматического выполнения операций синтеза родов структур и операции порождения множества структур данного рода с автоматической генерацией вспомогательных аксиом

3 Разработана и реализована технология хранения сети родоструктур-ных моделей, получаемых с помощью операций порождения множества структур и синтеза, позволяющая автоматически проводить изменения в зависимых моделях при изменениях в базисных моделях, что облегчает внесение согласованных правок в набор моделей при концептуальном моделировании и проектировании

4 Реализованы методы визуализации текстов родов структур с помощью М-графов и сети родоструктурных моделей в виде операционных схем, что позволяет проектировщикам быстрее ориентироваться в текстах моделей

Методы исследования

В работе использовались методы математической логики и теории множеств, а также теории реализации языков программирования Защищаемые положения

На защиту выносятся

1 Определение аппарата родоструктурного моделирования, построенное на языке первого порядка и теории множеств Цермело-Френкеля, позволившее перейти в концептуальном анализе к более распространенным на сегодня и привычным для специалистов теории и языку

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

3 Доказательства теорем о свойствах классов Е-объектов родов структур, полученных с помощью операций порождения множества структур данного рода и синтеза, и критерия непротиворечивости синтезированного рода структуры

4 Программный комплекс, реализующий функции

• проверки текстов родов структур на соответствие синтаксическим правилам и условиям биективной переносимости и ссылочной целостности (парсера),

• выполнения операций синтеза родов структур и операции порождения множества структур данного рода,

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

• визуализацию текстов родов структур с помощью М-графов и операционных схем

Апробация работы и научные публикации

Основные результаты диссертационной работы были доложены, обсуждены и получили одобрение специалистов на следующих научных конференциях и семинарах научные конференции МФТИ (Долгопрудный, 20032007 г г), VI Международная научно-практическая конференция «Информационные технологии и математическое моделирование» (Анжеро-Судженск, 2007 г), семинары кафедры концептуального анализа и проектирования (Москва, 2003-2007 г г), научных семинарах отдела систем математического обеспечения Вычислительного центра им Дородницына РАН Программа «Бур-бакизатор» внедрена в учебный процесс на кафедре Концептуального анализа и проектирования факультета ИВТ МФТИ

Основные результаты диссертации опубликованы в девяти работах, в том числе в одной — в издании из списка, рекомендованного ВАК РФ

Структура и объем диссертации

Диссертация состоит из введения, пяти глав, заключения и списка использованных источников, включающего 77 наименований Работа изложена на 98 страницах

КРАТКОЕ СОДЕРЖАНИЕ РАБОТЫ Введение

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

Глава 1 Концептуальные модели. Постановка задачи

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

Глава 2. Шкалы и ступени

Глава начинается с обзора предшествующих работ по теме исследования Далее вводятся операции над схемами конструкции ступеней, которые будут задействованы в главе 3

Определим операции над схемами конструкции ступеней, используя определение схемы конструкции ступени, данное Бурбаки Если при программной реализации интерпретировать упорядоченную последовательность упорядоченных пар индексов, введенную Бурбаки, как динамический массив двух-компонентных структур, то приведенные здесь определения прямым образом преобразуются в процедуры на каком-либо языке программирования

Пусть ¿> = (с1; ст) — схема конструкции ступени над п множествами Тогда схема над п множествами есть схема, полученная добавлением к в пары (1,0), т е

Ф5=(С1, с™, (1,0)),

и для ступени, построенной по схеме

Пусть ¿>1 = (с1, с1п) — схема над р множествами и ¿г = (с|, с^) — схема над (? множествами Тогда схема х над тах(р, <?) множествами есть схема, полученная объединением и и добавлением к результату пары (I + 1,1), т е

51Х52 = (С}, с1,С2ь €¡,(1 +1,1)), и для ступени, построенной по схеме 5х х 5г,

(б1! х 32){хи жтах(р^)] = ^[жх, ау] х 52[жх, хг/],

р'

Операция ф определена для любой схемы конструкции ступени, операция х — для любой пары схем Далее будут рассмотрены операции, определенные лишь для схем, удовлетворяющих некоторым требованиям

Назовем Р-схемами такие схемы конструкций ступеней, у которых последняя пара имеет вид (вт, 0), ат > 0 Если Б есть Р-схема над п множествами, т е 5 = (сх, Ст-1, (ат,0)), то схема ОБ над не более чем п множествами есть схема, полученная из исходной взятием только первых т. — ат пар

£>5 = (сх, ст-ат)

Можно сказать, что операция В «снимает ф» со ступени, построенной по схеме 5

Легко видеть, что для произвольной схемы 5 имеет место = Я, но

соотношение = 5 имеет место только для Р-схем, т к если Б — не

Р-схема, то операция Б для нее не определена

Назовем Х-схемами такие схемы конструкций ступеней, у которых последняя пара имеет вид (ат,Ьт), причем ат > 0, Ьт > 0 Если 5 есть Х-схема над п множествами, те ¿> = (сх, Сщ-х, (ат, Ьт)), то схемы Рх5 и Р25 над не более чем п множествами есть схемы, полученная из исходных взятием только первых т — ат пар или т — Ьт пар, соответственно

— (СЬ Ст—ат) ^ Р2в = (си Ст-Ьт)

Можно сказать, что операции Рх и Р2 «расчленяют на сомножители» ступень, построенную по Х-схеме £> Легко видеть, что если йх — Х-схема, 82 и 5з - любые схемы, то Р^) х Р2(31) = 5Ь Рх(52 х 53) = 52

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

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

По схеме Я конструкции ступени М-граф строится по следующему алгоритму 1) каждая из пар (аг, Ьг) соответствует г-й вершине графа, 2) если пара имеет вид (аг, 0), аг > 0, то к ней проводится дуга, исходящая из вершины с номером г—аг, 3) если пара имеет вид (аг, Ьг), а, > 0, Ьг > 0, то к ней проводятся две дуги с номером 1 из вершины г — аг и с номером 2 из вершины г - Ьг

Пример М-графа см на рис 1 в нем вершина А соответствует ступени ф(ж1), вершина В — ступени х\ х хо и т д

При отрисовке изображения М-графа на плоскости удобно использовать понятие ранга ступени (введенное Н К Никитиной), отображая вершины,

соотношения (глава 3)

Рис 1 Пример М-графа

имеющие одинаковый ранг, на одном уровне (именно так сделано на на рис 1) Соотношение типизации при этом иллюстрируется так, как на рис 1 сделано для терма имеющего типизацию х хз)

В программе «Бурбакизатор» [1] нами реализована визуализация М-графов для имеющихся в обрабатываемых этой программой родах структур соотношений типизации, построенная на описанных здесь принципах

Характерно смысловое и графическое соответствие между М-графами и диаграммами нотации ORM (Object Role Modelling), применяемыми некоторыми специалистами как альтернатива UML на этапе концептуального моделирования предметной области (подробнее см текст диссертации) ORM в настоящий момент представляет собой хорошо проработанную методику концептуального моделирования Имеются CASE-средства для моделирования в ORM, проработаны методы построения баз данных на основе ORM-моделей, произведен сравнительный анализ возможностей ORM-моделей и UML-диаграмм классов Представляется перспективным сравнительное исследование методологий ORM и КАиП, возможное объединение опыта обоих методологий

Глава 3. Синтаксис языка родов структур

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

По Бурбаки, теория множеств (а значит, и любая выразимая в ней математическая теория) может быть построена с помощью только нескольких основных символов в простом языке Мы предлагаем усовершенствованный вариант базового языка Бурбаки Lb, который с помощью форм Бэкуса-Наура может быть определен следующим образом

Синтаксис Ьд снабжается аксиоматикой и правилами вывода, порождающими формулы, истинные в теории множеств

Грамматика Ьд относится к классу ЬЬ( 1), т е допускает создание детерминированного алгоритма построения дерева синтаксической структуры «сверху вниз» при чтении строки слева направо Кроме того, префиксная форма записи (е ху вместо х € у) позволяет применять особенно простые необходимые условия синтаксической корректности, свойственные грамматикам Лукасевича

Из-за ограниченного количества основных символов, запись в языке Ьв даже несложных математических понятий и утверждений занимает большой

<терм> <буква>

I

<соотношение> |<соотношение><соотношение>

I £<терм><терм>

<терм>

объем и неудобочитаема Бурбаки предлагают использовать стандартные логические и теоретико-множественные обозначения, рассматривая их как сокращающие обозначения для конструкций в языке Ьв (например, А В ^ У^АВ и 3хА ^ (тхА | х)А, где (у | х)А означает текстовую подстановку у вместо х в строку А)

В связи с прикладным значением языка Бурбаки возникает задача синтаксического контроля термов и соотношений, записанных с использованием сокращающих символов, на предмет возможности их трансляции в Ьв Еще одна проблема связана с тем, что применяемая Бурбаки специфическая аксиоматика, связанная с синтаксисом Ьд, отличается от принятой в большинстве современных монографий по логике и теории множеств В частности, это затрудняет использование работ Бурбаки в процессе обучения специалистов по концептуальному анализу и проектированию Более знакомыми специалистам и распространенными на сегодняшний день являются язык и аксиоматика теории множеств Цермело-Френкеля Мы предлагаем их использование в качестве основы для аппарата родов структур и обосновываем их эквивалентность языку Ьв и теории множеств Бурбаки

В качестве символов языка первого порядка теории множеств Цермело-Френкеля применяются имена переменных, знак € для обозначения принадлежности элемента множеству, знаки V, логических связок, кванторы V, 3, скобки С учетом того, что все используемые в этом языке знаки являются сокращающими обозначениями, определяемыми непосредственно через знаки Ьв, не составляет труда построить транслятор из Ьгр в УАСС-спецификация такого транслятора выглядит следующим образом (в качестве операций, применяемых в семантических правилах, используются конкатенация строк, обозначаемая точкой, и операция Заменить (строка!., строка2, строкаЗ), выполняющая в аргументе строка!, замену подстроки строка2 на подстроку строкаЗ)

<терм> • <буква>

<соотношение> | -|<соотношение>

I (<соотношение>\/<соотношение>){$$ = V $1 $3,} I (<соотношение>&<соотношение>) {$$ = -1 V -1$1->$3,} I (<соотношение>=Ф-<соотношение>) {$$ = V —■ $1 $3,} I 3<буква><соотношение> {$$ = 3аменить($3, $2, т ( $3 )),} I \/<буква><соотношение> {$$ = Заменить ($3, $2, ~>т §2 ( $3 I ,<терм>£<терм> {Вывести($1 + $2)> Кроме того, можно принять более распространенную в современной литературе аксиоматику исчисления предикатов и теории множеств Цермело-Френкеля, основанную на Ьгр, которая, за небольшими исключениями, эквивалентна аксиоматике Бурбаки В рамках этой системы легко показать,

что если в этой теории выводится 3€ и -й- Л), то выводится также £ и А) Для того, чтобы ссылаться на существующее и единственное и как на терм, образованный с помощью формулы А, обычно применяют обозначение {г | Л} Термам такого вида не могут соответствовать термы языка первого порядка, где термами являются только константы или переменные Термы вида {г | А} являются принципиально новой синтаксической конструкцией, но корректно внедряются в язык Ьгр, если показать, как преобразовывать формулы с их участием в формулы языка первого порядка Синтаксис языка Ьгр можно расширить определением если А — формула, не содержащая переменную и в качестве параметра, и ZFC I- ЗиУг(г € 6 ив А), то {г \ А} — терм Термы такого вида могут участвовать в логических формулах наряду с переменными и константами Формулы расширенного языка могут быть переведены в формулы языка первого порядка по следующему алгоритму 1) все вхождения терма {г | А} заменяются на переменную и, 2) формула обрамляется конструкцией е и -44- А) & ), при этом имена переменных г и и должны быть выбраны таким образом, чтобы не возникло нежелательных связываний кванторами Основное свойство данного определения задает следующее утверждение (доказательство в тексте диссертации)

Теорема 1. Если формула В' получена из формулы В заменой подформул вида £ € и на (£ | г) А, то 3 е и » А) & В) ~ 3 и(\/,ф ей» А) к В')

Теорема 1 дает возможность свободно заменять конструкции вида £ € € {г | А} в формулах на {I | г)А, что значительно упрощает вид (и, как следствие, вывод) этих формул

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

Пусть зафиксирована некоторая теория множеств Т в языке Как известно, род структуры представляет собой текст из следующих составляющих (конституэнт) переменных Х\, хп, называемых основными базисными множествами, термов <?ь вт теории Т, называемых вспомогательными базисными множествами, формулы Т вида ё, 6 5[а.1, хп,0\, 0т] (где 5(2:1, хп,01, 0т] — ступень над п + т множествами), являющейся соотношением типизации и называемой типовой характеристикой рода структуры, формулы К, биективно переносимой при типизации Т, называемой аксиомой рода структуры

Определенные выше конституэнты составляют ядро рода структуры (терминология Н К Никитиной) К телу рода структуры относятся термы и теоремы рода структуры, от которых не зависит аксиома R Соотношение R, термы и теоремы рода структуры записываются на языке теории множеств с использованием сокращающих символов На основании изложенного построена синтаксическая спецификация языка родов структур Lg, которая ложится в основу атрибутной грамматики этого языка, приведенной ниже на с 17

Для реализации синтаксического анализатора, работающего по этим правилам, использовалась утилита YACC Автором использовалась версия YACC для системы разработки Delphi, генерирующая код анализатора на языке Object Pascal

Глава 4. Семантика языка родов структур

В четвертой главе решается задача построения атрибутной формальной грамматики языка родов структур Глава начинается с обзора предшествующих работ по теме исследования Далее приводятся условия биективной переносимости, преобразованные к каноническому виду, задействующему операции над схемами конструкции степеней, определенные в соответствующей главе, с тем, чтобы осуществить переход к формулировке данных условий как семантических правил атрибутной грамматики языка родов структур

1 0 есть биективно переносимый терм типаф(5'[жх, ]), какова бы ни была схема S",

2 базисные множества х\, хп есть биективно переносимые термы, т(хг) =

= Ф(®,),

3 вспомогательные множества Oi, 9m есть биективно переносимые термы, т{вг) = ф(0,),

4 родовая константа d, для которой вводится соотношение типизации d € € 5[zi, ], есть биективно переносимый терм, г(d) = ¿"[жх, ],

5 если R, возможно, зависящее от £, биективно переносимо в случае, когда r(i) = ], то {t € ¿ЭДжх, ] | R} — биективно переносимый терм, r({t € St[x1: ] I R}) = фф[®ь ])

6 если £ — биективно переносимый терм, причем Т I- VxVу(х е £ Szy € £ £ х = у), то (равный единственному элементу множества £) есть биективно переносимый терм и r(|J£) = Dt(£),

7 если £ — биективно переносимый терм, то ргг(£) и рг2(£) — биективно переносимые термы, т(ргх(£)) = Лт(£), т(рг2(£)) =

8 если £ и г] — биективно переносимые термы и ф(т(£)) = т(г]), то £ € г] — биективно переносимое соотношение,

9 если £ и г] — биективно переносимые термы и т(£) = т(г)), то £ = г) — биективно переносимое соотношение,

10 если Л и Л' — биективно переносимые соотношения, то -¡К, Л V Л', Д& Л', Л =>- Л', Л Л' — биективно переносимые соотношения,

11. если Л, возможно, зависящее от биективно переносимо в случае, когда т(£) = . ], то \/£ £ ]Л и € ¿¿[^ь ]Л — биективно

переносимые соотношения

Данных условий биективной переносимости достаточно для того, чтобы распространить их на большинство стандартных разновидностей термов и соотношений теории множеств Для этого обычные знаки для соотношений и термов должны быть переопределены как сокращающие обозначения для биективно переносимых соотношений и термов, с введением ограничений на типизацию аргументов Например, отношение «С» может быть переопределено как ^ С ^ VI е £>т({)(£ 6 £ £ € ??), так определенное отношение С является биективно переносимым по построению

Обобщение ограниченных кванторов Мх £ £Л ^ Ух £ £>т(£)(ж £ £ =>- Л), Эж € £Л ^ Уж е £>г(4)(х £ £ & Л) При таком определении ограниченных кванторов сохраняются законы де Моргана -|9£ £ 5*[жь ]Д ~ е € 54[ж1, ]->Л, -АЛ 6 ]Д ~ ЗЬ € ]-|Д Для знаков «С» и «С»

определения аналогичные

По аналогии можно определить переносимые варианты некоторых из операций над термами

. Синглетон {£} ^ {х 6 т(Щх = £)}, т(ф) =

• Множество-сумма и £ ^ {х 6 £Шт(£)|Зм 6

ее(*е«)},таК) = Ф(ШМО)

На рис 2 показана «верхушка» М-графа для ступеней, типизирующих термы У £ и связанную переменную х, фигурирующую в определении и£ Таким образом, множество-сумма, образованное от биективно переносимого терма с типом ]), биективно

переносимо (для случая типизации ]) см п 6

в приведенном выше списке критериев биективной переносимости)

Выражение ф(ООт(£)) не сокращается до поскольку иначе поте-

ряется ограничение на типизацию аргумента (£>т(£) определена и для типов ф^Жх, ]), не только фф^Жь ])) Общее правило таково допустимо сокращать конфигурацию £*ф (т к она всюду применима и тождественна), но недопустимо сокращать конфигурацию ф!) (т к она, хотя и является тождественной, применима только для ступеней вида ]))

Аналогичным образом, т(У У(£)) = ф(Г>п+1т(£))

п раз

• Объединение £ и т] ^ {х € £>т(£)|(х € £) V (х € ??)}, т(£ и ??) = = ф(1)(т(£))) = ф(0(т(?]))) Аналогичным образом вводятся пересечение, дополнение и симметрическая разность

• Дополнение множества относительно собственного типа С£ ^ {х €

е ХМОК® е О}. = ф(1М0)

• Неупорядоченная пара {£, ??} ^ {£} и {??}, т({£, ??}) = ф(Г>ф(£)) =

= Ш=Ш

• Упорядоченная пара (£, г/) = и({ж € т(£) хг(?|)|(рг1(а;) = £)&(рг2(а:) =

• Декартово произведение £ х г) ^ {х 6 £>г(0 х От(г]) | (ргх(ж) 6 е 0 & (рг2(ж) € 7/)}, т(£ х,)= ф(Г>г(0 X Вг(ч))

Заметим, что, в отличие от упорядоченной пары, биективно переносимой при как угодно типизированных £ и г), декартово произведение биективно переносимо для термов, имеющих характер множеств

• Множество-степень ф(£) {х в т(£)|(ж С £)}, т(ф(£)) = ф(ф(£>т(Ш

Рис 3 15

4 о

Ж € РГ1(0

Рис 4

• Большая проекция Ргг(£) ^{ге Р,1)т(£)\Эу 6 £(х = рг,(г/))}, г(Рг,(£)) =

= ф(Р,£>т(0)

• Возведение в степень ^ ^ {/ € ФФ(»7 х О I / V ~'> £}> Т(С) = = фф(Ят(ч) х Рг(<£))

Как и в компиляторе обычного языка программирования, в программном коде парсера должна быть доступна таблица символов, в которую помещается информация о именах и типизации глобальных термов, а также информация о именах и типизациях связанных переменных кванторных формул и сверток вида {ле5[ ] | Л}

В качестве особого типа данных в коде парсера необходимо ввести тип данных «ступень», для которого должны быть доступны операции £>, Р, х, ф, определенные в главе 2 (из их определений непосредственно ясны необходимые структуры данных и алгоритмы)

V

Рис 5

Кроме того, должны быть доступны следующие процедуры

1 НачалоБлокаО — увеличивает счетчик вложенных блоков на единицу

2 Добавить (имя, типизация) — добавляет запись о терме с именем имя, типизацией типизация и уровнем видимости, равным текущему счетчику вложенных блоков, в таблицу символов Генерирует ошибку «Переменная с именем уже определена», если производится попытка дважды использовать одно и то же имя для разных термов

3 Найти (имя) — находит в таблице символов терм с именем имя, помечает его как использованный и возвращает сохраненную типизацию этого терма Генерирует ошибку «Переменная не определена», если производится попытка найти типизацию неопределенного терма

4 КонецБлокаО — уменьшает счетчик вложенных блоков на единицу и удаляет из локальной таблицы символов все термы с уровнем видимости, равным предыдущему значению счетчика вложенных блоков Если при этом приходится удалять записи о термах, не помеченных как использованные, генерируется ошибка «Локальная переменная определена, но не используется»

5 Сравнить(типизация1, типизация2) — если аргумент типизация1 не равен аргументу типизация2, генерирует ошибку «Несоответствие типизации ожидается , имеется »

6 Преобразовать(имяФункции, парам1, парам2, типизация)—преобразовывает типизацию для теоретико-множественных операций с одним аргументом, как описано выше

7 Принять () — завершает разбор конституэнты и возвращает управление вызывающей программе

С учетом всего сказанного выше, спецификация языка Ь$ родоструктур-ной экспликации, записанная в форме синтаксических и семантических правил Уасс, выглядит следующим образом

<родструктуры> <конституэнты> <конституэнты> <конституэнта>

I <конституэнта>, <конституэнты>

<конституэнта>

<имяБМ><конецСтроки> {Добавить($1, 1);

Принять()

I <имяРС>€<ступень><конецСтроки> {Добавить ($1, $3),

Принять()Л

<имяТерма>=<терм><конецСтроки> {Добавить ($1, $3),

Принять()Л <имяАксиомы> <соотношение><конецСтроки>

{Принять(),} <имяТеоремы> <соотношение><конецСтроки>

{Принять(),}

<ступень> <ИмяБМ> {$$ = £>(Найти($1))Л

<ступень>х <ступень> {$$ = $1х $3,>

<терм>

I ф(<ступень>)

{$$ = ф$2Л

<ИмяБМ> <буква> <ИмяРС> <ИмяТерма> <терм>и<терм> <терм>П<терм> <терм>\<терм> <терм>—<терм> <терм> х <терм> -1<терм> <функция> {<перечисление>} {<декларация>I<соотношение>}

{НачалоБлока(), $$ = ф$2, КонецБлокаО,}

(<кортеж>)

{$$ = Найти($1)Л {$$ = Найти($1)Л {$$ = Найти($1)Л {$$ = Найти($1)Л {Сравнить($1, $3), $$ {Сравнить($1, $3), $$ {Сравнить($1, $3), $$ {Сравнить($1, $3), $$ {$$ .= ф(Г>$1 х £>$3) Л {$$ = ф£>$2Л

{$$ = ф$2Л

= ф!)$1Л = ф£>$1Л = ф£»$1Л = ф£$1Л

<функция> <ИмяФункции>(<терм>)

{$$ = Преобразовать($1, $3)Л

I <ИмяФункции><число>(<терм>)

{$$ = Преобразовать($1, $2, $4)Л I <ИмяФункции><число><ЧИ°ЛО>(<терм>)

{$$ = Преобразовать($1, $2, $3, $5)Л

>

<кортеж> <терм>

I <кортеж>, <терм> {$$ =$1х$3)Л

<перечисление>

<терм>

I <перечисление>,<перечисление>

{Сравнить($1, $3), $$ = $1,}

<декларация>

<буква>€<ступень> {Добавить($1, $3), $$ = $3,}

<соотношение>

<квантор><алгформ> О

1 <алгформ> О

1 <предикат> О

<квантор> \/<декларация> {>

1 3<декларация> О

1 <квантор>,<квантор> О

<алгформ> (<предикат>) О

1 (<алгформ>) {>

1 -!<алгформ> {>

1 <алгформ>&<алгформ> О

1 <алгформ>\/<алгформ> о

1 <алгформ>=Ф><алгформ> О

1 <алгформ>Ф5><алгформ> О

<предикат> <терм>€<терм> {Сравнить ($1,£)$3),}

1 <терм>^<терм> {Сравнить ($1, D$3), >

1 <терм> С<терм> {£>$3, Сравнить($1, $3),}

1 <терм>С<терм> {jD$3, Сравнить($1, $3),}

1 <терм>$£<терм> {¿>$3, Сравнить($1, $3),}

i <терм>=<терм> {Сравнить($1, $3),}

1 <терм>т^<терм> {Сравнить($1, $3),}

1 <терм>= 0 {£>$1,}

1 <терм>^ 0 {£>$!,>

На основании приведенной спецификации языка с помощью утилиты YACC был построен семантико-синтаксический анализатор родоструктурных текстов программы «Бурбакизатор» [1] Глава 5. Операции над родами структур

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

Введем вспомогательные определения Пусть даны некоторый род структуры Е (в теории Т, с типовой характеристикой Т и аксиомой Н) и теория Т', более сильная, чем Т Тогда терм теории Т вида (£1, £,п,$) называется Т,-объектом (или теоретико-множественной интерпретацией Е), если

Иногда также бывает удобно говорить о классе всех Е-объектов в теории Т Ке = {(*1> хп,й)\Тк.Щ

Если а = (£1, £»!<£)> то условия а е «<г есть Е-объект», «сг есть теоретико-множественная интерпретация Е» эквивалентны

Операция порождения множества структур данного рода

Пусть дан род структуры Е, имеющий типовую характеристику (1 е 5[ж1, и класс Е-объектов /Се Операция порождения множества структур данного рода позволяет в этом случае построить из Е такой род структуры Е, что класс Е-объектов будет удовлетворять условию

/Сё = {(ж1, 3) | Ус1{<1 е й =>■ (жь х„, 4) в /Се)}

Например, если Е есть род структуры функции из Хг в Х2, то Е, получаемый из него операцией порождения множества структур данного рода, есть род структуры множества функций из Х\ в Х2 В Е-объекте элементами множества, соответствующего родовой константе, являются множества, которые могут интерпретировать родовую константу Е при фиксированной интерпретации базисных множеств

Построить Е можно по следующим правилам

1 базисные множества не изменяются,

2 типовая характеристика Т вида <1 6 5[ж1, ж„] заменяется на Т вида

3 аксиома Д заменяется на аксиому Д вида V« £ ¿((и | <1)11)

Родовая константа в этом процессе превращается во множество, каждый элемент которого типизирован как исходная родовая константа Прежние выражения для внутренних термов Е теряют смысл в Е в силу изменения типизации родовой константы

Теорема 2. Если Е построена из Е при помощи операции порождения структур данного рода, то класс Е-объектов удовлетворяет условию

/С§ = {(жх, хп, ¿) | Ш((1 еЗ=>(х1; хп, й) е /Се)}

Теорема 3. Род структуры Е, полученный операцией порождения множества структур данного рода, заведомо непротиворечив, и (£1, £„, 0) есть Т,-объект при любых множествах £1, £п

Теорема 4. Среди Т,-объектов (£1, £п,<5) существуют объекты с непустым 5 тогда и только тогда, когда Е непротиворечив

Теорема 5 Если Р — теорема Е, то формула Р вида Ум € ¿(и | й)Р есть теорема Е

Операция синтеза родов структур Потребность в синтезе родов структур возникает, когда имеется набор родов структур (в простейшем случае — пара родов структур Е и В), описывающих различные аспекты изучаемой области, и требуется построить обобщающий, комплексный род структуры Обычного слияния текстов родов структур бывает недостаточно часто к получившемуся роду структуры необходимо добавлять утверждения о тождестве некоторых множеств Е некоторым множествам 0 Прикладной пример пусть имеется род структуры, описывающий «теорию субординации» в организации, в котором задано множество сотрудников х\, и на этом множестве введено отношение «подчинения» 6 х Хг) Пусть, кроме этого, имеется род структуры, описывающий «теорию родства», в котором задано множество людей хг и на этом множестве введено отношение «быть родителем» <1% € %$(х2 х Х2) Если теперь отождествить множество сотрудников в первой теории и людей во второй (что в рассматриваемом случае можно сделать простой заменой хх на Х2 по всему тексту рода структуры), то в синтезированной теории будет выразимо и отношение «подчинения», и отношение «быть родителем» Также можно будет образовать принципиально новые термы, в которых используются оба эти отношения Например, терм «множество подчиненных, которые являются детьми своего начальника»

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

Формальное определение Пусть даны

1 род структуры Е (который будем называть конкретизируемым родом структуры) с выделенными в нем р базисными множествами Без ограничения общности можно считать, что Е построен на п базисных множествах Х1, хп, из которых выделены р первых х\, хр, р ^ п, и имеет родовую константу Йе, типовую характеристику Те вида <1% € 5е[х1, хп] и аксиому Де,

2 род структуры 0 (который будем называть конкретизирующим родом структуры) с выделенными в нем р внутренними термами фр с типами Я^йх), ф(5п), причем не исключается случай, когда любой из фг

совпадает либо с базисным множеством 0, либо с родовой константой © Без ограничения общности можно считать, что © построен на т базисных множествах жп+х, хп+т и имеет родовую константу а!е, типовую характеристику Т© вида (¿в £ ¿>е[жп+ь жп+т] и аксиому Де

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

1 конкретизируемые множества жх, хр удаляются из текста конкретизируемого рода структуры (их место в синтезированном роде структуры займут термы фр),

2 тексты обоих родов структур объединяются в один текст (предполагается, что имена всех конституэнт выбраны таким образом, что ни одно имя конституэнты из Е не встречается среди имен конституэнт О), если в текстах Ей© имеются совпадающие вспомогательные базисные множества, то в тексте Е оставляется одна копия,

3 типовая характеристика вида (¿к € ^[жх, жр,жр+х,жп] заменяется на типовую характеристику Т вида

(I £= [Жп+1, Жгс-^т], Вр[хп | I, Хп+Гп], . Хп\

(напомним, что термы ф^ фр имеют типы ф^х), ф(5п)),

4 во всех прочих выражениях все вхождения букв Жх, хр заменяются на термы фр мы будем обозначать через Д результат этой замены в аксиоме Дц, ясно, что выражения Те и Де, не содержащие Жх, хр в качестве параметров, в синтезированную схему перейдут без изменений,

5 добавляется аксиома синтеза Яв вида {ф\ \ х\) (фр \ хр)Т£

При этом мы говорим, что множества хр рода структуры Е отождествляются с термами ф^, фр рода структуры © Вновь заметим, что не исключается случай, когда любой из фг совпадает либо с базисным множеством ©, либо с родовой константой © (второе, правда, возможно лишь в случае, когда (¿е ), т е с?е имеет характер множества)

Действия, производимые нами при синтезе, например, рода структуры функции с родом структуры разбиения множества, можно следующим об-

разом проиллюстрировать на М-графах

о *

г< Ул

Теорема 6. Пусть Ё — синтезированный из Е и О род структуры, К.^ — класс Т,-объектов В этом случае выполняется соотношение

^Ё = {(Жр+1,

(^(жрКГЕ&Дв&Ге&Лв)} Теорема 7. Если .Р — теорема Е, то (фх | Ж1) (фр \ хр)Р — теорема Е

Критерий непротиворечивости синтезированного рода структуры Легко видеть, что необходимым условием непротиворечивости синтезированного рода структуры является непротиворечивость синтезируемых родов структур Однако даже при синтезе непротиворечивых родов структур может образоваться противоречивый род структуры Критерий непротиворечивости определяет следующее утверждение

Теорема 8. Пусть Е — конкретизируемый, © — конкретизирующий род структуры, причем множества Х\, хр рода структуры Е отождествляются с термами фх, фр рода структуры 0 Синтезированный род структуры Е непротиворечив тогда и только тогда, когда одновременно выполнены следующие условия

1 существует Т,-объект V = (£1,

2 существует <д-объект и> = (£п+ъ £п+т,5е),

3 каждое из множеств £1, равномощно соответствующему множеству фг = (£„+1 I хп+1) (£„+т I хп+т){5в I ¿в)фг, где г — 1 р, р < п

Рис 6 Пример операционной схемы

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

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

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

Задавшись базисными родами структур и операционной схемой, мы однозначным образом определяем ядра всех родов структур, которые будут получены с помощью соответствующих операций В программе «Бурбакизатор» [1] нами на описанных здесь принципах реализовано конструирование сети родов структур и визуализация сети обрабатываемых этой программой родов структур в виде операционной схемы Заключение

В заключении изложены основные результаты диссертационной работы и указываются перспективные направления исследований по данной теме ОСНОВНЫЕ РЕЗУЛЬТАТЫ ДИССЕРТАЦИИ

1 Показано, что роды структур Бурбаки могут быть построены на аксиоматической теории множеств Цермело-Френкеля с сохранением синтаксической основы теории

2 Установлено, что выявленные Бурбаки критерии биективной переносимости термов и соотношений могут быть описаны в виде семантических

правил атрибутной формальной грамматики с применением операций над схемами конструкций ступеней

3 Построена атрибутная грамматика языка родов структур и программно реализован парсер, осуществляющий автоматическую проверку текста на соответствие синтаксическим правилам и условиям биективной переносимости и ссылочной целостности

4 Исследованы свойства классов Е-объектов родов структур, полученных с помощью операций порождения множества структур данного рода и синтеза и реализованы алгоритмы автоматического выполнения операций синтеза родов структур и операции порождения множества структур данного рода

5 Разработана и реализована технология хранения сети концептуальных схем, получаемых с помощью операций порождения множества структур и синтеза, с автоматическим обновлением зависимых конституэнт

6 Реализованы методы визуализации текстов родов структур с помощью М-графов и сети концептуальных схем в виде операционных схем

СПИСОК РАБОТ, ОПУБЛИКОВАННЫХ АВТОРОМ ПО ТЕМЕ

ДИССЕРТАЦИИ

1 Пономарев И Н Семантико-синтаксический анализатор текстов родов структур Бурбакизатор // Технология концептуального проектирования / Под ред Никанорова С П — М «Концепт», 2004 — С 78-79

2 Пономарев И Н Применение LALR-парсинга к языкам математической логики и теории множеств // Труды XLVIII научной конференции МФТИ / Моек физ -тех ин-т — Долгопрудный, 2005 - С 213-214

3 Пономарев И Н Язык родоструктурной экспликации как атрибутная грамматика // Труды XLVII научной конференции МФТИ / Моек физ -тех ин-т — Долгопрудный, 2004 — С 129-130

4 Пономарев И Н Введение в математическую логику и роды структур учебное пособие — М МФТИ, 2007 — 240 с

5 Пономарев И Н Методические указания по курсу Математическая логика-2 - М МФТИ, 2007 - 26 с

6 Пономарев И Н Язык родов структур // Эл журнал СУПиР — 2007 — Т 7 — 20 с — Зарегистрировано в Информрегистре 02 08 2007 п/н 0420700026/0001 http //www supir ru/j7sl html

7 Пономарев И Н Операции над родами структур // Эл журнал СУ-ПиР — 2007 — Т 8 — 9 с — Зарегистрировано в Информрегистре 02 08 2007 п/н 0420700026/0005 http //www supir ru/j8sl html

8 Пономарев И H, Гараева Ю Р Базисные преобразования на множестве ступеней и операции над термами в аспекте этих преобразований // Труды XLVI научной конференции МФТИ / Моек физ -тех ин-т — Долгопрудный, 2003 - С 112-114

9 Пономарев И Н Спецификация языка концептуального моделирования // Системы управления и информационные технологии — 2007 — Т 3 2 (29) - С 286-291

Подписано в печать 28 09 07 Формат 60x90/16 Уел печ л 1 0 Тираж 80 экз Московский физико-технический институт (государственный университет)

НИЧ МФТИ

Оглавление автор диссертации — кандидата физико-математических наук Пономарёв, Иван Николаевич

ВВЕДЕНИЕ

Актуальность работы.

Цель и задачи работы.

Научная новизна.

Практическая ценность.

Методы исследования.

Защищаемые положения.

Глава1. Концептуальные модели. Постановка задачи

1.1. Основные понятия концептуального моделирования.И

1.2. Прикладной пример построения концептуальной модели.

1.3. Задачи автоматизации концептуального моделирования.

Глава2. Шкалы и ступени

2.1. Обзор работ по теме исследования.

2.2. Определение схемы конструкции ступени.

2.3. Операции над схемами конструкции ступеней

2.4. М-графовая визуализация соотношения типизации. Связь с нотацией ORM.

ГлаваЗ. Синтаксис языка родов структур

3.1. Обзор работ по теме исследования.

3.2. Язык теории множеств LB и аксиоматика Бурбаки.

3.3. Язык первого порядка LZF и аксиоматика Цермело-Френкеля, трансляция в LB.

3.4. Синтаксис родов структур

Глава4. Семантика языка родов структур

4.1. Обзор работ по теме исследования.

4.2. Условия биективной переносимости как семантические правила

4.3. Построение производных биективно переносимых операций над термами.

4.4. Контроль ссылочной целостности текста посредством таблицы символов

4.5. УАСС-спецификация языка родоструктурной экспликации.

Глава5. Операции над родами структур

5.1. Обзор работ по теме исследования.

5.2. Предварительные замечания.

5.3. Операция порождения множества структур данного рода и её свойства

5.4. Операция синтеза родов структур и её свойства.

5.5. Критерий непротиворечивости синтезированного рода структуры

5.6. Сеть родов структур и операционная схема.

Введение 2007 год, диссертация по информатике, вычислительной технике и управлению, Пономарёв, Иван Николаевич

Актуальность работы

Аппарат родов структур [1, 33, 34, 73] был разработан группой французских математиков под коллективным псевдонимом Н. Бурбаки в 40-х годах XX в. Цель, поставленная Бурбаки, заключалась в создании универсального способа описания (экспликации) математических объектов средствами теории множеств. Большая часть современных на тот момент разделов анализа, абстрактной алгебры и топологии была изложена в родах структур в многотомном трактате Н. Бурбаки «Начала математики».

Метод концептуального анализа и проектирования систем организационного управления (КАиП СОУ) [64, 65, 66] разрабатывается в нашей стране с 1970-х гг. Основная идея метода (предложенная С. П. Никаноровым и Д. Б. Персицем в [37, 38]) заключается в использовании аппарата родов структур для описания нематематических предметных областей. Такое описание производится в виде концептуальных схем — родов структур, снабжённых комментариями, указывающими на соответствие между термами и объектами описываемой предметной области. К главным приложеням концептуальных методов относятся создание систем организационного управления и автоматизированных систем управления предприятиями с использованием концептуальных схем исследуемой области. Некоторое обоснование выбора аппарата родов структур было дано в [42] (перепечатано в 2001-м в [59]).

Перед другими методами описания предметных областей концептуальные схемы имеют ряд преимуществ. Описание предметной области (например, деятельности организации), данное на естественном языке, доступно каждому, но, в силу своей неформализованности, может содержать двусмысленности, пробелы и логические противоречия. С другой стороны, полностью формальное описание отдельных аспектов деятельности организации содержится, в некотором смысле, в исходном коде работающей в этой организации автоматизированной системы управления (например, класса MRP или ERP), которая производит, в частности, регистрацию установленных бизнес-процессов и проверку выполнения принятых регламентирующих ограничений (бизнес-правил). Но, во-первых, успешно разработанная и внедрённая в организацию система наличествует далеко не всегда, а во-вторых, программный код понятен только небольшому кругу IT-специалистов.

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

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

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

В настоящее время широкое применение получили автоматизированные системы бизнес-моделирования, к которым относятся и так называемые CASE-средства (сокр. Computer Aided Software Engineering). Наличие подобной системы для метода КАиП позволило бы значительно повысить эффективность его применения на практике. В связи с этим необходима чёткая формализация аппарата концептуальных методов и его исследование с позиций автоматизации работы с концептуальными схемами.

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

На основании изложенного тема диссертации является актуальной.

Цель и задачи работы

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

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

2. исследовать свойства и область применимости наиболее востребованных в практике концептуального проектирования операций над родами структур и разработать методы, позволяющие производить эти операции автоматически;

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

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

Научная новизна

1. Показано, что аппарат родов структур Бурбаки может быть построен не только на основе предложенного Бурбаки синтаксиса математических теорий и аксиоматики теории множеств, но также на основе аксиоматической теории множеств Цермело-Френкеля с помощью языка исчисления предикатов первого порядка, что обосновало использование в концептуальном анализе и моделировании более распространённых на сегодня и привычных для специалистов теории Цермело-Френкеля и языка этой теории.

2. Исследованы и доказаны в виде теорем свойства классов Е-объектов родов структур, полученных с помощью операций порождения множества структур данного рода и синтеза, выявлен и доказан в виде теоремы критерий непротиворичивости синтезированных родов структур, состоящий в том, что род структуры, полученный синтезом, непротиворечив тогда и только тогда, когда у каждого из синтезируемых родов структур имеется по Х-объекту, причём эти объекты таковы, что каждый терм, соответствующий конкретизируемому базисному множеству первого рода структуры, равномощен терму, соответствующему конкретизирующему терму второго рода структуры.

3. Установлено, что выявленные Бурбаки критерии биективной переносимости термов и соотношений могут быть описаны в виде семантических правил атрибутной формальной грамматики, что дало возможность осуществлять автоматический контроль биективной переносимости с помощью известных методов реализации языков программирования.

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

Практическая ценность

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

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

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

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

Методы исследования

В работе использовались методы математической логики и теории множеств, а также теории реализации языков программирования.

Защищаемые положения

На защиту выносятся:

1. Определение аппарата родоструктурного моделирования, построенное на языке первого порядка и теории множеств Цермело-Френкеля, позволившее перейти в концептуальном анализе к более распространённым на сегодня и привычным для специалистов теории и языку.

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

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

4. Программный комплекс, реализующий функции

• проверки текстов родов структур на соответствие синтаксическим правилам и условиям биективной переносимости и ссылочной целостности (парсера);

• выполнения операций синтеза родов структур и операции порождения множества структур данного рода;

• хранения сети концептуальных схем, получаемых с помощью операций синтеза и порождения множества структур данного рода, с автоматическим обновлением унаследованных частей;

• визуализацию текстов родов структур с помощью М-графов и операционных схем.

Основные результаты диссертационной работы были доложены, обсуждены и получили одобрение специалистов на следующих научных конференциях и семинарах: научные конференции МФТИ (Долгопрудный, 2003— 2007 г. г.); семинары кафедры концептуального анализа и проектирования (Москва, 2003-2007 г. г.); научных семинарах отдела систем математического обеспечения Вычислительного центра им. Дородницына РАН. Программа «Бурбакизатор» внедрена в учебный процесс на кафедре Концептуального анализа и проектирования факультета ИВТ МФТИ.

Основные результаты диссертации опубликованы в девяти работах, в том числе в одной — в издании из списка, рекомендованного ВАК РФ.

Заключение диссертация на тему "Математический аппарат и программные средства концептуального проектирования"

ЗАКЛЮЧЕНИЕ

В диссертационной работе получены следующие результаты:

1. Показано, что роды структур Бурбаки могут быть построены на аксиоматической теории множеств Цермело-Френкеля с сохранением синтаксической основы теории.

2. Установлено, что выявленные Бурбаки критерии биективной переносимости термов и соотношений могут быть описаны в виде семантических правил атрибутной формальной грамматики с применением операций над схемами конструкций ступеней.

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

4. Исследованы свойства классов Е-объектов родов структур, полученных с помощью операций порождения множества структур данного рода и синтеза и реализованы алгоритмы автоматического выполнения операций синтеза родов структур и операции порождения множества структур данного рода.

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

6. Реализованы методы визуализации текстов родов структур с помощью М-графов и сети концептуальных схем в виде операционных схем.

Перспективными представляются следующие направления исследований:

1. Разработка автоматизированных методов верификации доказательств родостуруктурных теорем. Нам представляется, что задача может быть решена теми же методами построения атрибутных грамматик, что и решённая нами задача проверки биективной переносимости термов и соотношений.

2. Сравнительное исследование методологий ОЯМ и КАиП (см. с. 2.4. настоящей работы), в которых моделирование предметных областей производится по схожим принципам, возможное объединение опыта обоих методологий.

3. Решение вопроса о непротиворечивости рода структуры в тех частных случаях, когда это возможно сделать автоматически.

4. Конструирование Е-объектов для непротиворечивых родов структур в тех частных случаях, когда это возможно сделать автоматически.

5. Поиск доказательств теорем рода структуры в тех частных случаях, когда это возможно сделать автоматически.

Библиография Пономарёв, Иван Николаевич, диссертация по теме Математическое моделирование, численные методы и комплексы программ

1. Теория множеств и математическая логика

2. Бурбаки Н. Теория множеств: Пер. с фр. / Под ред. В. А. Успенского.— М.: Мир, 1965.- 455 с.

3. Верещагин Н. К., Шень А. X. Лекции по математической логике и теории алгоритмов. Ч. 1. Начала теории множеств. — М.: МЦНМО, 2002. — 128 с. ftp://ftp.mmce.ru/users/shen/logic/sets/.

4. Верещагин H. К., Шень A. X. Лекции по математической логике и теории алгоритмов. 4.2. Языки и исчисления,— М.: МЦНМО, 2002,— 288 с. ftp://ftp.mmce.ru/users/shen/logic/firstord/.

5. Д. Гильберт, П. Бернайс. Основания математики, т. 2: Теория доказательств / Под ред. Адяна С. И. — М.: Наука, 1982. — 652 с.

6. Д. Гильберт, П. Бернайс. Основания математики, т. 1: Логические исчисления и формализация арифметики / Под ред. Адяна С. И. — М.: Наука, 1979. 557 с.

7. Ершов Ю. Л., Палютин Е. А. Математическая логика: Учебное пособие. — 3-е, стереотип, изд. — СПб.: «Лань», 2004. — 336 с.

8. Игошин В. И. Математическая логика и теория алгоритмов. — М.: «Академия», 2004. — 448 с.

9. Иех Т. Теория множеств и метод форсинга. — М.: Мир, 1973.— 150 с.

10. Казимиров Н. И. Введение в аксиоматическую теорию множеств. — Интернет-издание, http: //lib .mexmat. ru/books/1394.

11. Клини С. К. Введение в метаматематику / Под ред. В. А. Успенского. — М.: Изд-во иностранной лит-ры, 1957. — 528 с.

12. Клини С. К. Математическая логика. — 2-е, стереотип, изд. — М.: УРСС, 2005.-480 с.

13. Колмогоров А. H., Драгалин А. Г. Математическая логика. — 2-е, стереотип. изд. М.: УРСС, 2005. - 240 с.

14. Коэн П. Дж. Теория множеств и континуум-гипотеза. — М.: Мир, 1969. — 347 с.

15. Куратовский К., Мостовский А. Теория множеств. — М.: Мир, 1970. — 416 с.

16. Успенский В. А., Верещагин Н. КПлиско В. Е. Вводный курс математической логики. 2-е изд. - М.: ФИЗМАТЛИТ, 2004. - 128 с.

17. Френкель А. А., Вар-Хиллел И. Основания теории множеств / Под ред. А. С. Есенина-Вольпина. — М.: Мир, 1966. — 556 с.

18. Хао Ван, Мак-Нортон Р. Аксиоматические системы теории множеств: Пер. с фр. — М.: Изд-во иностранной лит-ры, 1963.— 54 с.

19. Хаусдорф Ф. Теория множеств / Под ред. П. С. Александрова, А. Н. Колмогорова. — 3-е, стереотип, изд. — М.: УРСС, 2004. — 204 с.

20. Разработка языков программирования

21. Levine J. R., Mason T., Brown D. Lex & Yacc. — 2nd, updated edition.— Sebastopol: O'Reilly k, Associates, 1992. — 366 pp.

22. Ахо А., Сети P., Ульман Дж. Компиляторы: принципы, технологии, инструменты: Пер. с англ. — М.: Издательский дом «Вильяме», 2003.— 768 с.

23. Ахо А., Ульман Дж. Теория синтаксического анализа, перевода и компиляции: в 2 тт. / Под ред. Курочкина В. M. — М.: Мир, 1978.— Т. 1. Синтаксический анализ. — 612 с.

24. Ахо А., Ульман Дж. Теория синтаксического анализа, перевода и компиляции: в 2 тт. / Под ред. Курочкина В. M. — М.: Мир, 1978.— Т. 2. Компиляция. — 488 с.

25. Мартыиенко Б. К. Языки и трансляции: Учебное пособие. — СПб.: Изд-во СПбГУ, 2004. 229 с.

26. Пентус А. Е., Пентус М. Р. Математическая теория формальных языков: Учебное пособие. — М.: БИНОМ, 2006.— 248 с. http://www.mccme. ru/f ree-books/pentus/pentus.pdf.

27. Пратт Т., Зелковиц М. Языки программирования: разработка и реализация.: Пер. с англ. — СПб.: Питер, 2002. — 688 с.

28. Рейуорд-Смит В.Дж. Теория формальных языков. Вводный курс: Пер. с англ. — М.: Радио и связь, 1988.— 128 с.

29. Серебряков В. А. и др. Теория и реализация языков программирования: Учебное пособие. — М.: МЗ-Пресс, 2003. — 345 с.

30. Фостер До\с. Автоматический синтаксический анализ: Пер. с англ. / Под ред. Э. 3. Любимского. — М.: Мир, 1975. — 72 с.

31. Фридл Дж. Регулярные выражения: Пер. с англ. — 2е изд. — СПб.: Питер, 2003.-464 с.

32. Хаитер Р. Основные концепции компиляторов: Пер. с англ. — М.: Издательский дом «Вильяме», 2002. — 256 с.

33. Карпов, Ю. Г. Теория и технология программирования. Основы построения трансляторов. — СПб.: БХВ-Петербург, 2005.— 272 с.

34. Теория родов структур Бурбаки и автоматизация концептуального проектирования

35. Павловский Ю. Н. О шкалах родов структур // Доклады РАН. — 1998. — Т. 363.-С. 163-165. http://www.ras.ru/ph/0002/CFTS2FJH.pdf.

36. Павловский Ю. Н., Смирнова Т. Г. Шкалы родов структур, термы и соотношения, сохраняющиеся при изоморфизмах. — М.: ВЦ РАН, 2003.— 92 с.

37. Павловский Ю. Н., Смирнова Т. Г. Проблема декомпозиции в математическом моделировании. — М.: ФАЗИС, 1998. — 266 с.

38. Тищенко А. В. Шкалы множеств и теории родов структур // Подмножество: Сб. ст. М.: Концепт, 2000.- С. 3-6.

39. Тищенко А. В. Алгебра родов структур // Освоение и концептуальное проектирование интеллектуальных систем: Сб. тез. докл. и сообщ. науч. конф., Москва, 21-27 апреля 1990 г. Т. 1. - 1990. - С. 58.

40. Никаиоров С. П., Персиц Д. Б. Об одном направлении в развитии теории систем и его значении для приложений // Вопросы кибернетики / АН СССР. 1977. - Т. 32. - С. 74-89.

41. Гараева Ю. Р. Разработка автоматизированных средств анализа синтаксиса и семантики текстов на языке родоструктурной экспликации. — Дипломная работа на кафедре прикладных концептуальных методов МФТИ, 1998. Науч. рук. Никитина Н. К.

42. Акименков А. М. О мощности модели теории, в которой заданный терм этой теории не пуст // Подмножество: Сб. ст.— М.: Концепт, 2000. — С. 49-59.

43. Климишин В. В. Автоматизированная библиотека и программный комплекс синтеза концептуальных моделей // Управление большими системами: Материалы Междунар. науч.-практ. конф., Москва, 22-26 сентября 1997 г.- 1997.

44. Ключников А. В. Эквивалентность теорий родов структур // Подмножество: Сб. ст. М.: Концепт, 2000.- С. 60-73.

45. Ключников А. В., Кучкаров 3. А. Логические методы синтеза родов структур // Управление большими системами: Материалы Междунар. науч.-практ. конф., Москва, 22-26 сентября 1997 г. 1997.- С. 334-335.

46. Кононенко А. А. Блок синтеза концептуальных схем и блок построения комплекта организационных процедур // Управление большими системами: Материалы Междунар. на-уч.-практ. конф., Москва, 22-26 сентября 1997 г.- 1997.-С. 58-63.

47. Никитина Н. К. Развитие математических средств концептотехники // Освоение и концептуальное проектирование интеллектуальных систем: Сб. тез. докл. и сообщ. науч. конф., Москва, 21-27 апреля 1990 г. — 1990. — С. 5-6.

48. Никитина Н. КПостников В. В. Развитие языка родоструктурной экспликации предметных областей // Освоение и концептуальное проектирование интеллектуальных систем: Сб. тез. докл. и сообщ. науч. конф., Москва, 21-27 апреля 1990 г. 1990.

49. Постников В. В. Разработка языка родоструктурной экспликации концептуальных моделей // Подмножество: Сб. ст. — М.: Концепт, 2000.— С. 37-48.

50. Пунинская В. А. Об одном классе PC-форм // Подмножество: Сб. ст. — М.: Концепт, 2000.- С. 74-87.

51. Тищенко А. В., Акименков А. М., Ключников А. В. Система операций над концептуальными схемами, представленными в родоструктурной форме // Подмножество: Сб. ст. — М.: Концепт, 2000. — С. 7-36.

52. Юдкин Ю. Ю. Программный комплекс для поддержки операций над концептуальными схемами и визуализации М-графа // Управление большими системами: Материалы Междунар. науч.-практ. конф., Москва, 22-26 сентября 1997 г. 1997. - С. 367.

53. Юрьев О. И. Разработка автоматизированных средств поддержки процессов концептуального анализа и проектирования сложных предметных областей. — Дипломная работа на кафедре прикладных концептуальных методов МФТИ, 1997. Науч. рук. Никитина Н. К.

54. Кононенко A.A. и др. Технология концептуального проектирования.— М.: Концепт, 2004. 580 с.

55. Прикладное использование родов структур

56. Кучкаров 3. А. Методы концептуального анализа и синтеза в теоретическом исследовании и проектировании социально-экономических систем: Курс лекций. В 2 т. М.: «Концепт», 2005.- 252, 260 с.

57. Кучкаров 3. А. Теоретические основы и методы проектирования систем организационного управления сложными социально-экономическими структурами: Автореф. дис. докт. техн. наук: 05.13.10. — СЗАГС, 2007. — 47 с.

58. Никитина Н. К. Разработка и исследование методов и средств автоматизированного синтеза баз данных на концептуальном уровне: Автореф. дис. канд. техн. наук: 05.13.06. МФТИ, 1984.- 24 с.

59. Исследования по безопасности / Под ред. С. П. Никанорова. — М.: Концепт, 1998. 624 с.

60. Никапоров С. П. Теоретико-системные конструкты для концептуального анализа и проектирования. — М.: Концепт, 2006. — 312 с.

61. Публикации автора по теме диссертации

62. Пономарев И. Н. Семантико-синтаксический анализатор текстов родов структур Бурбакизатор // Технология концептуального проектирования / Под ред. Никанорова С. П. — М.: «Концепт», 2004.— С. 78-79.

63. Пономарев И. Н. Применение ЬАЬИ,-парсинга к языкам математической логики и теории множеств // Труды ХЬУШ научной конференции МФТИ / Моск. физ.-тех. ин-т. — Долгопрудный, 2005. — С. 213-214.

64. Пономарев И. Н. Язык родоструктурной экспликации как атрибутная грамматика // Труды XLVII научной конференции МФТИ / Моск. физ.-тех. ин-т. — Долгопрудный, 2004. — С. 129-130.

65. Пономарев И. Н. Введение в математическую логику и роды структур: учебное пособие. М.: МФТИ, 2007. - 240 с.

66. Пономарев И. Н. Методические указания по курсу Математическая логика-2. М.: МФТИ, 2007. - 26 с.

67. Пономарев И. Н. Язык родов структур // Эл. оюурнал СУПиР. — 2007. — Т. 7.— 20 е.— Зарегистрировано в Информрегистре 02.08.2007 п/н 0420700026/0001. http: //www. supir. ru/j7sl.html.

68. Пономарев И. H. Операции над родами структур // Эл. эюурнал СУПиР. — 2007. — Т. 8. — 9 с. — Зарегистрировано в Информрегистре 02.08.2007 п/н 0420700026/0005. http://www.supir.ru/j8sl.html.

69. Пономарев И. Н., Гараева Ю. Р. Базисные преобразования на множестве ступеней и операции над термами в аспекте этих преобразований // Труды XLVI научной конференции МФТИ / Моск. физ.-тех. ин-т. — Долгопрудный, 2003.- С. 112-114.

70. Пономарёв И. Н. Спецификация языка концептуального моделирования // Системы управления и информационные технологии. — 2007. — Т. 3.2 (29).-С. 286-291.