Формальная системная спецификация в AtelierB - Lhs бинарного оператора должна быть последовательностью (заданный тип POW(POW(INTEGERS * ORDERs)))

Question

Я пытаюсь разработать спецификацию B для небольшой системы управления запасами, и я борюсь с ошибкой:

Левая часть бинарного оператора должна быть последовательностью (данный тип POW(POW(INTEGERS * ORDERs)))

Это моя абстрактная машина:

      MACHINE
    stock(ORDER, order_limit)
CONSTRAINTS
    order_limit: NAT1
SETS
    PART_COSTS;
    PARTS;
    ORDERS
    
CONSTANTS
    backlog_limit
PROPERTIES 
    backlog_limit: NAT1 & backlog_limit <= 20
VARIABLES
    limit,
    backlog,
    part_quantity
INVARIANT 
    backlog = iseq(ORDERS) & limit : NAT1 & card(backlog) <= limit & limit <= 20 &
    part_quantity : NAT1 & part_quantity >= 200
INITIALISATION
    limit := order_limit || backlog := iseq(ORDERS) || part_quantity := 0
OPERATIONS

     receiveorder(order) =
        PRE 
            order : ORDER & limit > card(backlog)
        THEN
            backlog := backlog <- order
        END
END

Я не понимаю, почему я получаю эту ошибку, поскольку невыполненная работа - это буквально последовательность (я инициализировал ее как последовательность набора (ЗАКАЗЫ)?

Answer 1

Первое появление (после его объявления) символа находится в следующем предикате типизации:backlog = iseq(ORDERS). Таково множество всех инъективных последовательностей значений. Вы, наверное, хотели иметьbacklog: iseq(ORDERS), т. е. является некоторой инъективной последовательностью .

Конечно, вам нужно изменить инициализацию для . Вы можете инициализировать его с помощью:

• пустая последовательность:backlog := []
• или любая последовательностьbacklog :: iseq(ORDERS)
• или любое выражение типаiseq(ORDERS)

Наконец, в эксплуатацииreceiveorder, тип входного параметраorderдолжен быть типом элементовbacklogпоследовательность, то естьORDERS, и неORDER(и машинные параметры не нужны).