test/db1/dbase.lcl

   1 imports employee, empset, <stdio>;
   2
   3 typedef struct{gender g; job j; int l; int h;} db_q;
   4 typedef enum {db_OK, salERR, genderERR, jobERR,
   5               duplERR, missERR} db_status;
   6 spec immutable type db;
   7 spec db d;
   8
   9 claims UniqueKeys (employee e1, employee e2) db d;
  10 {
  11  /* ensures
  12      (e1 \in d\any /\ e2 \in d\any  /\ e1.ssNum = e2.ssNum)
  13        => (e1 = e2);
  14  */
  15 }
  16
  17 db_status hire(employee e) db d;
  18 {
  19   modifies d;
  20   /* ensures
  21      (if result = db_OK
  22       then d' = hire(e, d^) else d' = d^)
  23         /\ result =
  24           (if e.gen = gender_ANY then genderERR
  25            else if e.j = job_ANY then jobERR
  26            else if e.salary < 0 then salERR
  27            else if employed(d^, e.ssNum) then duplERR
  28            else db_OK);
  29   */
  30 }
  31
  32 void uncheckedHire(employee e) db d;
  33 {
  34   /* requires e.gen \neq gender_ANY /\ e.j \neq job_ANY
  35             /\ e.salary >= 0 /\ ~employed(d^, e.ssNum);
  36   */
  37   modifies d;
  38   /* ensures d' = hire(e, d^); */
  39 }
  40
  41 bool fire(int ssNum) db d;
  42 {
  43   modifies d;
  44   /* ensures result = employed(d^, ssNum)
  45        /\ d' = fire(d^, ssNum);
  46   */
  47 }
  48
  49 int query(db_q q, empset s) db d;
  50 {
  51   modifies s;
  52   /* ensures s' = s^ \U query(d^, q)
  53        /\ result = size(query(d^, q));
  54   */
  55 }
  56
  57 bool promote(int ssNum) db d;
  58 {
  59   modifies d;
  60   /* ensures
  61        result = (employed(d^, ssNum)
  62                 /\ find(d^, ssNum).j = NONMGR)
  63           /\ (if result then d' = promote(d^, ssNum)
  64               else d' = d^);
  65   */
  66 }
  67
  68 db_status setSalary(int ssNum, int sal) db d;
  69 {
  70   modifies d;
  71   /*
  72   ensures
  73       result =
  74         (if employed(d^, ssNum)
  75            then (if sal < 0 then salERR else db_OK)
  76            else missERR)
  77       /\ (if result = db_OK
  78             then d' = setSal(d^, ssNum, sal)
  79             else d' = d^);
  80   */
  81 }
  82
  83 void db_print(void) db d; FILE *stdout;
  84 {
  85   modifies *stdout^;
  86   /*
  87   ensures
  88     \exists s:ioStream ((*stdout^)' = write((*stdout^)^, s) /\ isSprint(d^, s));
  89   */
  90 }
  91
  92 void db_initMod(void) db d;
  93 {
  94   modifies d;
  95   /* ensures d' = new; */
  96 }