|
types
Plant :: schedule : Schedule
alarms : set of Alarm
inv mk_Plant(schedule,alarms) ==
forall a in set alarms &
forall per in set dom schedule &
QualificationOK(schedule(per),a.quali,a);
Schedule = map Period to set of Expert
inv schedule == forall exs in set rng schedule & exss <> {};
Period = token;
Expert :: expertid : ExpertId
quali : set of Qualification
inv ex == ex.quali <> {};
ExpertId = token;
Qualification = <Elec> <Mech> | <Bio> | <Chem>;
Alarm :: alarmtext : seq of char
quali : Qualification
functions
NumberOfExperts: Period * Plant -> nat
NumberOfExperts(per,plant) ==
card plant.schedule(per)
pre per in set dom plant.schedule;
ExpertIsOnDuty: Expert * Plant -> set of Period
ExpertIsOnDuty(ex,mk_Plant(sch,-)) ==
{per| per in set dom sch & ex in set sch(per)}
ExpertToPage(a:Alarm,per:Period,plant:Plant) r Expert
pre per in set dom plant.schedule and
a in set plant.alarms
post r in set plant.schedule(per) and
a.quali in set r.qualifi;
QualificationOK: set of Expert * Qualification -> bool
QualificationOK(exs,reqquali) ==
exists ex in set exs reqquali = ex.quali
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.19Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
