Student.ocl

~~~~~
package Student
context Name
inv: (Student.allInstances()->select(v0 | v0.name->includes(self))->size() <= 1)
context Lab
inv: (Course.allInstances()->select(v2 | v2.labs->includes(self))->size() <= 1)
context Student
inv: (not Course.allInstances()->forAll(v4 | (self.current->includes(v4) implies self.approved->includes(v4))))
context Student
inv: Course.allInstances()->forAll(c | (self.approved->includes(c) implies (Lab.allInstances()->forAll(v9 | (c.labs->includes(v9) implies self.donelabs->includes(v9))) and Grade.allInstances()->forAll(v13 | (self.exams[c]->includes(v13) implies ((((v13 = Grade::A) or (v13 = Grade::B)) or (v13 = Grade::C)) or (v13 = Grade::D)))))))
context Student
inv: Course.allInstances()->forAll(v19 | (((self.current->includes(v19) or self.approved->includes(v19)) or Grade.allInstances()->exists(v24 | self.exams[v19]->includes(v24))) implies College.allInstances()->exists(v27 | (v27.students->includes(self) and v27.courses->includes(v19)))))
context Student
inv: (College.allInstances()->select(v30 | v30.students->includes(self))->size() = 1)
context College::newstudent(s:Student)
pre: (College.allInstances()->select(v33 | v33.students->includes(s))->size() = 0)
pre: (s.approved->size() = 0)
pre: (s.current->size() = 0)
pre: (s.donelabs->size() = 0)
pre: (Course.allInstances()->collect(v45 | s.exams[v45]->size())->sum() = 0)
post: (College.allInstances()->forAll(v50 | Student.allInstances()->forAll(v51 | (v50.students->includes(v51) implies (v50.students@pre->includes(v51) or ((v50 = self) and (v51 = s)))))) and College.allInstances()->forAll(v54 | Student.allInstances()->forAll(v55 | ((v54.students@pre->includes(v55) or ((v54 = self) and (v55 = s))) implies v54.students->includes(v55)))))
context Student::enroll(c:Course)
pre: (self.current->size() = 0)
pre: (not self.approved->includes(c))
post: (Student.allInstances()->forAll(v64 | Course.allInstances()->forAll(v65 | (v64.current->includes(v65) implies (v64.current@pre->includes(v65) or ((v64 = self) and (v65 = c)))))) and Student.allInstances()->forAll(v68 | Course.allInstances()->forAll(v69 | ((v68.current@pre->includes(v69) or ((v68 = self) and (v69 = c))) implies v68.current->includes(v69)))))
context Student::lab(l:Lab)
pre: (self.current->size() >= 1)
pre: (not self.donelabs->includes(l))
pre: Course.allInstances()->exists(v79 | (self.current->includes(v79) and v79.labs->includes(l)))
post: (Student.allInstances()->forAll(v82 | Lab.allInstances()->forAll(v83 | (v82.donelabs->includes(v83) implies (v82.donelabs@pre->includes(v83) or ((v82 = self) and (v83 = l)))))) and Student.allInstances()->forAll(v86 | Lab.allInstances()->forAll(v87 | ((v86.donelabs@pre->includes(v87) or ((v86 = self) and (v87 = l))) implies v86.donelabs->includes(v87)))))
context Student::exam(g:Grade)
pre: (self.current->size() >= 1)
pre: (not Course.allInstances()->forAll(v93 | (self.current->includes(v93) implies Grade.allInstances()->exists(v96 | self.exams[v93]->includes(v96)))))
post: (Student.allInstances()->forAll(v99 | Course.allInstances()->forAll(v100 | Grade.allInstances()->forAll(v101 | (v99.exams[v100]->includes(v101) implies (v99.exams@pre[v100]->includes(v101) or ((v99 = self) and (self.current@pre->includes(v100) and (v101 = g)))))))) and Student.allInstances()->forAll(v106 | Course.allInstances()->forAll(v107 | Grade.allInstances()->forAll(v108 | ((v106.exams@pre[v107]->includes(v108) or ((v106 = self) and (self.current@pre->includes(v107) and (v108 = g)))) implies v106.exams[v107]->includes(v108))))))
context Student::approve()
pre: (self.current->size() >= 1)
pre: Grade.allInstances()->forAll(v116 | (Course.allInstances()->exists(v117 | (self.current->includes(v117) and self.exams[v117]->includes(v116))) implies ((((v116 = Grade::A) or (v116 = Grade::B)) or (v116 = Grade::C)) or (v116 = Grade::D))))
pre: Lab.allInstances()->forAll(v122 | (Course.allInstances()->exists(v123 | (self.current->includes(v123) and v123.labs->includes(v122))) implies self.donelabs->includes(v122)))
post: (Student.allInstances()->forAll(v128 | Course.allInstances()->forAll(v129 | (v128.approved->includes(v129) implies (v128.approved@pre->includes(v129) or ((v128 = self) and self.current@pre->includes(v129)))))) and Student.allInstances()->forAll(v134 | Course.allInstances()->forAll(v135 | ((v134.approved@pre->includes(v135) or ((v134 = self) and self.current@pre->includes(v135))) implies v134.approved->includes(v135)))))
post: (Student.allInstances()->forAll(v140 | Course.allInstances()->forAll(v141 | (v140.current->includes(v141) implies (v140.current@pre->includes(v141) and (not (v140 = self)))))) and Student.allInstances()->forAll(v144 | Course.allInstances()->forAll(v145 | ((v144.current@pre->includes(v145) and (not (v144 = self))) implies v144.current->includes(v145)))))
context Student::quit()
pre: (self.current->size() >= 1)
post: (Student.allInstances()->forAll(v151 | Course.allInstances()->forAll(v152 | Grade.allInstances()->forAll(v153 | (v151.exams[v152]->includes(v153) implies (v151.exams@pre[v152]->includes(v153) and (not ((v151 = self) and self.current@pre->includes(v152)))))))) and Student.allInstances()->forAll(v158 | Course.allInstances()->forAll(v159 | Grade.allInstances()->forAll(v160 | ((v158.exams@pre[v159]->includes(v160) and (not ((v158 = self) and self.current@pre->includes(v159)))) implies v158.exams[v159]->includes(v160))))))
post: (Student.allInstances()->forAll(v165 | Lab.allInstances()->forAll(v166 | (v165.donelabs->includes(v166) implies (v165.donelabs@pre->includes(v166) and (not ((v165 = self) and Course.allInstances()->exists(v169 | (self.current@pre->includes(v169) and v169.labs->includes(v166))))))))) and Student.allInstances()->forAll(v172 | Lab.allInstances()->forAll(v173 | ((v172.donelabs@pre->includes(v173) and (not ((v172 = self) and Course.allInstances()->exists(v175 | (self.current@pre->includes(v175) and v175.labs->includes(v173)))))) implies v172.donelabs->includes(v173)))))
post: (Student.allInstances()->forAll(v179 | Course.allInstances()->forAll(v180 | (v179.current->includes(v180) implies (v179.current@pre->includes(v180) and (not (v179 = self)))))) and Student.allInstances()->forAll(v183 | Course.allInstances()->forAll(v184 | ((v183.current@pre->includes(v184) and (not (v183 = self))) implies v183.current->includes(v184)))))
endpackage
~~~~~~