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
/
employee.lcl
< prev
next >
Wrap
Text File
|
1997-09-03
|
1KB
|
52 lines
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;
void employee_sprint (out 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;
}