Введение
Методы формализации информационных моделей и их уточнений 16
1.1 Каноническая информационная модель 16
1.2 Денотационная и аксиоматическая семантики как способ формального определения информационных моделей . 22
1.3 Методы формализации уточнения 27
1.4 Методы формализации языков спецификаций в AMN . 32
1.5 Выводы по главе 37
Формальное определение ядра канонической информационной модели 39
2.1 Абстрактный синтаксис ядра канонической модели 41
2.2 Экстенсиональная интерпретация абстрактных типов данных 43
2.3 Семантические домены и семантические функции построения пространства состояний 45
2.4 Семантические функции формирования ограничений па пространство состояний 52
2.4.1 Ограничение типизации экземпляров классов 52
2.4.2 Ограничения, налагаемые отношением тип-подтип . 54
2.4.3 Ограничения, налагаемые отношением класс-подкласс 55
2.4.4 Ограничения, налагаемые инвариантами 56
2.5 Семантические функции формирования предикатов, отвечающих функциям 57
2.6 Семантические функции преобразования правил канонической модели в формулы над пространством состояний 60
2.6.1 Семантика конъюнкции коллекций с условием , . 62
2.6.2 Семантика объединения коллекций 68
2.7 Семантические функции преобразования формул
канонической модели в формулы над пространством состояний 68
2.7.1 Атомарные предикаты 68
2.7,2 Условия 70
27.3 Составные формулы 74
2.7.4 Алгоритм SideEffectSemantics 74
2.8 Выводы по главе 76
Моделирование конструкций ядра канонической модели средствами языка AMN 78
3.1 Основные принципы моделирования 78
ЗЛЛ Экстенсиональная интерпретация АТД 78
ЗЛ.2 Двойственное представление методов АТД 80
3 1.3 Моделирование структуры спецификации типов канонической модели при помощи средств композиции абстрактных машин AMN 80
3-2 Контекстная машина 83
3.3 Структура абстрактной машины, соответствующей типу: моделирование атрибутов, методов, инвариантов - - - 85
3.4 Моделирование формул канонической модели предикатами AMN 90
3.4Л Атомарные предикаты 90
3.4.2 Условия 91
3.4.3 Составные формулы 93
3.5 Моделирование формул канонической модели обобщенными подстановками AMN 94
3.6 Моделирование правил канонической модели обобщенными подстановками AMN 99
3.7 Адаптация моделирования конструкций канонической модели в AMN для доказательства непротиворечивости спецификаций 104
3.8 Выводы по главе 107
Корректность отображения канонической модели в язык AMN 108
4Л Принципы доказательства корректности отображения канонической модели в AMN 108
4.2 Множество состояний информационной системы, задаваемой множеством абстрактных машин 111
4.3 Инъективное отображение пространства состояний ИС, задаваемой спецификацией модуля канонической модели, в пространство состояний ИС, задаваемой набором абстрактных машин 114
4.4 Корректность отображения ограничений на пространство состояний 117
4.5 Корректность отображения спецификаций методов 119
4.5.1 Корректность отображения формул 120
4.5.2 Корректность отображения правил 123
4.6 Выводы по главе 124
5 Автоматизация доказательства корректности решения задач над множественными неоднородными информационными источниками 125
5.1 Программа автоматического отображения спецификаций канонической модели в язык AMN 125
5.2 Автоматизация доказательства корректности задачи синтеза канонических моделей для посредников 129
5.3 Автоматизация доказательства корректности композиции ИС
из компонентов 137
5.4 Выводы по главе 145
Заключение 147
Литература
