Chapter 3

Solution of Patient Register

Copy the code in wordpad and save in rtf extension. Run it on VDM-SL

CODE:
types
Patient=token

values
limit:nat=200;
–DOES NAT INCLUDE ZERO OR NOT? WHY NOT MENTION card(r)>1

state patientRegister of
reg: set of Patient
inv mk_patientRegister(r)==card r<=limit
init mk_patientRegister(r)==r={}
end

operations
addPatient(patientIn:Patient)
ext wr reg:set of Patient
pre (patientIn not in set reg)and (card reg<limit)
post reg=reg~union {patientIn};
–in pre condition, card(reg)<limit, atleast one can be added.. don’t write card(reg)<=limit –in add function
–elemnet is in set or not in set, writing{patientIn} make it a set and member ship –operation checks a member is in a set ,does not check a set is in a set

removePatient(patientOut:Patient)
ext wr reg:set of Patient
pre patientOut in set reg
post reg=reg~\{patientOut};
–elemnet is in set or not in set, writing{patientOut} make it a set and member ship –operation checks a member is in a set ,does not check a set is in a set
–if I write {reg}={reg~}\{patientOut}.. type error.. set minus operation removes no element
–type error; act.. set of set of patients, expected.. set of patients

isRegistered(patientIn:Patient)query:bool
ext rd reg:set of Patient
pre card(reg)<>0
post query<=>patientIn in set reg;
–PRE CONDITION IS DIFFERENT FROM BOOK

getPatients()allPatients:set of Patient
ext rd reg:set of Patient
pre card reg <>0
post allPatients=reg;
–PRE CONDITION IS DIFFERENT FROM BOOK

numberedregistered() number:int
ext rd reg:set of Patient
pre true
post number=card reg;

Solution of Airport Class

CODE

types
Aircraft=token

state Airport of
permission:set of Aircraft
landed:set of Aircraft
inv mk_Airport(p,l)==l subset p
–subset deals with equal sets, proper subset can not. At a time p and l both can be empty as –all with permit may have landed also
init mk_Airport(p,l)==p={}and l={}
end

operations
givepermission(craftIn:Aircraft)
ext wr permission:set of Aircraft
pre craftIn not in set permission
post permission=permission~ union {craftIn};

recordLanding(craftIn:Aircraft)
ext wr landed:set of Aircraft
rd permission:set of Aircraft
pre craftIn in set permission and craftIn not in set landed
post landed=landed~ union {craftIn};

recordTakesOff(craftIn:Aircraft)
ext wr permission:set of Aircraft
wr landed:set of Aircraft
pre craftIn in set permission and craftIn in set landed
post permission=permission~ \ {craftIn} and landed=landed~ \ {craftIn};
–PERMISSION IS INCLUDED IN PRE CONDITION

getPermission()permittedCraft:set of Aircraft
ext rd permission:set of Aircraft
pre true
post permittedCraft=permission;
–PRE CONDITION; PERMISSION IS NOT EMPTY

getLanded()landedCraft:set of Aircraft
ext rd landed:set of Aircraft
pre true
post landedCraft=landed;
–PRE CONDITION; LANDED IS NOT EMPTY

numberWaiting()inPermission:nat
ext rd permission:set of Aircraft
rd landed:set of Aircraft
pre true
post inPermission=card(permission\landed);
–Pre is true; permission can be empty

 

Print Friendly

Share this with your friends

Leave a Reply

Your email address will not be published. Required fields are marked *