From UML to Design by Contract
Christine Mingins and Yu Liu
Listing 1.

		--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.
		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

Yu Liu is with CRC for Enterprise Distributed Systems Technology, Australia and can be contacted at


Sign up for our newsletter.

Terms and Privacy Policy consent

I agree to this site's Privacy Policy.

Upcoming Events