note
	description: "A Course with its administrative information."
	author: "Jackie Wang"
	date: "$Date$"
	revision: "$Revision$"

class interface
	COURSE

create 
	make

feature -- Attributes

	name: STRING_8

	time: STRING_8
	
feature -- Outputs

	debug_output: STRING_8
			-- String that should be displayed in debugger to represent Current.

	out: STRING_8
			-- New string containing terse printable representation
			-- of current object
	
feature -- Constructor

	make (n: STRING_8; d: INTEGER_32; s1, s2: STRING_8)
		require
				not n.is_empty
				valid_day (d)
				valid_time (s1)
				valid_time (s2)
				course_time (s2) > course_time (s1)
		ensure
				name ~ n
	
feature -- Auxiliary functions for contracts

	valid_day (d: INTEGER_32): BOOLEAN
		ensure
				Result = (1 <= d and then d <= 7)

	valid_time (s: STRING_8): BOOLEAN

	course_time (s: STRING_8): TIME
		require
				valid_time (s)
	
feature -- Equality

	is_equal (other: like Current): BOOLEAN
			-- Is current course equal to 'other'?
	
invariant
	valid_day: valid_day (day)
	finish_later_than_start: finish > start

end -- class COURSE

Generated by ISE EiffelStudio