ГОСТ Р ИСО/МЭК ТО I0023-W
х, у : ThreeTuple
ofsort Bool
First (х) le First (у), Second (x) le Second (y), Third (x)le
Third (y) = > x le y= irue.
not (First (x) le First (y)) - > x le у-false;
not (Second (x) le Second (y)) = > x le у-false;
not (Third (x) le Third (y)) - > x le y-false;
x ne у = > x It y - x le y;
x ge y=y le x;
x ne у = > x gt y - x ge y;
endtype (* POThreeTuple *)
type BasicPOFourTuple
is FourTuple actualizedby POEIement, POElement2, POElemcnt3,
POElement4 using
endtype (* BasicPOFourTuple *)
type POFourTuple
is BasicPOFourTuple
opns
-le_, -It-, _ge_,
-g t- : FourTuple. FourTuple — > Bool
af*
iorall
x, у : FourTuple
ofsort Bool
First (x) ie First (y), Second (x) le Second (y)-. Third (x) le
Third (y), Fourth (x) le Fourth(y) - > x le у-true;
not (First (x) le First (y)) = > x le y—false;
not(Second(x) le.Second(y)) - > x le у-false;
not (Third (x) le Third (y)) —> x le у-false;
not (Fourth (x) le Fourth (y)) = > x ie у—false;
x ne у - > x it y—x le y;
x ge y - y le x;
x ne у = > x gt y - x ge y;
endtype (* POFourTuple *)
Г ______________________________
___________
9 ГЛОБАЛЬНЫЕ ОГРАНИЧЕНИЯ
Определение поведения поставщика услуг разделено на две не
зависимые части: поставщик услуг в режиме-с-установлением-
соединення и поставщик услуг в режиме-без-установления-соедн-
исния. Определение поставщика услуг в режнме-с-установленнем-
соединения представлено в сочетании с отдельными ограничения-
30