Полнота языка трансформации моделей.
Важным требованием к языку описания трансформаций при его использовании в MDA является универсальность - возможность описать с его помощью любое преобразование из PIM в PSM для любой технологии. Причём необходимо учитывать не только все существующие технологии, но и те, которые будут разработаны в будущем. Это означает, что язык должен позволять задавать любые отображения моделей. Будем считать, что все метамодели связны, то есть любой элемент метамодели достижим из корневого элемента метамодели с помощью навигационных выражений.
Теорема 1. С помощью предложенного языка трансформации можно задать любое однозначное отображение моделей.
Для доказательства нам понадобятся две леммы.
Лемма 1. Для любой конечной модели можно написать правило, которое бы было применимо к ней и не применимо к любой другой модели.
Доказательство.
Применимость правила определяется его секцией выборки. Приведём алгоритм построения нужной нам секции выборки, которая бы соответствовала определённой модели a и не соответствовала никакой другой. Для каждого элемента модели ri из a построим оператор выборки forall ri from model/nav_expression, где nav_expression - навигационное выражение, позволяющее выбрать данный элемент (и все остальные элементы того же типа) в модели. Для каждого атрибута ej со значением fj построим уточняющее выражение where ri/ej=fj. Для каждой относящейся к данному элементу связи sj с кардинальностью 1 добавим уточняющее условие where ri/sj=rk, где rk - элемент модели, на который указывает связь. Для каждой связи sj с кардинальностью больше 1, которая связывает данный элемент с элементами rj1…rjn, добавим уточняющее условие where (rj1 belongsto ri/sj) and … and ( rjn belongsto ri/sj) and ((ri/sj exclude rj1 exclude rj2 … exclude rjn)=null) (если связь sj пуста, то есть n=0, то такое уточняющее условие вырождается в where ri/sj=null). Если создать такие операторы выборки и уточнения для всех элементов модели a, то полученная секция выборки будет удовлетворять необходимым свойствам: она применима к модели a и не применима ни к какой другой.
Лемма 2. Для любой модели можно написать правило, которое бы при выполнении создавало эту модель.
Доказательство этой леммы элементарно. Секция генерации позволяет императивно описывать процесс создания модели элемент за элементом. Поэтому для того, чтобы правило генерировало определённую модель a, следует в секцию генерации добавить операторы создания для каждого элемента модели и инициализировать все атрибуты и ссылки их значениями, взятыми из модели.
Доказательство теоремы 1.
Пусть есть множество исходных моделей A и множество генерируемых моделей B, и отображение U, которое каждой исходной модели ставит в соответствие определённую генерируемую модель. Необходимо доказать, что это отображение можно задать с помощью правил трансформации, то есть что ∃T: ∀ a∈A T(a)=U(a), где Т это описание трансформации, а T(a) - результат применения этой трансформации к модели a из A.
Будем строить это описание трансформации следующим образом. Представим отображение U в виде множества пар вида (,). Для каждой такой пары (a,b) в описание трансформации добавим правило специального вида.
Его секция выборки должна быть применима только на модели a, причём ровно один раз. То, что такая секция выборки возможна, доказано в лемме 1. А для того, чтобы правило никогда не применялось дважды (это могло бы случиться, если модель a обладает симметрией), добавим уточняющее условие вида where rules/rule_name=null, где rule_name - имя данного правила. После первого применения правила соответствующее множество трансформационных связей будет не пусто, а условие - ложно, что гарантированно не допустит повторного применения правила.
Секция генерации этого правила при выполнении должна создавать модель b со всеми содержащимися в ней элементами. Существование такой секции генерации доказано в лемме 2.
Итак, правило такого вида будет порождать модель b, если исходная модель - a, и не будет делать ничего (ни разу не будет применено), если исходная модель отлична от a.
Если создать такие правила для всех пар из исходного отображения U и объединить их в блок трансформации, то полученное описание трансформации T и будет искомым. Порядок следования и выполнения правил в блоке может быть любым. Доказательство того, что T- искомое описание трансформации, элементарно:
Возьмём произвольную модель a из множества исходных моделей, ей однозначно соответствует некоторая модель из множества генерируемых моделей, назовём её b. То есть выполняется U(a)=b. Тогда в описании трансформации T содержится правило t, соответствующее паре моделей (a,b), то есть t(a)=b. Так как отображение U однозначно, никаких других правил, применимых к модели а, в описании T не существует. Тогда T(a)=t(a)=b=U(a). Так как a - произвольная исходная модель, доказано что ∀ a∈A T(a)=U(a), то есть построенное нами описание трансформации T задаёт отображение U.
Доказательство окончено.
Существенным недостатком данной теоремы является то, что не гарантируется конечность описания трансформации, то есть если отображается бесконечное множество моделей, то и количество правил трансформации будет не ограничено. Даже если ограничить максимальное число элементов в модели, описание трансформации всё равно может быть бесконечным. Например, существует бесконечно много моделей, состоящих ровно из одного класса без атрибутов и операций, и различающихся только именами класса. Разумеется, на практике такое описание трансформации, состоящее из бесконечного количества правил, реализовано быть не может. Поэтому необходимо знать условия, при которых бы гарантированно существовало конечное описание трансформации.
Определение. Структурой модели назовём набор её элементов и связей между ними, без учёта значений атрибутов. Будем говорить, что две модели (определённые на общей метамодели) имеют общую структуру, если существует взаимно однозначное соответствие между элементами этих моделей, сохраняющее тип элемента и связи между элементами. На практике это означает, что модели имеют одинаковые элементы и связи между ними, но возможно разные значения атрибутов.
Определение. Будем называть модель конечной, если она состоит из конечного числа элементов метамодели. На практике, очевидно, все модели конечны.
Теорема 2. Пусть существует однозначное отображение U(x) множества исходных моделей A на множество генерируемых моделей B, и пусть все модели конечны. Пусть структура любой генерируемой модели зависит только от структуры исходной модели, но не от значений её атрибутов (то есть для любых исходных моделей a1 и a2 с общей структурой их образы U(a1) и U(a2) так же должны иметь общую структуру). И, наконец, пусть значение любого атрибута генерируемой модели может быть выражено как функция от исходной модели с использованием только алгебраических, строковых и теоретико-множественных операций. Тогда существует конечное описание трансформации T, задающее отображение U, причём это описание трансформации всегда выполнимо за конечное время.
Доказательство.
Множество исходных моделей A разобьём на минимальное число групп так, чтобы все модели внутри группы имели одинаковую структуру (то есть отличались только значениями атрибутов). Число таких групп будет конечно, так как по условию число элементов в любой модели конечно, а из конечного числа элементов можно составить конечное число моделей с различной структурой. Так как структура генерируемой модели зависит только от структуры исходной модели, отображение такой группы оператором U так же будет состоять из моделей с одинаковой структурой. Назовём её структурно однородной группой. Следовательно, отображение U можно представить в виде конечного множества отображений U1…Un, каждое из которых отображает структурно однородную группу моделей в структурно однородную группу. Представим это множество отображений в виде конечного множества пар (a, b=U(a)), где a и b - группы моделей с одинаковой структурой. Так же как и в доказательстве теоремы 1, построим правило трансформации для каждой такой пары.
Секция выборки строится аналогично теореме 1, за исключением того, что не добавляются уточняющие условия на значения атрибутов, так как правило пишется сразу для группы моделей и следовательно эти значения не определены.
В секции генерации, так же как и в доказательстве теоремы 1, явным образом используем операторы создания элемента и установления связей между ними. Так как модели в группе имеют общую структуру, генерация элементов и связей одинакова для всех моделей группы. А вот значения атрибутов для разных моделей могут отличаться, поэтому уже невозможно явно присвоить значения атрибутов. Но по условию теоремы, значение любого атрибута r из генерируемой модели bi∈ b может быть представлено как r=f(ai), где аi∈a, а f() - функция, которая может быть выражена через простейшие операции. Функция f() одна и та же для всех аi∈a. Следовательно, если для каждого атрибута r использовать оператор присваивания r=f(a), можно задать значения атрибутов сразу для всех bi∈b.
Итак, полученное правило t будет применимо ко всем моделям группы a, и ни к каким другим. При этом генерируемая модель всегда будет иметь структуру, соответствующую группе b, а значения атрибутов будут соответствовать отображениям конкретной исходной модели, то есть t(ai)=U(ai). Объединив множество таких правил для всех групп, получим описание трансформации T и ∀ а∈A T(a)=U(a). Число правил в описании трансформации равно числу групп моделей с одинаковой структурой. Так как число групп конечно (при условии что все модели конечны), описание трансформации T конечно. Так как для любой исходной модели при трансформации применяется ровно одно правило и только один раз, порядок применения правил в блоке трансформации T не влияет на результат. То есть мы можем назначить линейный порядок, в таком случае трансформация гарантированно завершится за конечное время. Все утверждения теоремы доказаны.
Замечание: на самом деле не обязательно наличие одной общей функции, выражающей атрибуты. Достаточно, чтобы значение каждого атрибута для всего множества генерируемых моделей задавалось с помощью конечного числа функций, представимых с помощью простейших операций над элементами, связями и значениями атрибутов исходных моделей.
Доказательство аналогично доказательству теоремы 2. Но вместо того, чтобы строить отдельное правило для каждой структурно однородной группы, эти группы следует сначала разбить на подгруппы так, чтобы значения атрибутов всех моделей в подгруппе выражались в виде одинаковых функций. Так как общее число функций, задающих атрибуты, конечно, то и число подгрупп будет конечно. Построив правило трансформации для каждой подгруппы так же, как и в доказательстве теоремы 1, и объединив все эти правила в единый блок трансформации, получим искомое описание трансформации.
Условия теоремы 2 можно смягчить ещё больше, но, к сожалению, невозможно совсем от них избавиться, придя к условиям теоремы 1 и сохранив гарантированную конечность описания трансформации. В частности, если значения атрибутов генерируемой модели не выражаются с помощью элементарных операций, то единственный способ задать такое отображение - перечисление. Если множество возможных значений атрибута бесконечно, то и количество правил трансформации, необходимых для задания такого перечисления, будет бесконечно большим. Однако описания трансформаций для большинства практических задач могут быть успешно заданы с помощью предложенного языка трансформации. Необходимо отметить, что используемый в доказательстве теорем метод построения описаний трансформации не рекомендуется для применения на практике, он крайне громоздок и использован только для формального доказательства полноты языка трансформации.
