我正在 Z 中编写操作模式。此操作 AssignValue 将属性映射到一个或多个值。
一个属性可以链接一个或多个值，一个值可以链接一个或多个属性，形成多对多关系，R ⊆ 属性 × 值。
我不确定如何编写此操作以指示一个属性可以映射到一个或多个值。我这里有两个版本。版本 A 似乎将一个属性映射到一个值。
版本 A：
--AssignValue---
| p? : Property
| v? : Value
-------
|R′ = R ∪ { p? ↦ v? }
-------
在版本 B 中，我在 v? 的声明中添加了一个幂集？表示 v? 是一组值（多个值）。
版本 B：
--AssignValue---
| p? : Property
| v? : P Value
-------
|R′ = R ∪ { p? ↦ v? }
-------
哪个版本是正确的？还是有更好的方法来表示这一点？我是 z 表示法的新手，任何帮助将不胜感激。谢谢！
您还没有显示整个架构。我假设您有一个S带有关系R : Property<->Value（相当于R ⊆ Property × Value）并AssignValue包含的状态模式∆S。
两种样式都可以工作，尽管您的版本 B 可能不是您想要的。
一个关系允许有许多对具有相同的域元素，所以从
R = {p0 ↦ v0, p0 ↦ v1, p3 ↦ v16}
你可以打电话AssignValueA给p?=p0,v?=v16来获得一个状态
R = {p0 ↦ v0, p0 ↦ v1, p0 ↦ v16, p3 ↦ v16}
也就是说，p0现在映射到三个单独的值。
在您的版本 B 中，您拥有完全相同的东西，但是您的值现在是一组值。您可能想要的是typeR的总函数Property → Value。p0现在，假设只有通过的属性p3，您的初始R值为
R = {p0 ↦ {v0, v1}, p1 ↦ ∅, p2 ↦ ∅, p3 ↦ {v16}}
你需要定义
--AssignValueB----------------
| ∆S
| p? : Property, v? Value
------------
| R' = R ⊕ {p? ↦ R p? ∪ {v?}}
------------------------------
这与 具有相同的接口AssignValueA，允许每次调用向单个属性添加单个值。
在这两种模型中，一个属性可能没有、一个或多个关联值，但该操作只允许为一个属性在每次调用时分配一个额外的值。
练习：尝试定义一个操作，允许在每次调用时为多个属性分配多个额外值。
举个大 Z 规范的例子，我推荐这个最近上传的项目：https ://github.com/vinahradau/finma
对于一对多，我会使用关系（作为函数的对立面）。
上述项目的示例：
userAccessRigths: USER ↔ ROLE
userAccessRigths′ = userAccessRigths ∪ {(user?, role?)}