ГОСТ Р HCO/HL7 27951— 2016
В.2.31.8 Свойство isOne: BL (нейтральный элемент умножения)
Определение: предикат, указывающий, что данное значение равно числу один, то есть нейтральному эле
менту умножения. Существует ровно одна физическая величина с таким свойством, называемая единицей.
invariant(PQ х, у)
where x.nonNuli.ana(y.nonNuil) 1
х.isOne.and(y.isOne).implies(x.equal
(y>
);
x.isOne.and(y.iaZero>.implies
(x .
equal
(y }
.not
} ;
1;
B.2.31.9 Свойство times: PQ (умножение)
Определение: произведением двух физических величин является произведение их количеств, умноженное
на произведение их единиц.
2
2
invariant(PQ х, у,
2
,
1
, о}
where х.nonNuil.and(y.nonNuil).and(.nonNuil)
.and(o.isZero>.and(i.isOne} (
x.times(o).equal(o
) ;
x.times(i).equal(x);
/ *
нейтральный элемент
*/
x.times(у).times(}.equal(
x.times(y.times(
2
>>;; /♦ ассоциативность */
x.times(у).equal(у.times(x));
/ *
коммутативность
*/
о.lessorEqual(x).and(o.lessorEqual(y).implies(o.lessorEqual(x.times(у»};
B.2.31.10 Свойство inverted: PQ (обратная величина)
Определение: значение типа PQ. которое, будучи умноженным на другое значение типа PQ. дает единицу
(нейтральный элемент умножения). Нуль (нейтральный элемент сложения) не имеет обратной величины. Отноше
ние двух сравнимых величин сравнимо с единицей (единица измерения 1).
invariant(PQ this, that, one}
where this.nonNuil.and(that.nonNuil).and(one.isOne} t
this.times(this.inverted).equal(one);
this.compares(that).implies(this,times(that.invertenj.equal (one))
1;
B.2.31.11 Свойство times: PQ (умножение на вещественное число)
Определение: при умножении на вещественное число образуется масштабированная величина. Эта величи
на сравнима с ее исходной величиной.
Если две величины Q, и 0 2 сравнимы друг с другом, то существует вещественное число г. для которого г1 =
Q ,/Q 2.
invariant(PQх? REAL г}
where х.nonNuil.ana(t.nonNuil) 1
x.times(r).value.equal(x.value.times(r));
x.times(r}.compares(x);
1;
B.2.31.12 Гомоморфизм значения типа REAL в величину типа PQ: REAL
Значение типа REAL может быть преобразовано в значение типа PQ с единицей 1 (один). Аналогично физи
ческая величина, сравнимая с единицей, может быть преобразована в вещественное значение.
invariant(PQ х, unity)
where x.nonNuli.ana.unity.isOne.and(x.compares(unity))
1
unity.times((REAL)x).equal(x>;
);
B.2.31.13 Свойство power: PQ (возведение в степень)
Определение: физическая величина может быть возведена в целую степень.
invariant (PQх, i; INT n. О)
where x.nonNuil.and(i.isOne).and(n.nonNuil.and(o.lsZero) t
369