ГОСТ Р HCO/HL7 27951— 2016
В.2.29.5 Свойство isOne: BL (нейтральный элемент умножения)
Определение: предикат, указывающий, что данное значение является единицей, го есть нейтральным эле
ментом умножения. Этим свойством обладает ровно одно целое значение.
•invariant(REAL х, у(
where х.nonNull.апа(у.nonNull) (
х.isOne.апй(у.isOne).implies(x.equal(y
>>;
x.isOne.ana(y.isZero).implies(x.equal(y).not);
j
;
B.2.29.6 Свойство умножения times: REAL
Определение: операция над множеством значений REAL, формирующая абелеву группу и связанная со сло
жением правилом дистрибутивности.
2
2
invariant(REAL х, у, z, i, о)
where х.nonNull.ana(y.nonNull).and(z.nonNull)
.and(i.isOne».and(o.isZero) t
x.times<o>.equal(o);
x.times(i).equai(x);
I
* neutral element
* /
x.
t
imes(y>.times(}.equal(x.
t
imes
( y . t
imes()>>; /
* associative */
x.times(y>.equal(y.times(x));
t
* commutative
*/
x.times
(y.
plus
(
2
)
).equal(x.times
(y>
.plus(x.times
(z
>);
I
*
distributive
*1
t>.lessorEqual(x).and(o.lessOtEqual(y).implies(o.lessOrEqua1(x.times(y>);
i ;
B.2.29.7 Свойство inverted (обратное значение): REAL
Определение: значение типа REAL, которое при умножении на другое значение типа REAL дает единицу
(нейтральный элемент умножения). Нуль (нейтральный элемент сложения) не имеет обратного значения.
1
invariant(REAL X, i)
where x.isZero.not.and(i.isOne) (
x.times(x.inverted!.equal();
l ;
B.2.29.8 Гомоморфизм типа данных INT в тип данных REAL: INT
Определение: типыданных INT и REAL связаны гомоморфизмом, преобразующим каждое значение типа INT
в значение типа REAL с сохранением алгебраических операций типа данных INT. Это означает, что целое значение
может быть приведено к вещественному, а вещественное может быть понижено до целого числа с помощью окру
гления дробной части.
invariant(INT n, m>
where n.nonNull.ana(m.nonNull) (
((REAL)n.plus(m>.equal (((REAL)n).plus((REAL)m));
((REAL)n.times(m>).equal(((REAL)n).times((REAL)m));
);
B.2.29.9 Свойство возведения в степень power: REAL
Определение: основой возведения в степень является повторение умножения вещественного значения, рас
ширенное до рациональной степени с помощью обратной операции извлечения корня.
Ниже перечислены только некоторые общие свойства возведения в степень.
invariant(REAL х, у, 2, О, i)
where х.nonNull.апа(у.nonNull).and
(z.
nonNull)
.ana(о.isZero).and.(i.isOne) (
forall(INT n)
where n.nonNull (
n.greaterThan(o).implies(
x.power(n).equal(x.times(x.power(n.predecessor)))>;
n.le3sThan(o>.implies(
x.power(n).equal (x.power(n.negated).inverted)
J
363