note description: "An electronic health (e-Health) system." author: "Jackie Wang" class interface HEALTH_SYSTEM create make feature -- Constructor make -- Initialize an empty system. ensure patients.is_empty medications.is_empty pr.is_empty di.is_empty dpr.is_empty not warn feature -- State Attributes patients: SET [PATIENT] -- set of patients medications: SET [MEDICATION] -- set of medications pr: REL [PATIENT, MEDICATION] -- prescriptions di: REL [MEDICATION, MEDICATION] -- dangerous interactions dpr: REL [PATIENT, INTERACTION] -- dangerous prescriptions report warn: BOOLEAN -- warning signal for the system supervisor feature -- Commands add_patient (p: PATIENT) -- Add patient 'p' into the system. require p /= Void and then not patients.has (p) ensure patients.count = old patients.count + 1 patients ~ (old patients.deep_twin).extended (p) add_medication (m: MEDICATION) -- Add medication 'm' into the system. require m /= Void and then not medications.has (m) ensure medications.count = old medications.count + 1 medications ~ (old medications.deep_twin).extended (m) add_interaction (m1, m2: MEDICATION) -- Add an interaction between 'm1' and 'm2'. require m1 /= Void and then m2 /= Void m1 /= m2 ensure dangerous_interactions_extended: di ~ (old di.deep_twin).extended (mm ([m1, m2])).extended (mm ([m2, m1])) add_to_prescription (p1: PATIENT; m1: MEDICATION) -- Add a prescription of 'm1' to 'p1'. require p1 /= Void and m1 /= Void ensure interactions_stay_intact: di ~ old di.deep_twin prescriptions_extended: pr ~ (old pr.deep_twin).extended (pm ([p1, m1])) dangerous_prescriptions_report_updated: across patients as patient all across medications as med_1 all across medications as med_2 all dpr.has (pi ([patient.item, med_1.item |-> med_2.item])) = ((old dpr.deep_twin).has (pi ([patient.item, med_1.item |-> med_2.item])) or else (p1 ~ patient.item and across medications as med some di.has (mm ([med.item, m1])) and pr.has (pm ([p1, med.item])) and pr.has (pm ([p1, m1])) and (m1 |-> med.item ~ med_1.item |-> med_2.item or else m1 |-> med.item ~ med_2.item |-> med_1.item) end)) end end end warning_for_supervisor_reset: warn = across (old pr.deep_twin).domain as patient some across (old pr.deep_twin).image (patient.item) as med some di.has (mm ([med.item, m1])) end end or else (old warn) remove_from_prescription (p1: PATIENT; m1: MEDICATION) -- Remove prescription of 'm1' to 'p1'. require p1 /= Void and m1 /= Void ensure prescription_removed: pr ~ (old pr.deep_twin).subtracted (pm ([p1, m1])) dangerous_prescriptions_report_updated: across medications as med all not (dpr.has (pi ([p1, med.item |-> m1])) or else dpr.has (pi ([p1, m1 |-> med.item]))) end invariant symmetry: across medications as m1 all across medications as m2 all di.has (mm ([m1.item, m2.item])) = di.has (mm ([m2.item, m1.item])) end end irreflexivity: across medications as m1 all not di.has (mm ([m1.item, m1.item])) end dangerous_prescriptions_reported: across medications as m1 all across medications as m2 all across patients as p1 all (di.has (mm ([m1.item, m2.item])) and pr.has (pm ([p1.item, m1.item])) and pr.has (pm ([p1.item, m2.item]))) = dpr.image (p1.item).has (m1.item |-> m2.item) end end end end -- class HEALTH_SYSTEM
Generated by ISE EiffelStudio