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

( for all X1, X2, ..., Xn )   

( p( X1, X2, ..., Xn ) iff F1 or F2 or ... or Fm ).

Например, положим, что следующие утверждения описывают всё известное о wine и likes.

wine( port ).

wine( burgundy ).

likes( carol, port ).

( for all * ) ( likes( alice, X ) ifdef wine( X ) ).

( for all * ) ( likes( bob, X ) ifdef likes( X, Y ), wine( Y ) ).

Эти записи равносильны обычному описанию.

( for all X1 ) ( wine( X1 ) ifdef X1 = port ).

( for all X1 ) ( wine( X1 ) ifdef X1 = burgundy ).

( for all X1, X2 ) ( likes( X1, X2 ) ifdef X1 = carol, X2 = port ).

( for all X1, X2 ) ( likes( X1, X2 ) ifdef X1 = alice, wine( X2 ) ).

( for all X1, X2 ) ( likes( X1, X2 ) ifdef X1 = bob, 

( for some Y ) ( likes( X2, Y), wine( Y ) ) ).

Последнее предложение распространяет значение на следующую за ней сущность.

Если переменная Y не появляется в свободном виде в G, тогда

( for all Y ) ( if F then G )  

if and only if

if ( for some Y ) ( F ) then G )

Это сложное утверждение ниже показывает, что в любой модели ничего, кроме того, что было описано о wine и likes не может быть правдой. 

( for all X1 ) ( if wine( X1 ) then 

( X1 = port )

or ( X1 = burgundy ) ).

( for all X1, X2 ) ( if likes( X1, X2 ) then

( X1 = carol, X2 = port )

or ( X1 = alice, wine( X2 ) )

or ( X1 = bob, ( for some Y ) ( likes( X2, Y ), wine(Y ) ) ).

likes( bob, alice) and likes( carol, port ) содержатся в любой модели. Без сложного утверждения, likes( carol, burgundy ) и likes( alice, carol ) тоже может.  Без них - нет.


B.2 Создание метода IDEF1X из модели IDEF1X

Модель IDEF1X строится с использованием одного или нескольких представлений (атрибутов, сущностей, связей) в совокупности со словарем определений для всех сущностей и доменов используемых в модели. Процедура формализации создает соответствующую основу логикой первого порядка.

Для упрощения процесса формализации, все альтернативные имена сущностей и доменов заменяются соответствующими реальными названиями. Если необходимо, этот шаг повторяется до полного исчезновения псевдонимов. В результате, формализация проводится в моделях, которые не содержат альтернативные имена.

Взгляд может быть формализован только моделью, в которой содержится только этот взгляд.

Процедура формализации для модели

1.  Включить константы, функции и предикаты общие для всех IDEF1X методов.

2.  Включить аксиомы, общие для всех IDEF1X методов.

3.  Добавить предикаты для всех сущностей и связей.

4.  Добавить словарь, сущности, домены, атрибуты, специфичные связи, неспецифичные связи, первичные и вторичные ключи, внешние ключи и ограничивающие утверждения.

5.  Добавить сложные утверждения для entity, domain, viewEntity, viewEntityAttribute, viewEntityParticipant, exists, has, и isa метода.

6.  Добавить все идентификаторы всех констант, используемых в любом утверждении.

7.   Добавить отдельные константы утверждений.

B.3 Словарь IDEF1X метода

В этой секции константы, функции и предикаты метода IDEF1X описаны вместе с неформальным описанием их особых значений и использования. 

B 3.1 Константы

B.3.1.1 Константы общие для всех методов IDEF1X

Каждый метод IDEF1X включает константы null и [] (означающий постой список).

Константа null означает отсутствие значения. Экземпляр сущности может содержать значение атрибута, а может и не содержать. Значение атрибута “value” null значит, что атрибут не имеет значения для этой сущности. 

B.3.1.2 Константы описанные в IDEF1X модели

Считается, что все константы, которые появляются в любом утверждении метода, находятся в словаре модели.

B.3.2 Идентификаторы

Идентификаторы присваивание имен, конструктор списка и сложение являются общими для всех методов IDEF1X.

B.3.2.1 Присваивание имен

Функция присваивания X: Y использовалась для именования одного объекта другим. Здесь, X и Y – это элементы предметной области. Функция X: Y оценивает другой, отдельный элемент предметной области и аналогична оцениванию 2+3 как 5. (В отличие от функции, где 1+4=5, функция присваивания говорит, что утверждения уникально.) Отметим, что X: Y называют элемент только в смысле описания, не в лексическом смысле. 

В IDEF1X все классы-сущности связаны с представлением. Поэтому, очень удобно называть класс сущности комбинацией представления и сущности. Например, класс-сущность для сущности part представления TcCo production назван как production: part.

Функция присваивания также использовалась для называния экземпляров классов. Например, если production: part это класс и I это экземпляр, тогда ( production: part ): I называет класс, который может быть рассмотрен  как I as a production: part. Такой же экземпляр I так же может быть экземпляром класса production: made_part. Функция присваивания позволяет называть классы действительным образом.   

Другой пример, если qty_on_hand это атрибут и QOH это экземпляр домена, тогда qty_on_hand: QOH  - имя атрибута экземпляра. Это значит, что qty_on_hand атрибут, QOH экземпляр домена и qty_on_hand: QOH – это пересечение, экземпляр домена как атрибут экземпляра. QOH называется значением атрибута экземпляра или просто значением атрибута.

Наконец, если standard_price это домен и 3 – это значение сущности домена, то standard_price: 3 называет экземпляр домена.

B.3.2.2 Конструктор списка

Конструктор списка записывается как [ X | Y ]. В независимой интерпретации [ X |Y ]  - это список с элементом X в начале и хвостом Y и Y сам по себе тоже список. [ X ] можно записать как [ X| [ ] ], а [ X, Y ]  как [ X, [ Y | [ ] ] ]  и так далее.   

B.3.2.3 Сложение

Сложение записывается как X +Y.

B3.3 Предикаты

B.3.3.1 Предикаты, общие для всех методов IDEF1X

Сравнение

Оператор сравнения записывается как X <Y,  X ²Y, и так далее. 

Список

Выражение list( L ) означает, что L - список.

Выражение member( List, Member ) означает, что Member – член списка list List. Например, member( [ 1, 2, 3 ], 2 ) верное утверждение;  member( [ 1, 2, 3 ], 4 ) - ложное.

Выражение count( List, Count ) значит, что список List состоит Count элементов.  Например, count( [ a, b, b ], 3 ) верно.

Выражение nodup( List ) значит, что в списке List нет повторяющихся элементов. Например, nodup( [ 1, 2, 3 ] ) верно. nodup( [ a, b, b ] ) ложь.