Примеры формального анализа транзакций
Обратимся к следующей демонстрационной модели, формально описанной на языке EXPRESS (см. Рис. 4). Модель описывает объектный тип данных A с вещественными атрибутами x, y, z, целочисленным идентификатором id и квалификационным именем q, представленным множеством из трех строк. Модель определяет также объектные типы данных B и C, содержащие необязательную и обязательную ссылки соответственно на экземпляр объекта типа A.
Определение типа A содержит правила Wr1, Wr2, ограничивающие допустимую область значений атрибутов x, y, z, а также правило уникальности Ur1 для значений атрибута id, действие которого распространяется на всю популяцию объектов типа A.
Пусть начальное состояние данных x = {a
Рис. 4. Демонстрационная модель данных, формально описанная на языке EXPRESS
Аналогичные отношения t1' → t2', t1' ⊕ t2'', t1' ∠ t2', и t1'' ∠ t2'' могут быть установлены для операций в сформированном временном журнале T'
T'' = {t1' = del(a), t2' = wr(b1.ref, 0), t1'' = new(b1
B), t2'' = wr(b1.ref, a), …}.
Отношение t1' → t2' вытекает из того, что удаление объекта a требует обнуления соответствующей ссылки b1.ref, указывающей на него. Отношение t1' ⊕ t2'' появляется, потому что операции удаления объекта a в первой транзакции и установки на него ссылки b1.ref во второй транзакции являются взаимоисключающими.
Для временного журнала T'
T'' = {t1' = rm(a.q,…), t2' = in(a.q,…), t1'' = rm(a.q,…), t2'' = in(a.q,…) …}, чтобы сохранить атрибут q в корректном состоянии, необходимо потребовать, чтобы количество элементов соответст-вующего множества было ровно 3. Предполагая, что начальное состояние было корректным и применение каждой транзакции не нарушает целостности, мы устанавливаем отношение кардинальности D(0:0)(t2'+, t2''+, t1'-, t1''-). Это означает, что количество добавляемых элементов равно количеству исключаемых элементов, и мощность множества остается неизменной.Рассмотрим отношения между операциями, порождаемые правилами ограничения области значений. Для корректности итоговой транзакции с временным журналом T'
T'' = {t1' = wr(a.x), t2' = wr(a.y), t1'' = wr(a.z), …} требуется выполнение отношения алгебраической зависимости 
DWr1(t1', t2', t1'')
. В этом случае в итоговую транзакцию включаются все участвующие в ограничении операции первой или второй транзакции, и ограничение будет гарантированно удовлетворено. Отметим, что данное отношение носит предположительный характер, являясь достаточным, но не необходимым условием корректности транзакции. Поэтому при необходимости оно может быть снято на этапе семантического анализа транзакции, но тогда связанное с ней ограничение обязано быть проверено на последующем этапе валидации. Аналогичный вывод справедлив для отношения DWr2(t1', t2', t1''). Однако более детальный анализ показывает, что данное отношение следует исключить из рассмотрения, так как модифицируемые в различных транзакциях атрибуты появляются в различных термах конъюктивной нормальной формы предиката ограничения области значений.Наконец, рассмотрим отношения, устанавливаемые для ограничения уникальности. Предположим, что в каждой транзакции создается объект типа A, и инициализируется его обязательный атрибут id. Журнал для представления транзакции выглядит следующим образом: T'
T'' = {t1' = new(a1A), t2' = wr(a1.id, id1), t1'' = new(a2A), t2'' = wr(a2.id, id2),…}. Чтобы удовлетворить ограничение уникальности значений атрибута id, в дополнение к отношениям импликации t2' → t1', t2'' → t1'' и предшествования t1' ∠ t2', t1'' ∠ t2'' следует установить отношение исключения t1' ⊕ t2''. Однако такое отношение может оказаться слишком сильным, так как присваиваемые значения идентификаторов могут различаться. Поэтому здесь следует применить нестрогую форму отношения. Заметим, что даже если в дальнейшем на этапе валидации будет обнаружено, что идентификаторы случайно совпали, существует возможность переназначить их с использованием корректирующих методов.Конечно, приведенные примеры не исчерпывают все содержательные случаи семантического анализа транзакций. Тем не менее, они описывают типовые ситуации, возникающие на данном этапе реконсиляции, и иллюстрируют возможности применения формального, основанного на спецификациях прикладной модели данных, подхода. Отметим только, что для определения алгебраических зависимостей между данными и установления соответствующих отношений между операциями транзакций могут быть использованы методы инкрементального анализа и верификации данных [, ].
