Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/VDM/VDMSL/TrackerSL/ (Wiener Entwicklungsmethode ^©) Datei vom 13.4.2020 mit Größe 3 kB

SSL tracker.vdmsl Sprache: VDM

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_materials: set1 of 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 in set phases(dest).expected_materials;

-- 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_materials,
                     phases(source).capacity)
  in
    mk_Tracker(containers, phases ++ {source |-> pha})
pre source in set dom phases and
    cid in set phases(source).contents;

-- move a known container between two phases

Move: Tracker * ContainerId * PhaseId * PhaseId -> Tracker
Move(trk, cid, ptoid, pfromid) ==
  let cont = trk.phases(ptoid)
  in
   let pha = mk_Phase(cont.contents union {cid},
                      cont.expected_materials,
                      cont.capacity)
   in
     mk_Tracker(trk.containers,
                Remove(trk,cid,pfromid).phases ++
                {ptoid |-> pha})
pre Permission(trk, cid, ptoid) and
    pre_Remove(trk,cid,pfromid);

-- 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 inter 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 in set ph.expected_materials

quality88%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.