ГОСТ Р 56271-2014
hasR(x.y) -» (А(х) v В(х)).
Множество допустимых значений атрибута представляется на языке ИСО 15926-2 путем за
дания ограничения на диапазон бинарного предиката, представляющего рассматриваемый атрибут. В
языке EXPRESS значения атрибутов всегда ограничиваются по отношению к данному типу сущ ности.
Указанные ограничения представляются локальными ограничениями диапазонов на языке ИСО
15926-2. Это означает, что ограничение диапазона всегда включает ограничение области бинар ного
предиката.
Предположим, что г — это атрибут, значения которого ограничены типом сущности f для типа
сущности а и типом сущности g для типа сущности Ь. Тогда на языке ИСО 15926-2 это записывается
следующим образом:
А(х)
a
hasR(x.y) -» F(y)
В(х) л hasR(x.y) -» G(y)
Каждый атрибут практической реализации EXPRESS ИСО 15926-2 имеет ограничение карди
нального числа: [0.1] или [1.1]. Ограничения кардинального числа для атрибутов задаются на каж
дый тип сущности как для ограничений диапазона. Ограничения кардинального числа на бинарные
предикаты представляются с помощью двух аксиом. Предположим, что атрибут г имеет ограничение
кардинального числа [1,1] для типа сущности а. На языке ИСО 15926-2 это записывается как пара
аксиом:
А(х) -» Hy(hasR(x.y))(1)
А(х)
a
hasR(x.y) л hasR(x.z) -» у = z(2)
Формула (1) представляет собой ограничение кардинального числа [1,*). Вторая аксиома пред
ставляет собой ограничение кардинального числа [0.1]. Вместе они выражают ограничение кардиналь
ного числа [1.1]. Ограничение кардинального числа [0,1] представляется только формулой (2).
Если атрибут ограничен правилом UNIQUE языка EXPRESS, то на языке ИСО 15926-2 это пред
ставляется путем задания требования, что предикат — это обратный функционал. Если атрибут г удов
летворяет требованию UNIQUE для типа сущности А. то:
А(х) л А(у) л hasR(x.z)
л
hasR(y.z) -> х = у.
Множество аксиом языка ИСО 15926-2 перечислено в приложении В.
При м е ча н и е 3 - С помощью блока проверки логики первого порядка FOL доказано, что рассматривае
мое множество аксиом логически непротиворечиво.
4.2 Определение логического шаблона
Настоящий раздел определяет логические шаблоны. Данные шаблоны, в соответствии с разде
лом 5. дополнительно имеют подписи. В настоящем стандарте этот вопрос не рассматривается.
Для формулы I
q
первого порядка, использующей названия предикатов аксиоматики языка
ИСО 15926-2 для базового языка, определением логического шаблона для £ является формула логики
первого порядка:
Л/(х.у,...)О
где N г I — символ предиката, называемого именем шаблона, х.у,... набор переменных, называемых
формальными аргументами. <р— формула типа «л - v - 3» над символами в £. содержащая только
формальные аргументы х.у.... как свободные переменные (тело шаблона).
Множество TS (£0). состоящее из множеств логических шаблонов над £0. индуктивно определяет
ся как наименьшее множество. В этом случае:
- 0 € TS (£о) — множество логических шаблонов над £0;
- если S
е
TS (£0) — множество логических шаблонов над £0 и d — определение логического
шаблона надnames(S), то S u ( d } e rS(£0) — также множество логических шаблонов над £0. где
names(S): = [N | v>е S) — это множество названий шаблонов, определенных в S.
При м е ча н и е - Интуитивное представление о рассматриваемом множестве шаблонов: чтобы гаранти
ровать. что расширение шаблона заканчивается, нужно запретить множества циклических определений шаблонов
(например, если шаблон расширяется до формулы, содержащей шаблон в, который, всвою очередь, расширяется
до формулы, содержащей шаблон А). Наше определение гарантирует, что определение шаблонаможет
только быть добавлено к множеству шаблонов, если все шаблоны, поименованные в
<р.
были предварительно
определены без ссылок на N.
7