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

• Автор: Ступников, Сергей Александрович
• Шифр специальности: 05.13.17
• Научная степень: Кандидатская
• Год защиты: 2006
• Место защиты: Москва
• Количество страниц: 195 с. : ил.

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 Алгоритм SideEffectSemantics
2.8 Выводы по главе
3 Моделирование конструкций ядра канонической модели средствами языка AMN
3.1 Основные принципы моделирования
3.1.1 Экстенсиональная интерпретация АТД
3.1.2 Двойственное представление методов АТД
3.1.3 Моделирование структуры спецификаций типов
канонической модели при помощи средств композиции абстрактных машин AMN
3.2 Контекстная машина
3.3 Структура абстрактной машины, соответствующей
типу: моделирование атрибутов, методов, инвариантов
3.4 Моделирование формул канонической модели
предикатами AMN
3.4.1 Атомарные предикаты
3.4.2 Условия
3.4.3 Составные формулы
3.5 Моделирование формул канонической модели
обобщенными подстановками AMN
3.6 Моделирование правил канонической модели
обобщенными подстановками AMN
3.7 Адаптация моделирования конструкций канонической
модели в AMN для доказательства непротиворечивости спецификаций
3.8 Выводы по главе
4 Корректность отображения канонической модели в язык AMN
4.1 Принципы доказательства корректности отображения
канонической модели в AMN
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 Выводы по главе
Заключение
Литература
А Синтаксис ядра канонической модели
В Нотация абстрактных машин
В.1 Спецификация состояний системы в АМИ
В.2 Спецификация операций в ААШ
В.З Виды конструкций и структурные механизмы АМИ
В.4 Формализация понятия уточнения в АМИ
В.5 Формализация непротиворечивости спецификаций в АМИ
С Представление языков ЫМЬ и ОСЬ в канонической
информационной модели
Б Примеры конструкций АМ1Г, моделирующих
спецификации канонической модели

в формулу, накладывающую ограничения на экстенсионал, осуществляется семантической функцией sTypelnvariant. Эта функция по имени типа выделяет инвариант типа и преобразует его в формулу логики предикатов первого порядка. Замена имен атрибутов а*, где dom(L) = {ai an}, на выражения v(a{) преобразует полученную формулу в ограничение на экстенсионал. Данная замена специфицируется помещением списка замен переменных в фигурные скобки: выражение /{а —> £}, где / — формула, а — переменная в }, t — терм, есть формула /, в которой вхождения а заменены на t.
Определение функции sTypelnvariant семантическими соотношениями будет дано в следующих разделах.
Заметим, что формируемый собственный экстенсионал удовлетворяет свойству (2.1), рассмотренному в разделе 2.2: для каждого набора значений атрибутов типа, удовлетворяющего инварианту, в экстенсионале существует ровно один такой (помеченный именами атрибутов) набор. Очевидно также, что собственные экстенсионалы типов с различными наборами атрибутов не пересекаются - свойство (2.3). Действие константных атрибутных функций на экстенсноналах определяется следующим образом. Если а - атрибут типа Т, v € W, и v(a) GU, т.е. атрибут а ссылается на значения объектного типа, то действие константной атрибутной функции а на значении v определяется как a(v) = S(v(a)). Если v(a) не есть объектный идентификатор или а = self, то a(v) = u(a).
Имея определение семантической функции sAVAL, можно определить семантическую функцию sOBJ, формирующую множество значений объектных типов.
sOBJTSL — {н | v 6 sAVAC{TSLj Л self € dom(n)}
Функция sIRSection формирует семантический домен тотальных функций из множества имен коллекций в множество подмножеств AVAO.
sIRSection[CS L] = s ClassSpecList | CSLj sClassSpecListCSL
[U {sClassSpec[i(CSL)l} -» P{sAVAC[TSL])],

где i(CSL) — i-я спецификация класса из списка sClassSpecCD = sClassDeclCD sClassDeclID MNL SCL /5]