F2 → P2,
...
Fn → Pn )
к теории.
Пример
Для компании Телекоммуникаций связь между деталью и составной_частью, результатом для В1 будет добавление следующих аксиом.
(для всех *)
((для некоторых I) ((производство: составная_часть): J имеет компонент: I )
если
(для некоторых F1 )
((производство: составная_часть): J имеет имя_части_детали: F1 ) ).
(для всех *)
(если (производство: составная_часть): J имеет компонент: I,
(производство: составная_часть): J имеет имя_части_детали: F1
тогда (для некоторых P1 )
( ( производство: деталь ): I имеет имя_детали: P1,
F1 → P1 ) ).
Для компании Телекоммуникаций связь между деталью и изготовленной_деталью, является результатом добавления к В2 следующих аксиом.
(для всех *) ( если существует ( производство: изготовленная_деталь ): I,
(производство: изготовленная_деталь): I имеет
имя_изготовленной_детали: F1,
(производство: деталь ): I имеет имя_детали: P1,
тогда
F1 → P1).
Б.4.2.10 Ограничения в качестве аксиом
Для любого ограничения или определения, которое является that is a закрытым предложением, S, в языке для модели, добавьте правило,
S
к теории.
Б.4.2.11 Различные неделимые константы
Различно названные константы являются различными и неделимыми. Пусть имеется множество констант c1, c2,..., cn.
Для 1≤ i≤n, добавьте правило
неделимый( ci )
к теории.
Для 1≤i <j≤n, добавьте правило
не ci = cj.
к теории.
Б.5 Метамодель IDEF1X
Методика IDEF1X может использоваться непосредственно для описания самой себя. Такая метамодель может использоваться для различных целей, например, для проектирования хранилищ, создания инструментальных средств или для обоснования правильности множества моделей IDEF1X. Модели, построенные с разными целями, могут существенно различаться. Не существует «единственно правильной модели». К примеру, модель для инструментального средства, которое поддерживает инкрементное построение моделей, должна разрешать неполные или даже противоречивые модели. Метамодель, используемая для формализации, уделяет большое внимание согласованию с концепциями формализации. Поэтому неполные или противоречивые модели не предусмотрены.
В метамоделях существуют два важных ограничения. Во-первых, оговорен синтаксис, но не семантика. Во-вторых, метамодель должна дополняться ограничениями естественного или формального языка. Формальная теория стандарта IDEF1X предоставляет как семантику, так и средства для точного выражения необходимых ограничений.
Метамодель для IDEF1X приведена ниже. Имя представления – мм. Также приведены иерархия доменов и ограничений. Ограничения выражены в виде предложений, соответствующих формальной теории метамоделей.
Б.5.1 Диаграмма IDEF1X.
Б.5.2 Домены
Иерархия доменов представлена на диаграмме ниже.
Для базового домена ID нет специального типа данных.
Основные домены типа character (символьные): имя, описание, тип данных, уровень, цель, границы, авторские обозначения, имя 1, имя 2 и правило домена.
Тип данных базового домена Положительное число – numeric (числовой). Правило домена: значение должно быть больше нуля.
Базовые домены типа Boolean (логические) – является: обязательным, тождественным, индивидуальным, общим, зависимым, ненулевым, принадлежащим, перемещаемым. Допустимыми значениями являются «Истина» или «Ложь».
Б.5.3 Ограничения
Правила для создания полноценной модели IDEF1X являются ограничениями метамодели. Ограничения объявлены с использованием языка формальной теории метамоделей. (Ограничения могут быть заметно упрощены с помощью усовершенствования языка).
Б.5.3.1 Ациклическое обобщение
Ни одна категория не может быть обобщением самой себя.
J – родовой родитель категории I, если I находится в кластере K и K является родовым представлением сущности J.
(для всех *)
((мм.категория): I имеет родового родителя: J, если определено:
(мм.категоря): I содержит кластер: K,
(мм.кластер): K имеет род: J).
У категории I есть родовой предок J, если у I есть родовой предок J или у I есть родовой родитель K и у K есть родовой предок J.
(для всех *)
((мм: категория): у I есть родовой предок J, если определено:
(мм: категория): у I есть родовой родитель: J
или
(мм: категория): у I есть родовой родитель: K,
(мм: категория): у K есть родовой предок: J).
Ни одна категория не может быть родовым предком для самой себя.
(для всех *) ( ((мм: категория): у I нет родового предка: I)).
Б.5.3.2 Ациклический тип домена и псевдонимы
Ни один домен не может быть предком для самого себя, где под предком понимается родитель или родитель родителя и тому подобное. Домен I имеет родителя J, если I является псевдонимом домена и J имеет свой истинный домен, или I является типизированным доменом и J является его надтипом.
(для всех *)
((мм: домен): I имеет родителя: J, если определено:
(мм: псевдоним домена): I имеет истинный: J
Или (мм: типизированный домен): I имеет надтип: J).
Домен I имеет предка J, если I имеет родителя J или I имеет родителя K и K имеет предка J.
(для всех *)
((мм: домен): I имеет предка: J, если определено:
(мм: домен): у I есть родитель: J
или
(мм: домен): у I есть родитель: K,
(мм: домен): у K есть предок: J).
Ни один домен не может быть предком для самого себя.
(для всех *) ( ((мм: домен): у I нет предка: I)).
Б.5.3.3 Ациклические псевдонимы сущностей
Ни один псевдоним не может быть предком-псевдонимом для самого себя, где под предком-псевдонимом понимается истинная сущность или истинная сущность истинной сущности и тому подобное.
Домен I имеет предка-псевдонима J, если J является истинной сущностью I или I является К и J является предком-псевдонимом для K.
(для всех *)
((мм: псевдоним сущности): I имеет предка-псевдонима: J, если определено:
(мм: псевдоним сущности): I имеет истинный: J
или
(мм: псевдоним сущности): I имеет истинный: J),
(мм: псевдоним сущности): К имеет предка-псевдонима: J).
Домен I имеет предка J, если I имеет родителя J или I имеет родителя K и K имеет предка J.
(для всех *)
Уважаемый посетитель!
Чтобы распечатать файл, скачайте его (в формате Word).
Ссылка на скачивание - внизу страницы.