Requirements for the system

• The whereabouts of people, who work in a building for a particular organisation, need to be monitored for reasons of security.
• The system to do this must be able to identiify who is in the building and who is out of the building, and allow people to check in and check out of the building.
• NewStaff must be able to be added to the system when they join the organisation, and old staff removed when they leave the organisation.
• The system should be capable of being interrogated and be robust enough to deal with invalid data inputs.

Some sample schemas from the specification.

An idea is expressed as a schema which will have a name, declarations and contraints.

ÚÄCheckInÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ œState
³ staff? : STAFF_ID
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ staff? î out
³ in' = in µ {staff?}
³ out' = out \ {staff?}
³ users' = users
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄCheckOutÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ œState
³ staff? : STAFF_ID
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ staff? î in
³ in' = in \ {staff?}
³ out' = out µ {staff?}
³ users' = users
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

[STAFF_ID]

ÚÄStateÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ in,out,users : ˆ STAFF_ID
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ in � out = í
³ in µ out = users
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

Initialise the system.

ÚÄInitStateÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ State
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ in = í
³ out = í
³ users = í
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄœStateÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ State
³ State'
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

N.B. - The above schema is not generally required.

Adding a new staff member to user group, assumed to be outside.

ÚÄAddÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ œState
³ new? : STAFF_ID
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ new? ç users
³ in' = in
³ out' = out µ {new?}
³ user' = users µ {new?}
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

Removing a member of staff

ÚÄRemoveÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ œState
³ staff? : STAFF_ID
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ staff? ç out
³ in' = in
³ out' = out \ {staff?}
³ users' = users \ {staff?}
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

- It is assumed that staff? has first checked out of the building before being removed.

Querying the system

ÚÄQueryForInÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ �State
³ in! : ˆ STAFF_ID
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ in! = in
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄQueryForOutÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ �State
³ out! : ˆ STAFF_ID
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ out! = out
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄQueryForUsersÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ �State
³ users! : ˆ STAFF_ID
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ users! = users
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

Querying a staff identity code

MESSAGE ::= staff_in | staff_out | not_a_user

ÚÄQueryForStaffÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ �State
³ staff? : STAFF_ID
³ output! : MESSAGE
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ staff? î in ΄ output! = staff_in
³ staff? î out ΄ output! = staff_out
³ staff ç users ΄ output! = not_a_user
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

Checking in a member of staff.

ÚÄCheckInÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ œState
³ staff? : STAFF_ID
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ staff? î out
³ in' = in µ {new?}
³ out' = out \ {staff?}
³ users' = users
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

Checking out a member of staff.

ÚÄCheckOutÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ œState
³ staff? : STAFF_ID
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ staff? î in
³ in' = in \ {staff?}
³ out' = out µ {staff?}
³ users' = users
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

Error Handling

REPORT ::= ok | already_user | already_in | not_known | already_out | still_in

ÚÄSuccessÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ result! : REPORT
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ result! = ok
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄAlreadyUserÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ �State
³ new? : STAFF_ID
³ result! : REPORT
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ new? î users
³ result! = already_user
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

RAdd ¡ (Add ™ Success) ˜ AlreadyUser

ÚÄStaffInÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ �State
³ staff? : STAFF_ID
³ result! : REPORT
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ staff? î in
³ result! = already_in
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄNotUserÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ �State
³ staff? : STAFF_ID
³ result! : REPORT
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ staff? î users
³ result! = not_known
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

CheckInError ¡ StaffIn ˜ NotUser

RCheckIn ¡ (CheckIn ™ Success) ˜ CheckInError

ÚÄStaffOutÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ �State
³ staff? : STAFF_ID
³ result! : REPORT
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ staff? î out
³ result! = already_out
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

CheckOutError ¡ StaffOut ˜ NotUser

RCheckOut ¡ (CheckOut ™ Success) ˜ CheckOutError

NotUser has already been defined

The rest of the specification.

ÚÄStillInÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ �State
³ staff? : STAFF_ID
³ result! : REPORT
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ staff? î in
³ result! = still_in
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

RemoveError ¡ StillIn ˜ NotUser

RRemove ¡ (Remove ™ Success) ˜ RemoveError

RQueryForin ¡ QueryForIn ™ Success

RQueryForOut ¡ QueryForOut ™ Success

RQueryForusers ¡ QueryForUsers ™ Success

RQueryForStaff ¡ QueryForStaff ™ Success