Chapter 3

Airport Class

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 also

Print Friendly

Share this with your friends

Leave a Reply

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