ГОСТ Р HCO/HL7 27951— 2016
В.3.2.5 Свойство item: Т
Определение: значением этого свойства является элемент, находящийся в заданной позиции списка (имею
щий заданный индекс). Нулевой индекс задает первый элемент списка (значение свойства head).
invariant(LIS T<T > lis t ; INT index)
where liS t.nonN ull.ana(index.nonN egative) (
l i s t . isE m p ty.im p lie s(1is t . ite m (in d e x ). is N u ll);
1
is t .notE m pty.and(index. isZero)
. im p lie s (lis t.ite m (in d e x ).e q u a l(lis t.h e a d ) >;
list.notE m pty.and(index.nonZ ero)
. im p lie s (1is t.ite m (in d e x ).e q u a l(
l i s t . t a i l . item (m aex.predecessor) ) ) ;
) ;
B.3.2.6 Свойство contains: BL
Определение: предикат, имеющий значение «true», если данный список содержит заданное значение.
invariant(LIS 3V T > l i s t ; Т item )
where lis t.n o n N u ll )
l i s t . is E m p ty .im p lie s (lis t. c o n ta in s (ite m ).n o t);
list.n o n E m pty.a n a (ite m .n o nK u ll) .im p lie s (lis t.c e n tm n s (ite m ).e q u a l(
lis t.h e a d .e q u a l(ite m ).o r(lis t. t a i
1
. c o n ta in s (ite m )) ) ) ;
lis t.n o t E m p ty.a n d (ite m .isN u ll). im p lie s (lis t.c o n ta in s (ite m ).e q u a l(
lis t.h e a d .is K u li.o r ( lis t. ta il.c o n ta in s (ite m )>>;
);
B.3.2.7 Свойство length: INT
Определение: число элементов списка. Пустые элементы включаются в подсчет наравне с обычными эле
ментами списка.
in v a ria n t (LIST<T> lis t )
where x.nonN ull (
l i s t . is E m p ty .e q u a l(lis t.le n g th .is Z e ro );
lis t.n o tE m p ty .e q u a l(lis t. le n g th .e q u a l(
lis t.ta il.le n g th .s u c c e s s o r)>;
);
B.3.2.8 Свойство equal: BL (унаследовано от типа данныхANY)
Два списка равны в том и только том случае, если либо они оба пусты, либо у них одинаковы свойства head
и свойства tail.
invariant (LIST<T> х, у)
where x.nonNull.and(y.nonNuli) I
x.isEmpty.and(y.isEmpty).impiies(x.equal(y));
x.notEmpty.and(y.notEmpt
у
).and(x.head.nonNui
1
)
.im p lie s (x .e q u a l(y > .e q u a l(
x.head.equal(y.head). a n d (x .ta il.e q u a l(y .t a il) > ));
x.notE m pty.ana(y.notE m pty). a n a (x.h e a d .isK u li)
. im p lie s (x .e q u a l(y ).e q u al(
y.heas. is N u ll.a n d (x .ta il.e q u a 1( y . t a il) ) ) ) ;
) ;
B.3.2.9 Литеральная форма
Если элементы типа Т имеют литеральную форму, то список элементов типа Т имеет литеральную форму,
в которой элементы списка пронумерованы и перечисляются внутри крутых скобок, разделяемые точками с за
пятой.
t$.equal($2)? i
($.isEmpty; );
LIST<T>.literal ST {
L2ST<T> :"(" elements
I"(" ">"
LIST<T> elements
387