Class VIDEO_ACCOUNT
From UML to Design by Contract
Christine Mingins and Yu Liu
Listing 1.
Class VIDEO_ACCOUNT
--Maintains a record of videos hired and payments made.
feature -Access
account_owner: STRING
--Owner of this Video Account.
videos_hired: SET[VIDEO]
--What videos are currently on hire for this account?
video_hire_limit: INTEGER
--How many videos can be hired out at one time?
account_balance: INTEGER
--What is the balance of the current account?
store: STORE
--Which store is this account registered to?
feature -Basic Operations
release (video: VIDEO)
--Release video to the customer.
require
video_exists: video /= Void-Checks that the argument is valid.
video_in_stock: store.stock.has(video)
video_available: video.available
under_hire_limit: videos_hired.count < video_hire_limit="" not_already_hired:="" not="" videos_hired.has(video)="" ensure="" still_in_stock:="" store.stock.has(video)="" video_hired:="" not="" available_videos.has(video)="" video_released:="" videos_hired.has(video)="" videos_up:="" videos_hired.count="old" videos_hired.count="" +="" 1="" renew="" (video:="" video)="" --renew="" video="" hire="" if="" not="" reserved="" by="" another="" customer.="" require="" video_exists:="" video="" void="" video_not_available:="" not="" video.available="" video_hired:="" videos_hired.has(video)="" video_not_available:="" not="" video.available="" video_not_reserved:="" not="" video.reserved="" ensure="" video_not_available:="" not="" video.available="" video_hired:="" videos_hired.has(video)="" same_video_count:="" videos_hired.count="old" videos_hired.count="" invariant="" video_count_positive:="" videos_hired="">= 0
hire_within_limits: video_count <= max_video_hire="" hired_videos_in_pool:="" store.stock.is_subset(videos_hired)="" end--class="" video_account="">=>
About the Authors
Christine Mingins is with the School of Computer Science and Software Engineering, Monash University, Australia and can be contacted at [email protected].
Yu Liu is with CRC for Enterprise Distributed Systems Technology, Australia and can be contacted at [email protected].