empset.lcl

imports employee;
mutable type empset;
uses Set(employee, empset),
     sprint(empset, char[]);
 
empset empset_create(void) {
   ensures fresh(result) /\ result' = { };
   }
void empset_final(empset s) {
   modifies s;
   ensures trashed(s);
   }
void empset_clear(empset s) {
   modifies s;
   ensures s' = { };
   }
bool empset_insert(empset s, employee e) {
   modifies s;
   ensures result = ~(e \in s^) /\ s' = insert(e, s^);
   }
void empset_insertUnique(empset s, employee e) {
   requires ~(e \in s^);
   modifies s;
   ensures s' = insert(e, s^);
   }
bool empset_delete(empset s, employee e) {
   modifies s;
   ensures result = e \in s^ /\ s' = delete(e, s^);
   }
empset empset_union(empset s1, empset s2) {
   ensures result' = s1^ \U s2^ /\ fresh(result);
   }
empset empset_disjointUnion(empset s1, empset s2) {
   requires s1^ \I s2^ = { };
   ensures result' = s1^ \U s2^ /\ fresh(result);
   }
void empset_intersect(empset s1, empset s2) {
   modifies s1;
   ensures s1' = s1^ \I s2^;
   }
int empset_size(empset s) {
   ensures result = size(s^);
   }
bool empset_member(employee e, empset s) {
   ensures result = e \in s^;
   }
bool empset_subset(empset s1, empset s2) {
   ensures result = s1^ \subseteq s2^;
   }
employee empset_choose(empset s) {
   requires s^ \neq { };
   ensures result \in s^;
   }
char *empset_sprint(empset s) {
    ensures isSprint(result[]', s^) /\ fresh(result[]);
    }
void empset_initMod(void) {
    ensures true;
    }