CODEWITHSUNDEEP
mapsrangeformal-languagesformal-methodsvdm++
bonapart3
bonapart3

Reputation: 519

Formal methods - Map of price relating cars to price with two sets BL and Fiat

I have a question from Chapter 5 in Practical Formal Methods with VDM by Derek Andrews and Darrel INCE which I was unsure how to answer, so here it is, thanks for any help!

If the map price relates cars to their price, the set BL contains the cars made by British Leyland and Fiat the cars made by Fiat. Write down the following descriptions using the map facilities and set facilities described in this chapter and chapter on sets.

(d) The number of Fiat cars that have a price between £6000 and £7000

This is what I think so far...

1.Get prices of all fiats i.e. price(fiat) returning a subset of the price map

i.e. {punto -→ 5500, panda -→ 6600}

2.Possibly card on a map restriction on the range of price(fiat)...

   **{6000...7000} ◁ rng price(fiat)**

But I am not sure that this is legal

Upvotes: 0

Views: 134

Answers (2)

danielp
danielp

Reputation: 1187

  1. I think a function application is not what you need to get a subset of the price map, you want to restrict the map to the domain of Fiats, so let's use a domain restriction:

    fiat <: price

    That should yield {punto → 5500, panda → 6600}

  2. Now we want a subset of that where the prices (the right side, i.e. the range) is restricted to 6000..7000:

    (fiat <: price) :> {6000,...,7000}

    That gives you the set of couples (Fiat,Price) where the prices are in the given interval.

  3. Apply the cardinality operator to the result to get the number of found cars.

(Caveat: I'm not very familiar with VDM but the underlying logic should be quite the same in VDM, B, Z, etc. I did not check if the used syntax above is completely correct.)

Edit: I fixed the syntax of the interval, thanks to Nick's answer.

Upvotes: 2

Nick Battle
Nick Battle

Reputation: 703

Daniel's answer is very nearly correct, just missing curley brackets round the integer range at the end. Here is the example, tested under VDMJ:

values
    price = { <PUNTO> |-> 5500, <PANDA> |-> 6600, <MINI> |-> 9000 };

    BL = { <MINI> };

    fiat = { <PUNTO>, <PANDA> };

And then:

> p fiat <: price
= {<PUNTO> |-> 5500, <PANDA> |-> 6600}
Executed in 0.079 secs.
>
> p (fiat <: price) :> {6000,...,7000}
= {<PANDA> |-> 6600}
Executed in 0.023 secs.
>
> p card dom ((fiat <: price) :> {6000,...,7000})
= 1
Executed in 0.064 secs.
>

Upvotes: 2

Related Questions