Correspondence
stack -> bag
%a(<
>) =
<< mk_set( items ), limit >>
where
mk_set(
\
%e
) = \0
mk_set( e \. s ) = mk_set(s) \uplus { e }
%r( push ) = put
,
%r( pop ) = get
%x(s.settop(i))
=
s.pop(); s.push(i);
slide
:
Behavioral subtypes -- correspondence
