University..

Thought I'd say something about where I'm at with my studies. I've just handed in the Formal methods 2 assignment-it felt like handing over a heavy weight that I'd been carrying around for weeks, what a relief!-and now have another assignment to start, databases, and two exams to look forward to. Here's the sort of thing I did in formal methods 2, a link to this years Database assignment, a link to last years exam for Networks, and last years for Object technology- any tips?! ;-)

MACHINE university
INCLUDES uglobals, students, courses, modules
PROMOTES join, withdraw, enrol, disenrol, suspendstudies, create, provide, shut, add, removereq, getpasses
INVARIANT

/*" Students can only follow created courses:"*/
Followed <: Created &
/*" Only created courses can be completed by students:"*/
Completed <: Created &
/*" Only registered students can enrol on modules:"*/
Enrollees <: Students &
/*" Students can only study modules for which they have passed all the necessary prequisites:"*/
(studies;requires) <: haspassed &
/*" Students can only study modules they need to complete their course:"*/
studies <: (follows;needs) &
/*" Students can only complete courses for which they have passed all the modules needed:"*/
(hascompleted;needs) <: haspassed

OPERATIONS

pass(pp,mm) =
PRE
pp : PERSON & pp : Students &
mm : MODULE &
mm : Modules &
mm : Diet(pp) &
{pp->mm} /\ haspassed = {}
THEN
IF Needed(follows(pp)) - Passes(pp) = {mm} & Diet(pp) - {mm} = {} THEN
finalpass(pp,mm)
ELSE
nonfinalpass(pp,mm)
END
END ;

require(mm,pm) =
PRE
mm : MODULE &
pm: MODULE &
mm : Modules &
pm : Modules &
mm /= pm &
needs~[{mm}] = needs~[{pm}] &
(studies;requires \/ {mm->pm}) <: haspassed &
dom(studies > {mm}) <: dom(haspassed > {pm}) &
cycles(requires \/ {mm->pm}) = {}
& Class(mm) = {}
THEN
Xrequire(mm,pm)
END
END