test/db3/dbase.c

   1 # include <strings.h>
   2 # include "dbase.h"
   3
   4 typedef enum
   5 {
   6   KND_MMGRS, KND_FMGRS, KND_MNON, KND_FNON
   7 } employeeKinds;
   8
   9 /*@constant static employeeKinds firstERC;@*/
  10 # define firstERC KND_MMGRS
  11
  12 /*@constant static employeeKinds lastERC;@*/
  13 # define lastERC KND_FNON
  14
  15 /*@constant static int numERCS;@*/
  16 # define numERCS (/*@+enumint@*/ (lastERC - firstERC + 1) /*@=enumint@*/)
  17
  18 typedef /*@only@*/ erc o_erc;
  19 static o_erc db[numERCS];
  20
  21 /*@iter employeeKinds_all (yield employeeKinds ek); @*/
  22 # define employeeKinds_all(m_ek) \
  23   { employeeKinds m_ek; for (m_ek = firstERC; m_ek <= lastERC; m_ek++) {
  24
  25 # define end_employeeKinds_all }}
  26
  27 static bool initDone = FALSE;
  28
  29 void db_initMod (void)
  30   /*@globals initDone, undef db, internalState@*/
  31   /*@modifies initDone, db, internalState@*/
  32 {
  33   if (initDone)
  34     {
  35       return;
  36     }
  37
  38   bool_initMod ();
  39   employee_initMod ();
  40   eref_initMod ();
  41   erc_initMod ();
  42   empset_initMod ();
  43
  44   employeeKinds_all (ek)
  45     {
  46       db[(int)ek] = erc_create ();
  47     } end_employeeKinds_all ;
  48
  49   initDone = TRUE;
  50 }
  51
  52 static eref db_ercKeyGet(erc c, int key)  /*@*/
  53 {
  54   erc_elements(c, er)
  55     {
  56       if (eref_get(er).ssNum == key)
  57         {
  58           return (er);
  59         }
  60     } end_erc_elements ;
  61
  62   return eref_undefined;
  63 }
  64
  65 static eref db_keyGet (int key) /*@globals db@*/
  66 {
  67   eref er;
  68
  69   employeeKinds_all (ek)
  70     {
  71       er = db_ercKeyGet (db[(int) ek], key);
  72
  73       if (eref_isDefined (er))
  74         {
  75           return er;
  76         }
  77     } end_employeeKinds_all ;
  78
  79   return eref_undefined;
  80 }
  81
  82 static int db_addEmpls (erc c, int l, int h, empset s)
  83   /*@globals internalState@*/
  84   /*@modifies s, internalState@*/
  85 {
  86   employee e;
  87   int numAdded;
  88   numAdded = 0;
  89
  90   erc_elements (c, er)
  91     {
  92       e = eref_get(er);
  93       if ((e.salary >= l) && (e.salary <= h))
  94         {
  95           empset_insert(s, e);
  96           numAdded++;
  97         }
  98     } end_erc_elements ;
  99
 100   return numAdded;
 101 }
 102
 103 db_status db_hire (employee e) /*@globals db@*/
 104 {
 105   if (e.gen == GENDER_UNKNOWN)
 106     {
 107       return DBS_GENDERERR;
 108     }
 109
 110   if (e.j == JOB_UNKNOWN)
 111     {
 112       return DBS_JOBERR;
 113     }
 114
 115   if (e.salary < 0)
 116     {
 117       return DBS_SALERR;
 118     }
 119
 120   if (eref_isDefined (db_keyGet (e.ssNum)))
 121     {
 122       return DBS_DUPLERR;
 123     }
 124
 125   db_uncheckedHire (e);
 126   return DBS_OK;
 127 }
 128
 129 void db_uncheckedHire (employee e)
 130    /*@globals db@*/ /*@modifies db@*/
 131 {
 132   eref er;
 133
 134   er = eref_alloc ();
 135   eref_assign (er, e);
 136
 137   if (e.gen == MALE)
 138     {
 139       if (e.j == MGR)
 140         {
 141           erc_insert (db[(int) KND_MMGRS], er);
 142         }
 143       else
 144         {
 145           erc_insert (db[(int) KND_MNON], er);
 146         }
 147     }
 148   else
 149     {
 150       if (e.j == MGR)
 151         {
 152           erc_insert (db[(int) KND_FMGRS], er);
 153         }
 154       else
 155         {
 156           erc_insert (db[(int) KND_FNON], er);
 157         }
 158     }
 159 }
 160
 161 bool db_fire (int ssNum)
 162   /*@globals db@*/ /*@modifies db@*/
 163 {
 164   employeeKinds_all (ek)
 165     {
 166       erc_elements (db[(int) ek], er)
 167         {
 168           if (eref_get(er).ssNum == ssNum)
 169             {
 170               erc_delete (db[(int) ek], er);
 171               return TRUE;
 172             }
 173         } end_erc_elements ;
 174     } end_employeeKinds_all ;
 175
 176   return FALSE;
 177 }
 178
 179 bool db_promote (int ssNum)
 180   /*@globals db@*/ /*@modifies db@*/
 181 {
 182   eref er;
 183   employee e;
 184   gender g;
 185
 186   g = MALE;
 187   er = db_ercKeyGet (db[(int) KND_MNON], ssNum);
 188
 189   if (!eref_isDefined (er))
 190     {
 191       er = db_ercKeyGet (db[(int) KND_FNON], ssNum);
 192
 193       if (!eref_isDefined (er))
 194         {
 195           return FALSE;
 196         }
 197
 198       g = FEMALE;
 199     }
 200
 201   e = eref_get (er);
 202   e.j = MGR;
 203   eref_assign (er, e);
 204
 205   if (g == MALE)
 206     {
 207       erc_delete (db[(int) KND_MNON], er);
 208       erc_insert (db[(int) KND_MMGRS], er);
 209     }
 210   else
 211     {
 212       erc_delete (db[(int) KND_FNON], er);
 213       erc_insert (db[(int) KND_FMGRS], er);
 214     }
 215
 216   return TRUE;
 217 }
 218
 219 db_status db_setSalary (int ssNum, int sal) /*@globals db@*/
 220 {
 221   eref er;
 222   employee e;
 223
 224   if (sal < 0)
 225     {
 226       return DBS_SALERR;
 227     }
 228
 229   er = db_keyGet (ssNum);
 230
 231   if (!eref_isDefined (er))
 232     {
 233       return DBS_MISSERR;
 234     }
 235
 236   e = eref_get (er);
 237   e.salary = sal;
 238   eref_assign (er, e);
 239
 240   return DBS_OK;
 241 }
 242
 243 int db_query (db_q q, empset s)
 244   /*@globals db@*/
 245 {
 246   int numAdded;
 247   int l, h;
 248
 249   l = q.l;
 250   h = q.h;
 251
 252   switch (q.g)
 253     {
 254     case GENDER_UNKNOWN:
 255       switch (q.j)
 256         {
 257         case JOB_UNKNOWN:
 258           numAdded = 0;
 259
 260           employeeKinds_all (ek)
 261             {
 262               numAdded += db_addEmpls (db[(int) ek], l, h, s);
 263             } end_employeeKinds_all
 264
 265           return numAdded;
 266         case MGR:
 267           numAdded = db_addEmpls (db[(int) KND_MMGRS], l, h, s);
 268           numAdded += db_addEmpls (db[(int) KND_FMGRS], l, h, s);
 269           return numAdded;
 270         case NONMGR:
 271           numAdded = db_addEmpls (db[(int) KND_MNON], l, h, s);
 272           numAdded += db_addEmpls (db[(int) KND_FNON], l, h, s);
 273           return numAdded;
 274         }
 275     case MALE:
 276       switch (q.j)
 277         {
 278         case JOB_UNKNOWN:
 279           numAdded = db_addEmpls (db[(int) KND_MMGRS], l, h, s);
 280           numAdded += db_addEmpls (db[(int) KND_MNON], l, h, s);
 281           return numAdded;
 282         case MGR:
 283           return db_addEmpls (db[(int) KND_MMGRS], l, h, s);
 284         case NONMGR:
 285           return db_addEmpls (db[(int) KND_MNON], l, h, s);
 286         }
 287     case FEMALE:
 288       switch (q.j)
 289         {
 290         case JOB_UNKNOWN:
 291           numAdded = db_addEmpls (db[(int) KND_FMGRS], l, h, s);
 292           numAdded += db_addEmpls (db[(int) KND_FNON], l, h, s);
 293           return numAdded;
 294         case MGR:
 295           return db_addEmpls (db[(int) KND_FMGRS], l, h, s);
 296         case NONMGR:
 297           return db_addEmpls (db[(int) KND_FNON], l, h, s);
 298         }
 299     }
 300 }
 301
 302 void db_print (void)
 303   /*@globals db@*/
 304 {
 305   char *printVal;
 306
 307   printf ("Employees:\n");
 308
 309   employeeKinds_all (ek)
 310     {
 311       printVal = erc_sprint (db[(int) ek]);
 312       printf ("%s", printVal);
 313       free (printVal);
 314     } end_employeeKinds_all ;
 315 }