0

我有一个来自 Derek Andrews 和 Darrel INCE 的 VDM 实用形式方法第 5 章的问题，我不确定如何回答，所以在这里，感谢您的帮助！

如果地图价格与汽车价格相关，则集合BL包含 British Leyland 制造的汽车和Fiat 菲亚特制造的汽车。使用本章和集合章节中描述的地图工具和集合工具写下以下描述。

(d) 价格在 6000 英镑到 7000 英镑之间的菲亚特汽车的数量

这是我目前的想法...

1.获取所有法币的价格，即price(fiat)返回价格图的子集

即{punto -→ 5500, panda -→ 6600}

2.可能在地图上限制价格范围（法币）...

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

但我不确定这是否合法

4

2 回答 2

2

  1. 我认为功能应用程序不是您需要获取价格图的子集，您希望将地图限制到 Fiats 的域，所以让我们使用域限制：

    fiat <: price

    那应该产生 {punto → 5500, panda → 6600}

  2. 现在我们想要一个子集，其中价格（右侧，即范围）限制为 6000..7000：

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

    这为您提供了价格在给定区间内的一组夫妇 (Fiat,Price)。

  3. 将基数运算符应用于结果以获取找到的汽车数量。

（警告：我对 VDM 不是很熟悉，但底层逻辑在 VDM、B、Z 等中应该是完全相同的。我没有检查上面使用的语法是否完全正确。）

编辑：感谢尼克的回答，我修复了间隔的语法。

于 2014-05-30T04:58:39.257 回答
2

丹尼尔的答案几乎是正确的，只是在最后的整数范围内缺少花括号。这是在 VDMJ 下测试的示例：

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

    BL = { <MINI> };

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

进而：

> 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.
>
于 2014-05-30T09:47:41.527 回答