-- find a container, returning the identifier of the phase where it is -- to be found. Modify to return an error value if not found. (implicit) -- Exercise is to add another error message for case where -- cid not in set dom db.containers -- Find(db:Tracker, cid:ContainerId) p: PhaseId | -- pre cid in set dom db.containers -- post if exists pid in set dom db.phases & -- cid in set db.phases(pid).contents -- then p in set dom db.phases -- else p = -- Tracker specification for Mapping Chapter -- JSF 2 December 1996 -- -- -- types Tracker :: containers : ContainerInfo phases : PhaseInfo inv mk_Tracker(containers,phases) == Consistent(containers,phases) and PhasesDistinguished(phases) and MaterialSafe(containers,phases); ContainerInfo = map ContainerId to Container; PhaseInfo = map PhaseId to Phase; Container :: fiss_mass : real material : Material; Phase :: contents : set of ContainerId expected_material : Material capacity : nat inv p == card p.contents <= p.capacity; ContainerId = token; PhaseId = token; Material = token functions -- introduce a new container to the plant (map union) Introduce : Tracker * ContainerId * real * Material -> Tracker Introduce(trk, cid, quan, mat) == mk_Tracker(trk.containers munion {cid |-> mk_Container(quan, mat)}, trk.phases) pre cid not in set dom trk.containers; -- permission to move (simple Boolean function) Permission: Tracker * ContainerId * PhaseId -> bool Permission(mk_Tracker(containers, phases), cid, dest) == cid in set dom containers and dest in set dom phases and card phases(dest).contents < phases(dest).capacity and containers(cid).material = phases(dest).expected_material; -- assign a known container to a given phase Assign: Tracker * ContainerId * PhaseId -> Tracker Assign(mk_Tracker(containers, phases), cid, pid) == let pha = mk_Phase(phases(pid).contents union {cid}, phases(pid).expected_material, phases(pid).capacity) in mk_Tracker(containers, phases ++ {pid |-> pha}) pre Permission(mk_Tracker(containers, phases), cid, pid); -- Remove a container from the contents of a phase Remove: Tracker * ContainerId * PhaseId -> Tracker Remove(mk_Tracker(containers, phases), cid, source) == let pha = mk_Phase(phases(source).contents \ {cid}, phases(source).expected_material, phases(source).capacity) in mk_Tracker(containers, phases ++ {source |-> pha}) pre source in set dom phases and cid in set phases(source).contents; -- delete a container from the plant Delete: Tracker * ContainerId * PhaseId -> Tracker Delete(tkr, cid, source) == mk_Tracker({cid} <-: tkr.containers, Remove(tkr, cid, source).phases) pre pre_Remove(tkr,cid,source); -- Auxiliary functions defined for inv-Tracker Consistent: ContainerInfo * PhaseInfo -> bool Consistent(containers, phases) == forall ph in set rng phases & ph.contents subset dom containers; PhasesDistinguished: PhaseInfo -> bool PhasesDistinguished(phases) == not exists p1, p2 in set dom phases & p1 <> p2 and phases(p1).contents = phases(p2).contents; MaterialSafe: ContainerInfo * PhaseInfo -> bool MaterialSafe(containers, phases) == forall ph in set rng phases & forall cid in set ph.contents & cid in set dom containers and containers(cid).material = ph.expected_material