home
***
CD-ROM
|
disk
|
FTP
|
other
***
search
/
OS/2 Shareware BBS: 10 Tools
/
10-Tools.zip
/
lclint.zip
/
lclint-2_3h-os2-bin.zip
/
test
/
db1
/
ereftab.lcl
< prev
next >
Wrap
Text File
|
1997-09-03
|
527b
|
32 lines
imports employee, eref;
mutable type ereftab;
ereftab ereftab_create(void)
{
/* ensures result' = empty; */
}
void ereftab_insert(ereftab t, employee e, eref er)
{
/* requires getERef(t^, e) = erefNIL; */
modifies t;
/* ensures t' = add(t^, e, er); */
}
bool ereftab_delete(ereftab t, eref er)
{
modifies t;
/* ensures result = in(t^, er) /\ t' = delete(t^, er); */
}
eref ereftab_lookup(employee e, ereftab t)
{
/* ensures result = getERef(t^, e); */
}
void ereftab_initMod(void)
{
ensures true;
}