ГОСТ Р HCO/HL7 27951—2016
В.3.1.6 Свойство union: SET<T>
Определение: свойство, описывающее объединение двух множеств (компонентов множества), при котором
каждый элемент объединения является также элементом как минимум одного компонента объединения.
invariant(SET<T> X, у,
2
»
where х.nonNull.апа(у.nonNull».and(2.nonNull» {
х.union(у>.equal(
2
>.equal(forall(T e» )
2
.contains(e>.equal(x.contains(e>.or(y.contains(e)
»;
1»;
);
B.3.1.7 Свойство union: SET<T>
Определение: свойство, описывающее добавление элемента к множеству.
invariant(SET<T> set, singletonset, T element»
where set.nonKull.and(element.nonNull»
.and(singletonset.cardinality.iaOne;
.and(singletonset.contains(element»>
i
set.union(element).equal(set.union(singleton»»;
1»
B.3.1.8 Свойство except: SET<T>
Определение: свойство, описывающее разность между данным множеством и вычитаемым, содержащую
все элементы данного множества, которые не являются элементами вычитаемого множества.
2
2
invariant(SET<T> х, у,
2
)
where х.nonNull.and(y.nonKull».and( .nonKull) (
x.except(у».equal(2».equal(forall(T e> t
.contains(e).equal(x.contains(e).and(y.contains
(e»
.not));
J»;
T;
B.3.1.9 Свойство except: SET<T>
Определение: свойство, описывающее удаление элемента из данного множества и представляющее собой
множество, состоящее из всех элементов данного множества, кроме удаляемого. Если удаляемый элемент не вхо
дит в данное множество, то результирующим множеством является данное множество.
2
invar 1ant(SET<T> х, г; Т d»
where
2
.nonKull.and(г.nonNull».and(a.nonNull; (
x.except (d».equal( ).equal(forall(T e» (
2
.contains
(e>
.equal
(x .
contains(e).and(d.equal(e>.not>J;
1
»r
T;
B.3.1.10 Свойство intersection: SET<T>
Определение: свойство, описывающее пересечение двух множеств, содержащее те и только те элементы,
которые входят в каждое из этих множеств.
2
invariant(SET<T> х, у,
2
»
where х.nonKull.ana(y.nonNull».and(2.nonNull) (
x.
intersection
( у »
.equal(».equal(forall
(T
e) (
2
.contains(e>.equal(x.contains(e).and(y.contains(e»»»;
»»;
);
B.3.1.11 Литеральная форма
Если элементы типа Т имеют литеральную форму, то множество элементов типа Т имеет литеральную фор
му. в которой элементы множества перечислены внутри фигурных скобок, отделяемые друг от друга точками с
запятой.
SET<T>.literal ST t
SET<T>: "t” elements "1" ( $.equal($2>; »;
384