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

[ Problem 1 | 434Problem 2 | 437Problem 3 | 440Problem 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

WhatQuantity
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.

J. N. Oliveira
2000-11-23