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

B1.2.1. Теория модели IDEF1X

   Модель IDEF1X состоит из одного или нескольких представлений (сущностей, атрибутов, отношений, представленных, например, в виде диаграммы, языка или таблиц) плюс ряд глоссариев с терминами, по крайней мере, для всех сущностей и доменов, используемых (прямо или косвенно) в этих представлениях данных. Процедура формализации формирует соответствующую IDEF1X теорию в логике первого порядка. Логику первого порядка можно считать формальной версией тех аспектов естественного языка, которые используются для описания и обоснования фактов. Отдельные факты передаются с помощью констант,  переменных и функций; связь между фактами передается с помощью предикатов; и утверждения об отношениях фактов передаются с помощью логических связок, таких как «and», «or» или «not», и кванторов «for all» и «for some».

   Теории первого порядка состоит из языка логики первого порядка, в котором константы, функции и предикаты ограничены в рамках определенного словаря, а так же из набора предложений (называемых аксиомами).

   Отправной точкой для теории IDEF1X является логика первого порядка со знаком равенства. Также предполагается наличие словаря и аксиом для теории целых чисел. Дополнительный словарь и аксиомы для IDEF1X основываются на следующих основных идеях:

   Каждый класс сущностей с n количеством атрибутов образует (n+1) предикатов. Предикат связывает экземпляр сущности с представлением атрибута. Если класс сущностей, первый атрибут которого a1 и второй – a2 представляет собой 3-арный предикат p, тогда выражение p(I,A1,A2)означает, что элемент, обозначенный как I, является членом класса сущностей и, как член класса, связывает представление атрибута a1с A1 и a2 с А2. Если A1 (или A2) является нулевым, то у I не имеет представления a1 (или a2).

   Каждое отношения формирует двойной предикат. Предикат связывает (идентифицирует) экземпляр родительской с экземпляром дочерней сущностей. Если отношения выражены бинарным предикатом r, то выражение r(I,J) означает, что (отдельно идентифицированный) I является родительским для J.

  Предикат (exist) определяет, существует ли экземпляр сущности или домена. Отметим, что exist не является экзистенциальным квантором. Exist С: I означает, что С: I является существующим экземпляром класса сущностей (или доменом), где, если С относится к классу сущностей, то I идентифицирует сущность и если С относится к классу доменов, то I является значением представления.  Отметим, для термина С: I просто называет что-то, что может быть экземпляром класса. С: I фактически является существующим экземпляром класса тогда и только тогда, когда exist С: I зарезервировано.

      Предикат (has) определен, что говорит о том, есть ли у экземпляра сущности представление атрибута, однозначно ее идентифицирующего, или она связана с некоторым другим экземпляром сущности. С: I has P: V означает, что экземпляр сущности С: I обладает представлением для свойств P и значение равно V. Свойство, P, может быть атрибутом или свойством, относящимся к атрибуту. Если P является атрибутом, представление V является экземпляром домена. Свойства, относящиеся к атрибутам, возникают из отношений; каждая сущность в отношении обладает свойствами сущности, с которой она связана. Если P является свойством, относящимся к атрибуту,  представление V является идентификатором экземпляра сущности. (has также ограничено определяет домены)  

   Правила (аксиомы для теории), описанные с использованием has и exists, которые ограничивают сущности, домены и предикаты отношений. Основные n-арные и бинарные предикаты прямо не используются. Вместо этого формальное значение конструкций модели IDEF1X выражаются в терминах существующего экземпляра класса сущностей и представления свойств этого экземпляра. Неформально, предложения, описанные с помощью exists и has, могут пониматься, как элементарный язык запросов для типовых экземпляров таблиц.

   То, что разрабатывается в IDEF1X – это факты, представляющие интерес для предприятия, а не просто обозначение фактов и не данные, содержащиеся в них (если только обозначения и информация сами по себе не представляют интерес, например в модели для склада). Таким образом, модель IDEF1X предназначена для создания концептуальной модели фактов, представляющих интерес для предприятия. Эта предметная область (UOD)  является независимой и отражает действительность за пределами любой модели, построенной для этой области. В любой момент времени UOD находится в определенном состоянии, то есть определенный экземпляр сущности обладает определенными свойствами и имеет определенные отношения с другим экземпляром сущности. Для любого состояния UOD некоторые утверждения верны, а не которые не верны. Например, в данном состоянии, утверждение о том, что деталь, названная верхней, имеется в наличии в количестве 17 штук, может быть как правдивым, так и ложным. Точно так же утверждение о том, что у каждого поставщика есть определенный номер поставщика может быть истинным или ложным. Некоторые состояния UOD возможны, а некоторые невозможны. Например, количество деталей, имеющихся в наличии, может равняться 17. Но число имеющихся в наличии деталей не может равняться «вторнику».  Стоит еще раз повторить, что UOD существует и отражает реальность независимо от моделей, в которых она описана. Утверждения о UOD являются истинными или ложными независимо от любой модели, описывающей эту область.

   Модель IDEF1X считается корректной, если она является релевантной предметной области. Корректная модель IDEF1X допускает все возможные состояния UOD и не допускает ложных утверждений, которые находятся в противоречии с истинными утверждениями модели. Другими словами, модель IDEF1X является корректной, если утверждения, которые она содержит, являются истинными (аксиомы) в возможных состояниях UOD и ложными в ее невозможных состояниях. Истинность определяется значениями терминов. Интерпретация терминов присваивается символам, основываясь на теории элементов из UOD.  В частности, интерпретация назначает отношения между предикатами. В результате утверждения теоретически становятся утверждениями о UOD и их истинность определяется согласно реальным фактам UOD. Таким образом, каждое утверждение является истинным или ложным в интерпретации. (Отметим, что термин отношение здесь используется в его математическом значении, обозначая набор n-картежей). Интерпретацию называют моделью теории, если все аксиомы теории истинны в интерпретациях. (Выделенная модель определяет логику использования терминов)