| import 'Hospital.ecore' | |
| package hosp | |
| context Hospital | |
| inv maxPatients: self.patients->size() <= self.beds | |
| inv uniquePatientId: self.patients->forAll(p1, p2 | p1 <> p2 implies p1.id <> p2.id) | |
| context Hospital::admitPatient(p:Patient) : | |
| pre: self.beds > 0 | |
| post: self.patients = self.patients@pre->including(p) | |
| endpackage |