Class VIDEO_ACCOUNT

• By Christine Mingins, Yu Liu
• April 1, 2001

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="">