ГОСТ Р HCO/HL7 27951—2016
является целым. Число является целым, если оно всегда является результатом подсмета, обычно представляя по
рядковый номер. В тех возможных сценариях, когда число является результатом оценки или усреднения, оно не
всегда имеет целое значение, и следовательно, необходимо использовать тип данных REAL.
type RealNumber alias
real
specializes QTY ;
literal
REAL negat ed;
REAL times(REAL
REAL inverted;
BLisOne;
REAL power(REAL
ST;
INT precision;
1NT;
REAL (INT x);
PQ;
RTO;
aemotion
promotion
promotion
promotion
Ir
Указанные здесь алгебраические операции определены как характеризующие операции в смысле ИСО
11404 по гой причине, что они необходимы в других частях настоящей спецификации.
В отличие от целых значений семантика вещественных значений не конструируется методом индукции,
а только интуитивно описывается на основе соответствующих аксиом об их алгебраических свойствах. Полно
та аксиоматики намеренно оставлена в стороне, чтобы не делать никаких утверждений об иррациональных
числах.
В.2.29.1 Свойство compares: BL (унаследовано от типа данных QTY)
Множество значений типа REAL является полностью упорядоченным.
invariant (REAL х, у;
where x.nonKull.and(y.nonNull) (
х.compares(у);
11
B.2.29.2 Свойство типа данных разности diffType TYPE (унаследовано от типа данных QTY)
invariant(REAL х) (
x.ditfType.implies(REAL);
};
Тип данных разности (diffType) двух значений типа REAL также является типом данных REAL.
В.2.29.3 Свойство сложения plus: REAL (унаследовано от типа данных QTY)
invariant (REAL х, у, z, о)
where x.nonNull.and(y.nonNuli;.and(z.nonNul
1
>.and(o.asZero) (
x.plus(o).equal(x);
/*
neutral element
*1
x.plus(y).plus(z).equal(x.plus(y.plus(z)));
/*
associative
*/
x.plus(y).equal(y.plus(x>); /* commutative
*/
z.lessOrEqual(x>,and(z.lessOrEqual(y!
.implies(z.lessOrEqual(x.plus(y)>;
x.lessOrEqual(y>.impiies(x.plus(z)
.lessOrEqual(y.plus(z))>;
i ;
B.2.29.4 Свойство negated (обратное значение к сложению): REAL
Определение: элемент, обратный значению типа REAL, то есть такое другое значение типа REAL, которое
при сложении с данным значением дает нулевой результат (нейтральный элемент сложения).
invariant(REAL х>
where x.nonNull {
x.plus(x.negated).iSZero;
i ;
362