MFP-I/0001: VDMSL Lab Sessions | |
---|---|
[ DI/UM ] |
Problem 1 [Modelling with Sets] |
2000.11.10 | 2000.11.15 |
To improve the operation of fire-brigades fighting forest fires in the hot season, the National Service for Social Protection is developing a mobile station-based geographical information system which keeps track of rural area accessibility.
In this exercise we are concerned with the design of the central database component which records road maps (distances, road alternatives and so on) - a component which we are going to model with sets.
We start from a very simple model (to be improved at a later stage): a road-map is a directed graph whose arcs A->B record the you can drive from A to B relation:
Map = set of Path; Path :: From: Location To: Location; Location = token;
UMap = set of UPath; UPath :: From: Location Info: PathInfo To: Location; PathInfo :: name: token distance: real speed: real; Location = token;
Scale up the function definitions above from Map to UMap. Clearly, you have to pay attention to the handling of PathInfos, by eg. summing up distances, computing average speeds and concatenating road names. (Hint: recall the notion of a weighted graph.)
Problem 2 [Modelling with Mappings]
2000.11.17 | 2000.11.22 |
types BAMS = map AccId to Account; Account :: H: set of AccHolder B: Amount; AccId = seq of char; AccHolder = seq of char; Amount = int; functions Init : () -> BAMS Init () == {|->}; OpenAccount : BAMS * AccId * set of AccHolder * Amount -> BAMS OpenAccount(bams,n,h,m) == bams munion ......................... pre not n in set dom bams; AddAccHolders: BAMS * AccId * set of AccHolder -> BAMS AddAccHolders(bams,n,h) == bams ++ { n |-> let a = bams(n) in mk_Account(a.H union h,a.B) } pre ...................; Credit: BAMS * AccId * Amount -> BAMS Credit(bams,n,m) == ............................... pre n in set dom bams; Withdraw: BAMS * AccId * Amount -> BAMS Withdraw(bams,n,m) == bams ++ { n |-> let a = bams(n) in mk_Account(a.H, a.B - m) } pre ....................................; GoodCostumers: BAMS * Amount -> set of AccId GoodCostumers(bams,m) == --- should select the accounts whose balance is greater than m
Problem 3 [Modelling with Mappings]
2000.11.24 | 2000.11.29 |
A multiset (vulg. «bag») is an «intermediate» notion between a set (set of A) and a sequence (seq of A). In a multiset, a given element a of A may occur more than once, its number of occurrences being called its multiplicity:
map @A to nat
Multisets are very common in formal modelling. For instance, an inventory
|
m = {"chair"|->12,"table"|->3,"cupboard"|->1}Invoices are multisets, bank statements are multisets, etc.
The empty mapping {|->} models the empty multiset and set-union generalizes to multiplicity addition, that is, given two multisets n and m, their union is defined as follows:
mseCup[@A] : map @A to nat * map @A to nat -> map @A to nat mseCup(m,n) == m ++ n ++ { a |-> m(a) + n(a) | a in set dom n inter dom m };
Generalize this by defining
mseExMul[@A] : map @A to nat * nat -> map @A to natthe multiplication of a multiset by a numeric factor.
mseDiff[@A] : map @A to nat * map @A to nat -> map @A to natwhich computes multiset difference.
mseCUP[@A] : seq of map @A to nat -> map @A to nat
Problem 4 [Modelling with Mappings]
2000.12.06 | 2000.12.08 |
Consider the following data model for a «toy factory» production database:
types PPD :: S: Stock P: Pricelist E: EquipDb; Stock = map Unit to Quantity; Unit = Equip | Comp; Quantity = nat; Equip :: K: nat; Comp :: K: nat; Pricelist = map Comp to Currency; Currency = real; EquipDb = map Equip to map Unit to Quantity;Observe that:
One of the most interesting operations which can be defined over the PPD data model specification above is that which (recursively) computes the part explosion (bill of materials) of some given equipment, according to its production tree.
Back to MFP-I's main URL.