note description: "Summary description for {REGISTRATION}." author: "" date: "$Date$" revision: "$Revision$" class interface REGISTRATION create default_create feature -- Attributes registrations: REL [STUDENT, COURSE] feature -- Constructor default_create -- Process instances of classes with no creation clause. -- (Default: do nothing.) 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)) ensure registrations ~ old registrations.deep_twin.extended (pair (s, c)) 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))) ensure registrations ~ old registrations.deep_twin.unioned (create {REL [STUDENT, COURSE]}.make_from_tuple_array (a)) remove (s: STUDENT; c: COURSE) -- Unregister student 's' for course 'c'. require registrations.has (pair (s, c)) ensure registrations ~ old registrations.deep_twin.subtracted (pair (s, c)) feature -- Auxiliary functions conflict (c1, c2: COURSE): BOOLEAN -- Do courses 'c1' and 'c2' conflict with each other? 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)))) no_conflicts (regs: REL [STUDENT, COURSE]): BOOLEAN -- ∀ (s1, c1), (s2, c2) ∈ regs : -- c1 ≠ c2 ⋀ s1 = s2 ⇒ ¬(conflict (c1, c2)) 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 feature -- Auxiliary functions for contracts pair (s: STUDENT; c: COURSE): PAIR [STUDENT, COURSE] 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