Back -
Formal Specification | Next - Filing SubsystemTutorial 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.