Author: Peter Gorm Larsen

This specification was produced for VDM-SL courses presented by Peter Gorm Larsen in 1996. The modelling of a Bill Of Material (BOM) is a rather standard example making use of an Directed Acyclic Graph (DAG) structure.

Properties | Values |
---|---|

Language Version: | classic |

Entry point : | DEFAULT`Parts(1,bom) |

Entry point : | DEFAULT`Parts(1,cycle) |

```
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))
```