note description: "A Course with its administrative information." author: "Jackie Wang" date: "$Date$" revision: "$Revision$" class COURSE inherit ANY redefine is_equal, out end DEBUG_OUTPUT undefine out, is_equal end create make feature -- Attributes name: STRING_8 time: STRING_8 do Result := day_string + ", " + start.formatted_out (code) + " -- " + finish.formatted_out (code) end feature -- Outputs debug_output: STRING_8 -- String that should be displayed in debugger to represent Current. do Result := out end out: STRING_8 -- New string containing terse printable representation -- of current object do Result := name.out + ":" + day_string + ", " + start.formatted_out (code) + " -- " + finish.formatted_out (code) end 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) do name := n day := d start := course_time (s1) finish := course_time (s2) ensure name ~ n end feature -- Auxiliary functions for contracts valid_day (d: INTEGER_32): BOOLEAN do Result := 1 <= d and then d <= 7 ensure Result = (1 <= d and then d <= 7) end valid_time (s: STRING_8): BOOLEAN local tool: DATE_TIME_CODE_STRING do create tool.make (code) Result := tool.is_time (s) and then tool.correspond (s) end course_time (s: STRING_8): TIME require valid_time (s) do create Result.make_from_string (s + ":00", code + ":ss") end feature {NONE} -- Auxiliary functiosn for implementation code: STRING_8 do Result := "[0]hh:[0]mi" end day_string: STRING_8 local tool: DATE_TIME_TOOLS do create tool Result := tool.Days_text [day + 1 \\ 7] end feature -- Equality is_equal (other: like Current): BOOLEAN -- Is current course equal to 'other'? do Result := name ~ other.name and then start ~ other.start and then duration ~ other.duration end feature {COURSE, REGISTRATION} -- Implementation day: INTEGER_32 -- constrained by an invariant start: TIME finish: TIME duration: TIME_DURATION do Result := finish.relative_duration (start) end invariant valid_day: valid_day (day) finish_later_than_start: finish > start end -- class COURSE
Generated by ISE EiffelStudio