使用域减法操作函数变量时出现类型不匹配错误求助

我在B方法的Rodin环境中编写无人机系统的形式化规范，尝试通过loc := loc ⩤ {dr}移除函数loc中的某个无人机条目，但始终遇到类型不匹配错误，具体错误如下：

该行存在多个标记

• 类型DRONES×TARGETS与DRONES不匹配
• 类型DRONES与'1×'2不匹配

上下文和机器代码如下：

上下文定义 #

CONTEXT
    Drone_Ctx
SETS
    DRONES
    TARGETS
CONSTANTS
    assigned
AXIOMS
    axm1: assigned : DRONES ↔ TARGETS
END

机器AV_0代码 #

MACHINE
    AV_0
SEES
    Drone_Ctx
VARIABLES
    loc
    reached
INVARIANTS
    inv1: loc : DRONES → TARGETS
    inv2: reached ⊆ DRONES
EVENTS
    INITIALISATION
    THEN
        act1: loc := ∅
        act2: reached := ∅
    END

    Abort_Mission:
    ANY
        dr
    WHERE
        grd1: dr ∈ DRONES
        grd2: dr ∈ dom(loc)
        grd3: dr ∉ reached
    THEN
        act1: loc := loc ⩤ {dr}
    END
END

我尝试过用loc ≔ ∅、∅ ▷ assigned、assigned ⩤ DRONES等方式初始化loc，但执行loc ⩤ {dr}时仍报错：

Types DRONES×TARGETS and DRONES do not match .

解决方法 #

问题出在⩤操作符的用法和类型匹配逻辑上：

在B语言中，⩤是**域反限制（Domain Anti-Restriction）**操作符，语法为rel ⩤ S，表示从关系rel中移除所有域属于集合S的元素。但Rodin的类型检查对该操作的约束较严格，这里可以用更明确的方式实现需求：

方式1：使用集合减法移除对应有序对

函数loc本质是DRONES × TARGETS的子集（每个无人机对应唯一目标），直接移除dr对应的有序对即可：

loc := loc \ {dr ↦ loc(dr)}

这种写法明确指定要移除的元素，Rodin能正确推断类型，完全符合loc的函数类型约束。

方式2：使用域限制操作符↾结合集合差

通过DRONES \ {dr}得到除dr外的所有无人机，再用域限制操作符↾保留这些无人机对应的函数条目：

loc := loc ↾ (DRONES \ {dr})

这种写法更贴合函数操作的语义，直接对函数的域进行筛选，类型匹配完全符合Rodin的检查要求。

补充说明 #

初始化loc时，loc := ∅是合法的（空函数属于DRONES → TARGETS），无需额外复杂写法。如果需要基于assigned关系初始化，可使用loc := assigned ↾ ∅或者直接loc := ∅，Rodin会自动维护函数类型的不变式。

内容的提问来源于stack exchange，提问作者Timur Umarov