( 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 ] ) ложь.
Уважаемый посетитель!
Чтобы распечатать файл, скачайте его (в формате Word).
Ссылка на скачивание - внизу страницы.