Оглавление
Введение
1 Методы формализации информационных моделей и их уточнений
1.1 Каноническая информационная модель.
1.2 Денотационная и аксиоматическая семантики как способ
формального определения информационных моделей
1.3 Методы формализации уточнения
1.4 Методы формализации языков спецификаций в АМЫ
1.5 Выводы по главе
2 Формальное определение ядра канонической информационной модели
2.1 Абстрактный синтаксис ядра канонической модели
2.2 Экстенсиональная интерпретация абстрактных типов данных
2.3 Семантические домепьт и семантические функции
построения пространства состояний
2.4 Семантические функции формирования ограничений на
пространство состояний.
2.4.1 Ограничение типизации экземпляров классов
2.4.2 Ограничения, налагаемые отношением типподтип . .
2.4.3 Ограничения, налагаемые отношением классподкласс
2.4.4 Ограничения, налагаемые инвариантами.
2.5 Семантические функции формирования предикатов,
отвечающих функциям .
2.6 Семантические функции преобразован и я правил
канонической модели в формулы над пространством состояний
2.6.1 Семантика конъюнкции коллекций с условием
2.6.2 Семантика объединения коллекций
2.7 Семантические функции преобразования формул
канонической модели в формулы над пространством состояний
2.7.1 Атомарные предикаты
2.7.2 Условия
2.7.3 Составные формулы
2.7.4 Алгоритм 1еЕДеМетапИсв
2.8 Выводы по главе
3 Моделирование конструкций ядра канонической модели средствами языка АМИ
3.1 Основные принципы моделирования
3.1.1 Экстенсиональная интерпретация АТД.
3.1.2 Двойственное представление методов АТД
3.1.3 Моделирование структуры спецификаций типов
канонической модели при помощи средств композиции абстрактных машин АКШ
3.2 Контекстная машина.
3.3 Структура абстрактной машины, соответствующей
типу моделирование атрибутов, методов, инвариантов .
3.4 Моделирование формул канонической модели
предикатами АМИ
3.4.1 Атомарные предикаты
3.4.2 Условия
3.4.3 Составные формулы
3.5 Моделирование формул канонической модели
обобщенными подстановками АМИ
3.6 Моделирование правил канонической модели
обобщенными подстановками АМН
3.7 Адаптация моделирования конструкций канонической
модели в АМЫ для доказательства непротиворечивости спецификаций
3.8 Выводы но главе.
4 Корректность отображения канонической модели в язык АМЫ
4.1 Принципы доказательства корректности отображения
канонической модели в ЛМЫ.
4.2 Множество состояний информационной системы,
задаваемой множеством абстрактных машин
4.3 Инъективное отображение пространства состояний ИС,
задаваемой спецификацией модуля канонической модели, в пространство состояний ИС, задаваемой набором абстрактных машин.
4.4 Корректность отображения ограничений на пространство
состояний.
4.5 Корректность отображения спецификаций методов.
4.5.1 Корректность отображения формул.
4.5.2 Корректность отображения правил.
4.6 Выводы по главе
5 Автоматизация доказательства корректности решения задач над множественными неоднородными информационными источниками
5.1 Программа автоматического отображения спецификаций
канонической модели в язык
5.2 Автоматизация доказательства корректности задачи синтеза
канонических моделей для посредников
5.3 Автоматизация доказательства корректности композиции ИС
из компонентов
5.4 Выводы но главе
Заключение
Литература
- Київ+380960830922