test/db3/employee.lcl

   1 imports <stdio> ;
   2
   3 constant size_t maxEmployeeName;
   4 constant int employeePrintSize;
   5
   6 typedef enum { MALE, FEMALE, GENDER_UNKNOWN } gender;
   7 typedef enum { MGR, NONMGR, JOB_UNKNOWN } job;
   8
   9 typedef struct
  10 {
  11   int ssNum;
  12   char name[maxEmployeeName];
  13   int salary;
  14   gender gen;
  15   job j;
  16 } employee;
  17
  18 void employee_sprint (out char s[], employee e)
  19 {
  20   /* requires maxIndex(s) >= employeePrintSize; */
  21   modifies s;
  22   /* ensures isSprint(s', e)
  23         /\ lenStr(s') = employeePrintSize;
  24   */
  25 }
  26
  27 bool employee_equal (employee *e1, employee *e2)
  28 {
  29   /* ensures result = sameStr(e1->name^, e2->name^)
  30            /\ (e1->ssNum^ = e2->ssNum^)
  31            /\ (e1->salary^ = e2->salary^)
  32            /\ (e1->gen^ = e2->gen^)
  33            /\ (e1->j^ = e2->j^);
  34   */
  35 }
  36
  37 bool employee_setName (employee *e, unique char na[])
  38 {
  39   /* requires nullTerminated(na^); */
  40   modifies e->name;
  41   /* ensures result = lenStr(na^) < maxEmployeeName
  42            /\ (if result
  43                then sameStr(e->name', na^)
  44                      /\ nullTerminated(e->name')
  45                else e->name' = e->name^);
  46   */
  47 }
  48
  49 void employee_initMod(void) internalState;
  50 {
  51   modifies internalState;
  52   ensures true;
  53 }
  54