employee.lcl

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;
 
uses employeeConstants, sprint(employee, char[]);
 
void employee_sprint(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;
   }