ГОСТ Р HCO/HL7 27951— 2016
literal
1;
BL isNegative;
BL nonNegative;
INT divinersBy(INT x!;
INT remainder(INT x|;
BL isOne;
ST;
Так как тип данных IntegerNumber имеет всю семантику математического понятия целого числа, то определе
ны базовые операции plus (сложение) и times (умножение). Эти операции определены здесь как характеризующие
операции в смысле ИСО 11404 по той причине, что они необходимы в других частях настоящей спецификации,
а именно для определения семантики литеральной формы.
Традиционное рекурсивное определение сложения и умножения восходит к Грассману и использует понятие
«следующее» (successor)’К
invariant(INT х, о, i|
where х.nonNull.and(о.isZero! (
x.lessThan(x.successorI;
x.plus(o>.equa!(x>;
x .p lu s (y .s u c c e s s o r|.e q u a l(x .p lu s (y >.successor!;
x.tim e s (o !.e q u a l(o > ;
x.times(y.successor!.equal(x.times(y|>.plus(x|;
);
B.2.28.1 Свойство successor: INT (следующее)
Определение: следующим называется такое значение типа INT, большее данного значения типа INT.
для которого не существует никакого значения типа INT. находящегося между данным и следующим значе
нием.
invariant (INT х, у!
where
х .
successor
(у! (
x.lessThan
( y j
.and.not(exists(INT
2
! |
x.lessThan(at>;
2
.lessThan(y>;
1);
B.2.28.2 Свойство типа данных разности diffType: TYPE (унаследовано от типа данных QTY)
mvariant(INT х!
1
х.diffType.implies(INT>;
I;
Тип данных разности (diffType) двух значений типа INT также является типом данных INT.
В.2.28.3 Свойство сложения plus: INT (унаследовано от типа данных QTY)
invariant(INT х, у, о!
where х.nonNull.ana(у.nonNull!.ana(о.isZero! t
x.plus(o>.equal(xj;
x.plus
(y .
successor!.equal(x.plus
(y !
.successor!;
B.2.28.4 Свойство умножения times: INT
Определение: результат умножения данного целого значения на операнд, эквивалентный повторениям сло
жения этого значения.
Н. Grassman. Lehrbuch der Arithmetik. 1861. Исходным аксиомам, предложенным Грассманом, отдается
предпочтение перед аксиомами Пвано. поскольку аксиомы Грассмана охватывают все целые числа, а не только
натуральные. Также «довольно хорошо известно, что. по собственному признанию Пеано. он позаимствовал свои
аксиомы у Дедекинда и при их разработке существенно использовал труды Грассмана» (Нао Wang. The Axiomati-
zation ofArithmetic. J. Symb. Logic: 1957:22(2): p. 145).
359