Z 表示法：如何编写可以向关系添加一个或多个元组的操作模式

Question

我正在 Z 中编写操作模式。此操作 AssignValue 将 属性 映射到一个或多个值。

一个属性可能与一个或多个值相关联，一个值可能与一个或多个属性相关联，形成多对多关系，R⊆属性×值.

我不确定如何编写此操作来指示一个 属性 可以映射到 一个或多个值 。我这里有两个版本。版本 A 似乎将一个 属性 映射到一个值。

版本 A：

--AssignValue---
| p? : Property
| v? : Value
-------
|R′ = R ∪ { p? ↦ v? }
-------

在版本 B 中，我在 v 的声明中添加了 powerset？表示 v?是一组值（多个值）。

版本 B：

--AssignValue---
| p? : Property
| v? : P Value
-------
|R′ = R ∪ { p? ↦ v? }
-------

哪个版本是正确的？或者有更好的方法来表示这个？我是 z 表示法的新手，将不胜感激任何帮助。谢谢！

Answer 1

您没有显示整个架构。我假设你有一个状态模式 S 与关系 R : Property<->Value （相当于 R ⊆ Property × Value）并且 AssignValue 包括 ∆S.

两种样式都可以，尽管您的版本 B 可能不是您想要的。

一个关系允许有许多具有相同域元素的对，所以从

开始

R = {p0 ↦ v0, p0 ↦ v1, p3 ↦ v16}

您可以用 p?=p0、v?=v16 调用 AssignValueA 来获得

的状态

R = {p0 ↦ v0, p0 ↦ v1, p0 ↦ v16, p3 ↦ v16}

也就是说，p0 现在映射到三个单独的值。

在您的版本 B 中，您拥有完全相同的东西，但您的值现在是值集。您可能想要的是 R 将是类型 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 具有相同的界面，允许在每次调用时将 单个 值添加到单个 属性。

在这两种模型中，一个 属性 可能没有、一个或多个关联值，但该操作只允许一个 属性 在每次调用时被分配一个额外的值。

练习：尝试定义一个允许在每次调用时为多个属性分配多个额外值的操作。

Answer 2

大Z规格的例子，推荐这个最近上传的项目：https://github.com/vinahradau/finma

对于一对多，我会使用关系（与函数相反）。

以上项目示例：

userAccessRigths: USER ↔ ROLE
userAccessRigths′ = userAccessRigths ∪ {(user?, role?)}