Формальные методы - Карта цен, относящая автомобили к цене с двумя наборами BL и Fiat

У меня есть вопрос из главы 5 "Практические формальные методы с VDM" Дерека Эндрюса и Даррела INCE, на который я не был уверен, как ответить, так что вот, спасибо за любую помощь!

Если цена на карте соотносит автомобили с их ценой, в набор BL входят автомобили, произведенные British Leyland, а Fiat - автомобили Fiat. Запишите следующие описания, используя карту объектов и набор объектов, описанных в этой главе и главе о наборах.

(d) Количество автомобилей Fiat, цена которых составляет от £6000 до £7000

Это то, что я думаю до сих пор...

1. Получить цены всех фиатов, т.е. цены ( фиат ), возвращающие подмножество ценовой карты.

т.е. {punto - → 5500, panda - → 6600}

2. Возможно на карте ограничение карты по диапазону цен (указ)...

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

Но я не уверен, что это законно

Источник

2 ответа

Решение

  1. Я думаю, что функциональное приложение - это не то, что вам нужно, чтобы получить подмножество ценовой карты, вы хотите ограничить карту доменом Fiats, поэтому давайте используем ограничение домена:

    fiat <: price

    Это должно дать {punto → 5500, panda → 6600}

  2. Теперь мы хотим получить подмножество того, где цены (правая сторона, то есть диапазон) ограничены 6000..7000:

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

    Это дает вам набор пар (Fiat,Price), где цены находятся в заданном интервале.

  3. Примените кардинальный оператор к результату, чтобы получить количество найденных автомобилей.

(Предостережение: я не очень знаком с VDM, но базовая логика должна быть совершенно одинаковой в VDM, B, Z и т. Д. Я не проверял, является ли приведенный выше синтаксис полностью правильным.)

Изменить: я исправил синтаксис интервала, благодаря ответу Ника.

Источник

Ответ Даниэля является почти правильным, просто пропуская фигурные скобки вокруг целого диапазона в конце. Вот пример, протестированный под 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.
>
Источник
Другие вопросы по тегам