imports bool;

constant int maxEmployeeName;
constant int employeePrintSize;

typedef enum { MALE, FEMALE, gender_ANY } gender;
typedef enum { MGR, NONMGR, job_ANY } job;

typedef struct 
{
  int ssNum;
  char name[maxEmployeeName];
  int salary;
  gender gen;
  job j;
} employee;

void employee_sprint (out char s[], employee e) 
{
  /* requires maxIndex(s) >= employeePrintSize; */
  modifies s;
  /* ensures isSprint(s', e)
        /\ lenStr(s') = employeePrintSize;
  */
}

bool employee_equal (employee *e1, employee *e2) 
{
  /* ensures result = sameStr(e1->name^, e2->name^)
           /\ (e1->ssNum^ = e2->ssNum^)
           /\ (e1->salary^ = e2->salary^)
           /\ (e1->gen^ = e2->gen^)
           /\ (e1->j^ = e2->j^);
  */
}

bool employee_setName(employee *e, char na[]) 
{
  /* requires nullTerminated(na^); */
  modifies e->name;
  /* ensures result = lenStr(na^) < maxEmployeeName
           /\ (if result
               then sameStr(e->name', na^)
                     /\ nullTerminated(e->name')
               else e->name' = e->name^);
  */
}

void employee_initMod(void) 
{
  ensures true;
}