0

Derek Andrews と Darrel INCE による Practical Formal Methods with VDM の Chapter 5 から質問があります。

マップの価格が車をその価格に関連付ける場合、セットBLには、British Leyland 製の車とFiat製の車が含まれます。この章とセットの章で説明されているマップ機能とセット機能を使用して、次の説明を書き留めます。

(d) 価格が 6000 ～ 7000 ポンドのフィアット車の数

ここまでは・・・と思います。

1. すべての法定通貨の価格を取得します。つまり、価格マップのサブセットを返すprice(fiat)

つまり、{プント -→ 5500、パンダ -→ 6600}

2.価格帯（法定通貨）のマップ上のカード制限の可能性...

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

しかし、これが合法かどうかはわかりません

4

2 に答える 2

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 に答える
2

  1. 関数アプリケーションは、価格マップのサブセットを取得するために必要なものではないと思います。マップをフィアットのドメインに制限したいので、ドメイン制限を使用しましょう。

    fiat <: price

    それは {punto → 5500, panda → 6600} をもたらすはずです

  2. ここで、価格 (右側、つまり範囲) が 6000..7000 に制限されているサブセットが必要です。

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

    これにより、価格が指定された間隔内にあるカップルのセット (フィアット、価格) が得られます。

  3. カーディナリティ演算子を結果に適用して、見つかった車の数を取得します。

(注意: 私は VDM にあまり詳しくありませんが、基になるロジックは VDM、B、Z などでまったく同じである必要があります。上記で使用されている構文が完全に正しいかどうかは確認していません。)

編集: Nick's answer のおかげで、間隔の構文を修正しました。

于 2014-05-30T04:58:39.257 に答える