employee.lcl

imports <stdio> ;
 
constant size_t maxEmployeeName;
constant int employeePrintSize;
 
typedef enum { MALE, FEMALE, GENDER_UNKNOWN } gender;
typedef enum { MGR, NONMGR, JOB_UNKNOWN } 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, unique 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) internalState;
{
  modifies internalState;
  ensures true;
}