object SetDB
    components:  Elem*;
    operations: Insert, Delete, Find, EmptyDB;

    (* Note that we do not need full operation signatures, nor
     * equations, since we are now specifying with pre and post-
     * conditions in place of the equations we used above.
     *)

end SetDB;

obj Elem;

operation Insert
    inputs: d:SetDB, e:Elem;
    outputs: d':SetDB;
    precondition: Find(d, e) = false;
    postcondition: d' = d + e;
end Insert;

operation Find
    inputs: d:SetDB, e:Elem;
    outputs: b:boolean;
    precondition: (* An empty precond means true *) ;
    postcondition: b = e in d;
end Find;

operation Delete
    inputs: d:SetDB, e:Elem;
    outputs: d':SetDB;
    precondition: e in d;
    postcondition: d' = d - e;
end Delete;

operation EmptyDB
    inputs: ;
    outputs: d':SetDB;
    precondition: ;
    postcondition: forall (e:Elem) not Find(d', e);
         (* See discussion below about removing this precond. *)
end EmptyDB;