\begin{vdm_al}
types
BOM = map Pn to set of Pn
inv bom ==
(forall ps in set rng bom & ps subset dom bom) and
(forall p in set dom bom & p not in set Parts(p, bom));
Pn = nat
values
bom = {1 |-> {2,4}, 2 |-> {3,4,5}, 3 |-> {5,6}, 4 |-> {6},
5 |-> {4}, 6 |-> {}};
cycle = {1 |-> {2,4}, 2 |-> {3,4,5}, 3 |-> {5,6}, 4 |-> {6},
5 |-> {4}, 6 |-> {1}};
functions
Parts: Pn * map Pn to set of Pn -> set of Pn
Parts(p, bom) ==
TransClos(bom, bom(p))
pre p in set dom bom;
TransClos: (map Pn to set of Pn) * set of Pn -> set of Pn
TransClos(bom, ps) ==
if forall p in set ps & bom(p) subset ps
then ps
else let newps = dunion { bom(p) | p in set ps}
in
TransClos(bom, ps union newps)
pre ps subset dom bom
measure IncrAcc;
IncrAcc: (map Pn to set of Pn) * set of Pn -> nat
IncrAcc(bom,pns) ==
card dom bom - card pns;
Explode: Pn * BOM -> set of Pn
Explode(p, bom) ==
bom(p) union Exps(bom, bom(p))
pre p in set dom bom;
Exps: BOM * set of Pn -> set of Pn
Exps(bom, ps) ==
if ps = {}
then {}
else let p1 in set ps
in
Explode(p1, bom) union Exps(bom, ps \ {p1})
pre ps subset dom bom;
Enter: BOM * Pn * set of Pn -> BOM
Enter(bom, p, ps) ==
bom munion { p |-> ps }
pre (p not in set dom bom) and (ps subset dom bom);
Delete: Pn * BOM -> BOM
Delete(p, bom) ==
{p} <-: bom
pre (p in set dom bom) and (inv_BOM({p} <-: bom));
Add: Pn * Pn * BOM -> BOM
Add(p1, p2, bom) ==
bom ++ {p1 |-> bom(p1) union {p2} }
pre (p1 in set dom bom) and (p2 in set dom bom) and
(p2 not in set bom(p1)) and (p1 not in set Explode(p2,bom));
Erase: Pn * Pn * BOM -> BOM
Erase(p1, p2, bom) ==
bom ++ { p1 |-> bom(p1) \ {p2} }
pre (p1 in set dom bom) and (p2 in set dom bom) and
(p2 in set bom(p1))
\end{vdm_al}
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
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.
Die farbliche Syntaxdarstellung ist noch experimentell.
Die farbliche Syntaxdarstellung ist noch experimentell.
|