MFP-I/0001: VDMSL Lab Sessions
[ DI/UM ]

[ Problem 1 | Problem 2 | Problem 3 | Problem 4 ]

  Problem 1 [Modelling with Sets]

Lab. Sessions:

2000.11.10

2000.11.15

Description:

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;

1. Specify functions in VDM-SL to obtain:
   1. The symmetric of a map (ie. the map of the «all ways back»)
   2. The symmetric closure of a map (ie. the map and all its ways back)
   3. The composition of two maps (ie. the map whose paths are obtained by arriving at a location accessible in the first map and proceeding from there to another location accessible in the second map)
   4. The reflection of a map (set of all trivial paths between a location in the map and itself).
   5. The transitive closure of a map (set of all direct or composed paths in a map).

2. The combined symmetric, transitive and reflexive closure of a map is a map which records an equivalence relation on locations. Which equivalence is this?

3. Upgrade your Map model by adding further information to each path, namely the name of the road, the distance involved and its (average) speed:

           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]

Lab. Sessions:

2000.11.17

2000.11.22

Description:

1. Complete the «..........» in the VDM-SL model below of a toy bank account management system (BAMS) in which accounts (Account) are uniquely identified by account identifiers (AccId). Every account records both a set of account holders (set of AccHolder) and the account's current balance (Amount):

   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
   

2. Attach an invariant to BAMS ensuring:
   1. that every account has at least one account holder.
   2. that the balance of every account is positive.

  Problem 3 [Modelling with Mappings]

Lab. Sessions:

2000.11.24

2000.11.29

Description:

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

What Quantity

chair 12

table 3

cupboard 1

is modelled by a multiset:

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 };

1. What is the outcome of mseCup(m,m)? Check it in the toolbox for m the multiset above. Check that mseCup(m,m) has the same elements of mseCup(m) but that their multiplicity is two times larger.

   Generalize this by defining

   mseExMul[@A] : map @A to nat * nat -> map @A to nat
   

   the multiplication of a multiset by a numeric factor.
2. Define a function

   mseDiff[@A] : map @A to nat * map @A to nat -> map @A to nat
   

   which computes multiset difference.
3. Generalize multiset union to a finite set of multisets:

   mseCUP[@A] : seq of map @A to nat -> map @A to nat
   

  Problem 4 [Modelling with Mappings]

Lab. Sessions:

2000.12.06

2000.12.08

Description:

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:

-

this factory builds equipments whose production involves individual components obtained from a second source;

-

each individual component has a cost and is stocked in some quantity;

-

components participate, in fixed quantities, in the production of equipments (e.g. PC board ref. X has n integrated circuits of ref. Y);

-

equipments may contain, in fixed quantities, other equipments as sub-blocks (e.g. personal computer ref. Z has m PC boards of ref. X).

-

(sub)equipments are stocked along with components in order to be readily available for production.

In summary, a production tree must exist for each equipment which may involve individual components and/or other production sub-trees.

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.

1. Define Explode : PPD * Equip -> map Comp to nat Hint: observe that the target datatype of Explode is a multiset and use the operators defined in Problem 3.
2. Add an invariant in EquipDb ensuring that an equipment is never a sub-equipment of itself. Will your Explode operation require this invariant to hold? Discuss.

Back to MFP-I's main URL.