note description: "Summary description for {REGISTRATION}." author: "" date: "$Date$" revision: "$Revision$" class REGISTRATION inherit ANY redefine default_create end create default_create feature -- Attributes registrations: REL [STUDENT, COURSE] feature -- Constructor default_create -- Process instances of classes with no creation clause. -- (Default: do nothing.) do create registrations.make_empty end feature -- Queries Max_course_load: INTEGER_32 = 3 feature -- Commands for registrations extend (s: STUDENT; c: COURSE) -- Register student 's' for course 'c'. require not_registered_yet: not registrations.has (pair (s, c)) no_conflicting_registrations: no_conflicts (registrations + pair (s, c)) do registrations.extend (pair (s, c)) ensure registrations ~ old registrations.deep_twin.extended (pair (s, c)) end extend_by_array (a: ARRAY [TUPLE [s: STUDENT; c: COURSE]]) -- Register the list of students and courses. require not_registered_yet: across a as it all not registrations.has (pair (it.item.s, it.item.c)) end no_conflicting_registrations: no_conflicts (registrations.unioned (create {REL [STUDENT, COURSE]}.make_from_tuple_array (a))) do across a as it loop extend (it.item.s, it.item.c) end ensure registrations ~ old registrations.deep_twin.unioned (create {REL [STUDENT, COURSE]}.make_from_tuple_array (a)) end remove (s: STUDENT; c: COURSE) -- Unregister student 's' for course 'c'. require registrations.has (pair (s, c)) do registrations.subtract (pair (s, c)) ensure registrations ~ old registrations.deep_twin.subtracted (pair (s, c)) end feature -- Auxiliary functions conflict (c1, c2: COURSE): BOOLEAN -- Do courses 'c1' and 'c2' conflict with each other? do Result := (c1.day = c2.day) and then ((c1.start ~ c2.start or (c1.start < c2.start and then c1.start + c1.duration >= c2.start) or (c2.start < c1.start and then c2.start + c2.duration >= c1.start))) ensure Result = ((c1.day = c2.day) and ((c1.start ~ c2.start or (c1.start < c2.start and c1.start + c1.duration >= c2.start) or (c2.start < c1.start and c2.start + c2.duration >= c1.start)))) end no_conflicts (regs: REL [STUDENT, COURSE]): BOOLEAN -- ∀ (s1, c1), (s2, c2) ∈ regs : -- c1 ≠ c2 ⋀ s1 = s2 ⇒ ¬(conflict (c1, c2)) local it1, it2: ITERATION_CURSOR [PAIR [STUDENT, COURSE]] c1, c2: COURSE s1, s2: STUDENT do Result := True from it1 := regs.new_cursor until not Result or else it1.after loop from it2 := regs.new_cursor until not Result or else it2.after loop s1 := it1.item.first c1 := it1.item.second s2 := it2.item.first c2 := it2.item.second if c1 /~ c2 and then s1 ~ s2 and then conflict (c1, c2) then Result := False end it2.forth end it1.forth end ensure Result = across regs as r1 all across regs as r2 all r1.item /~ r2.item and r1.item.first ~ r2.item.first implies not (conflict (r1.item.second, r2.item.second)) end end end feature -- Auxiliary functions for contracts pair (s: STUDENT; c: COURSE): PAIR [STUDENT, COURSE] do create Result.make (s, c) end invariant max_course_load: across registrations as r all # registrations.image (r.item.first) <= Max_course_load end no_conflicting_registrations: no_conflicts (registrations) end -- class REGISTRATION
Generated by ISE EiffelStudio