ГОСТ Р HCO/HL7 27951—2016
invariant(BAG<T> bag!
where bag.nonNull (
bag.lsEmpty.equal(notEmpty.not>;
1;
B.3.5.4 Свойство plus: BAG<T>
Определение: мультимножество, содержащее все элементы операндов-мультимножеств. то есть количество
элементов с каждым значением увеличивается.
invariant(BAG<T> х, у,
t)
where х.nonNul1.ana(у.nonNul1) {
x.plus(y>.equal(z).equal(
forall(T e)
where e.nonNull {
i.
contains(e).equal(x.contains(e>
.plus(y.contains(e)I);
IK-
17
B.3.5.5 Свойство minus: BAG<T>
Определение: мультимножество, содержащее все элементы данного мультимножества (уменьшаемого) за
вычетом элементов другого мультимножества BAG (вычитаемого). Мультимножества не могут иметь дефицит.
Если вьмитаемое содержит больше экземпляров одного и того же значения, то разность содержит нуль экземпля ров
этого значения.
invariant(BAG<T> х, у,
where х.nonNul1.ana(y.nonNull) )
х.minus(y>.equal(z>.equal(
forall(T e>
where e.nonNull )
exists(INT n)
where n.equal
(x .
contains(e).minus(y.contains(e
>)
|
n.nonKegative.equal
(z .
contains(e
));
n.isNegative.equal
(z .
contains(e>.isZerol;
l ;
D7
i;
B.3.5.6 Преобразование значения элемента в мультимножество: BAG<T>
Определение: значение типа Т может быть преобразовано в тривиальное мультимножество, содержащее это
значение как единственный элемент.
invariant(Тх) (
((BAG<T>>х).contains(хI.equal(1);
forall(Т у) (
((BAG<T>>х>.fontains(у>
.implies
(х.
equal(у)) );
i ;
B.3.6 Тип данных IVL (специализация типа данных SET)
Определение: множество последовательных значений упорядоченного базового типа данных.
Любой упорядоченный тип данных может быть базовымдля типа данных IVL; является пи он дискретным или
непрерывным, значения не имеет. Если базовый тип данных упорядочен только частично, то все элементы типа IVL
должны принадлежать полностью упорядоченному подмножеству этого типа данных.
Например, тип данных PQ (физическая величина) считается упорядоченным. Однако он упорядочен только
частично; полная упорядоченность определена только для сопоставимых физических величин (имеющих одну и ту
же размерность). В то время как между 2 и 4 метрами существуют интервалы, нельзя задать интервал между 2
метрами и 4 секундами.
Интервалы являются множествами (тип данных SET) и обладают всеми свойствами множеств. Однако объе
динение и разность интервалов может не быть интервалом, поскольку значения элементов, составляющих резуль тат
этих операций, могут не быть последовательными. Пересечения интервалов всегда являются интервалами.
392