Back - Formal Specification | Next - Filing Subsystem

Tutorial Solutions - Academic Administrator

 

System State Schema

ÚÄModuleÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
reg,ass : STUDENT
maxsize :
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
ass û reg
# reg ó maxsize
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

 

Initial State Schema

ÚÄModuleInitÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
Module
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
reg = í
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

 

Registering a Student

ÚÄRegisterÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
Module
s? : STUDENT
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
s? ç reg
# reg < maxsize
reg' = reg {s?}
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

 

Assessing a Student

ÚÄAssessÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
Module
s? : STUDENT
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
s? î reg
s? ç ass
ass = ass {s?}
reg' = reg
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

 

Monitoring Status

ÚÄEnquireÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
Module
s? : STUDENT
r! : RESPONSE
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
s? ç reg Î r! = not_registered
s? î reg \ ass Î r! = already_registered
s? î ass Î r! = already_assessed
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

 

What's Going On?

The schema records a student's departure from the module. The state of the module changes once a student s? is supplied. The output response is either "Grade" or "No Grade" depending on whether the student has been assessed or not.