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