ГОСТ Р ИСО/МЭК ТО 10023-93
Pair: Element. Element2—> Pair
First
: Pair
—> Element
Second
: Pair
—> Element2
-eq,, _ne-: Pair, Pair—> Bool
eqns
forall
el : Element, c2 : E!ement2. p. p1 : Pair
ofsort Element
First (Pair(e 1. e2) —cl:
ofsort Element2
Second(Pair(el, e2))=c2;
ofsort Bool
p= pi = > p eq pi =true;
First (p) ne First (pi) = > p eq pi “ false;
Second(p) ne Second (pi) = > p eq pl=falsfe;
P
ne pl=not(p eq pi);
endtype (*Pair *)
fype ThreeTuple’
is Element, Element2, Element3, Boolean
sorts’
ThreeTuple
opns
Tuple: Element, E!ement2, Eiement3 —>ThreeTuple
First: ThreeTuple— > Element
Second: ThreeTuple—> Element2
Third: ThreeTuple— > Elernenl3
-eq., -ne-. : ThreeTuple.ThreeTuple—> Bool
eqns
forall
x, у : ThreeTuple. xl. yl: Element. x2, y2 : E!ement2,
x3. y3 : Flcmcnt3
ofsort Element
First (Tuple (xl. x2, x3)) - x l ;
ofsort Element2
Second (Tuple (x l, x2, x3)) = x2;
,
ofsort Element3
Third (Tuple (x I, x2, x3))=x3;
ofsort Boot
First (x) eq First (y), Second (x) eq Second (y). Third (x) eq
Third (y) “ > x eq у“ True;
not (First (x) eq First (у)) * > x eq у“ False;
not (Second (x) eq Second (y)) » > x eq y * False;
not (Third (x) eq Third (y)) - > x cq y-False;
20