Atelier B规范报错：二元运算符左操作数应为序列问题排查

问题根源分析 #

• 类型断言错误：你的不变式中backlog = iseq(ORDERS)写法错误。iseq(ORDERS)（等价于SEQ(ORDERS)）是所有ORDERS元素组成的有限序列的集合，而backlog是一个具体的序列实例，属于这个集合，应该用成员运算符∈代替等于=。
• 初始化赋值错误：初始化时backlog := iseq(ORDERS)是把整个序列集合赋值给backlog变量，但backlog要求是单个序列，正确的初始值应该是空序列[]。
• 不变式违反风险：part_quantity初始值设为0，但你的不变式明确要求part_quantity >= 200，这会在初始化阶段直接违反不变式，需要将初始值改为符合要求的数值（比如200）。

修正后的代码 #

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 ∈ SEQ(ORDERS) & limit : NAT1 & card(backlog) <= limit & limit <= 20 &
    part_quantity : NAT1 & part_quantity >= 200
INITIALISATION
    limit := order_limit || backlog := [] || part_quantity := 200
OPERATIONS

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

内容的提问来源于stack exchange，提问作者Jack Goodwin