Выражение v_e1_n1_n2_e2( I, J ) означает, что идентификатор I выступает предком в отношении J.
Для TcCo отношения между part и structure_item добавляет к словарю бинарный предикат production_part_goes_into_component_structure_item.
B.4 Постулаты метода IDEF1X
B.4.1 Общие постулаты для всех методов IDEF1X
B.4.1.1 Не отрицательные целы числа
Необходимые функции, предикаты и постулаты предполагаются.
B.4.1.2 Списки
Необходимые функции, предикаты и постулаты предполагаются.
B.4.1.3 Равенство
Обыкновенные постулаты равенства транзитивности, антисимметрии и рефлексивности предполагаются.
Обыкновенный предикат и функция постулата замены для каждого предиката и функции предполагаются.
B.4.1.4 Уникальное наименование
Индивидуальные наименование и список терминов обозначают уникальные элементы.
Один элемент не может быть назван двумя разными именами.
( for all * ) ( if X1: X2 = Y1: Y2 then X1 = Y1, X2 = Y2 ).
Список не может быть объектом.
( for all * ) ( not X1: X2 = [ Y1 |Y2 ] ).
B.4.1.5 Атомы
Элемент предметной области – это атом только в том случае, если это не набор имен или конструктор списка.
( atom( X ) iff not X = Y: Z, not X = [ Y | Z ] ).
B.4.1.6 Тождественность сущностей
Для того, чтобы убедиться, что тождественные сущности отличаются от констант, поименованных объектов и списков, добавляется правило
( for all * )
|
( if |
viewEntity( VE ), exists VE: I |
|
|
then |
||
|
atom( I ), not I = null, not I = [ ] ) |
||
|
к методу. |
Для того, чтобы убедиться, что у тождественных экземпляров сущности нет общих предков, нарушающих структуру, добавляется правило
( for all * ) ( if viewEntity( VE1 ),
viewEntity( VE2 ),
not ( for some X ) ( VE1 isa X ),
not ( for some X ) ( VE2 isa X ),
exists VE1: I1,
exists VE2: I2,
not VE1 = VE2
then not I1 = I2 )
к методу. Нарушающие структуру правила применяются ко всем сущностям всех представлений.
B.4.1.7 Доменные ссылки
Говорят, что экземпляр одного домена D:R ссылается на экземпляр другого домена T:R, (D:R→T:R), если либо В это T, либо В – это подтип T. Добавляем постулат
( for all * ) ( D: R → T: R iff
domain( D ),
exists D: R,
( D = T or D isa T or ( for some S ) ( D isa S, S: R → T: R ) ) )
к методу.
B.4.1.8 Значение домена
У домена, описанного, как показано в примере, значение является всего образом. Добавим правило задания значения
( for all * ) ( D: R has value: R ifdef domain( D ), exists D: R )
к методу.
B.4.1.9 Домен атрибута
Для того, чтобы быть уверенными в том, что каждый атрибут принадлежит своему домену, вводят правило
( for all * )
( if viewEntityAttribute(( VE: A ),
VE: I has A: ( D: R )
then exists D: R )
к методу. Отметим, что только не пустые значения атрибутов принадлежат доменам.
B.4.1.10 Наследование классов
Класс наследует свойства своего предка.
( for all * ) ( VE: I has P: DI ifdef
viewEntity( VE ),
exists VE: I,
not viewEntityAttribute( VE: P ),
not viewEntityParticipant( VE: P ),
VE isa VG,
VG: I has P: DI )
Правило наследования применимо ко всем представлениям, сущностям, атрибутам и связям.
B.4.2 Постулаты, описанные методом IDEF1X
B.4.2.1 Глоссарий
В IDEF1X, сущности и домены описаны в глоссарии и графически отображены в представлениях. В таком случае, такие сущности как part могут появиться в разных представлениях и содержать разные наборы атрибутов. Требуется, чтобы в каждом представлении сущность part означала одно и то же. Смысл в том, что part – это класс-сущность part во всех представлениях. В таком случае, классы формируются на основании схожих признаков.
В разделе описаны представления, сущности, домены и соответствующие процедуры создания правил, связанные с глоссарием.
G1. Для каждого представления, v, в наборе представлений, добавляется правило
view( v ).
G2. Для каждой сущности, e, в наборе сущностей, добавляется правило
entity( e ).
G3. Для каждого домена, d, в наборе доменов, добавляется правило
domain( d ).
G4. Для каждого псевдонима, a, для каждой сущности или домена , r, добавляется правило
alias( a, r ).
Example
Для TcCo, правила глоссария могут включать, кроме других, следующие:
view( production )
entity( part )
и
domain( part_name ).
B.4.2.2 Сущность
В IDEF1X у сущности есть атрибуты только в представлении. Представление описывается графически диаграммой, содержащей все сущности представления и все атрибуты в соответствие с представлением. Набор представлений (набор диаграмм) и процедуры создания постулатов для метода соотносятся со специфичными сущностями.
E1. Для каждого представления, v, и для каждой сущности, e, в v, где у e - n атрибутов, в соответствие с v, выполняется следующее.
E1.1. Объявление представления
viewEntity( v: e )
E1.2. Определение соответствующего состояния сущностей
( for all * ) ( exists ( v: e ): I ifdef v_e( I, X1, X2, ..., Xn ) ).
Выражения exists ( v: e ): I и v_e( I, X1, X2, ..., Xn ) означают, что объект, описанный как I – член класса сущностей. Этот постулат в качестве проверки на эквивалентность использует if оператор. Расширенная версия постулата использует only if.
Пример
Для TcCo, при работе с сущностью part
viewEntity( production: part ).
( for all * ) ( exists ( production: part ): I ifdef
production_part( I, X1, X2, X3, X4, X5 ) ).
В этом примере одна и та же сущность – ссылка part связана с production_part. Следующее верно для примера
exists ( production: part ): i1.
exists ( production: part ): i2.
И так далее.
B.4.2.3 Домен
Комбинация домена и представления составляют доменную сущность. Формально, домен рассматривается как элемент предметной области, графически изображенной приложением функции D: R где D – доме, а R – представление. Например, qty_on_hand: 3 – экземпляр сущности домена qty_on_hand. Следующие процедуры связаны с описанием доменов.
Домен-предок
D1. Домен, который не является подтипом любого другого домена, называется предком. Для каждого домена-предка в
( for all * )
( exists d: R ifdef
not R = null,
DataType,
DomainRule )
Поле DataType может быть пропущено. Если упомянуто, оно должно быть либо символом, либо числом, либо символом логики.
Уважаемый посетитель!
Чтобы распечатать файл, скачайте его (в формате Word).
Ссылка на скачивание - внизу страницы.