My Set abstract machine has the following interface:
Set = (
,
,
see above 
see next page 
).
Here are specifications of the actions, insert, delete, card, member, and pick.
1
insert (i: int)/ok()pre true
post
delete(i: int)/ok()
pre true
post
card()/ok(int)
pre true
post
member(i: int)/ok(bool)
pre true
post
pick()/ok(int)
pre
post
