Комплексное определение для информационного моделирования (IDEF1X), страница 42

Выражение 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 может быть пропущено. Если упомянуто, оно должно быть либо символом, либо числом, либо символом логики.