imports employee, empset, <stdio>;

typedef struct{gender g; job j; int l; int h;} db_q;
typedef enum {db_OK, salERR, genderERR, jobERR,
              duplERR, missERR} db_status;
spec immutable type db;
spec db d;

claims UniqueKeys (employee e1, employee e2) db d; 
{	
 /* ensures
     (e1 \in d\any /\ e2 \in d\any  /\ e1.ssNum = e2.ssNum)
       => (e1 = e2);
 */
}	

db_status hire(employee e) db d; 
{
  modifies d;
  /* ensures
     (if result = db_OK
      then d' = hire(e, d^) else d' = d^)
        /\ result =
          (if e.gen = gender_ANY then genderERR
           else if e.j = job_ANY then jobERR
           else if e.salary < 0 then salERR
           else if employed(d^, e.ssNum) then duplERR
           else db_OK);
  */
}

void uncheckedHire(employee e) db d; 
{
  /* requires e.gen \neq gender_ANY /\ e.j \neq job_ANY
            /\ e.salary >= 0 /\ ~employed(d^, e.ssNum);
  */
  modifies d;
  /* ensures d' = hire(e, d^); */
}

bool fire(int ssNum) db d; 
{
  modifies d;
  /* ensures result = employed(d^, ssNum)
       /\ d' = fire(d^, ssNum);
  */
}

int query(db_q q, empset s) db d; 
{
  modifies s;
  /* ensures s' = s^ \U query(d^, q)
       /\ result = size(query(d^, q));
  */
}

bool promote(int ssNum) db d; 
{
  modifies d;
  /* ensures
       result = (employed(d^, ssNum)
                /\ find(d^, ssNum).j = NONMGR)
          /\ (if result then d' = promote(d^, ssNum)
              else d' = d^);
  */
}

db_status setSalary(int ssNum, int sal) db d; 
{
  modifies d;
  /* 
  ensures
      result =
        (if employed(d^, ssNum)
           then (if sal < 0 then salERR else db_OK)
           else missERR)
      /\ (if result = db_OK
            then d' = setSal(d^, ssNum, sal)
            else d' = d^);
  */
}

void db_print(void) db d; FILE *stdout; 
{
  modifies *stdout^;
  /*
  ensures 
    \exists s:ioStream ((*stdout^)' = write((*stdout^)^, s) /\ isSprint(d^, s));
  */
}

void db_initMod(void) db d; 
{
  modifies d;
  /* ensures d' = new; */
}