z-notation - 如何使用 Z 语言在其他模式中包含模式

Question

我正在使用 Z 语言的 z 表示法为我的模型编写正式规范。我被卡住了，不知道如何在另一个模式中包含一个模式并在其他模式中创建它的变量。任何指导和帮助将不胜感激。谢谢。

Answer 1

您可以使用类似于记录数据类型的模式。例如，假设您有一个描述复整数的模式：

--- Complex ---
| real, img: ℤ
------

您可以将另一个模式中的变量声明为该类型：

--- Ex1 ---
| c: Complex
----
| c.real = 5 ∧ c.img = 6
-------

您当然可以使用它创建更复杂的数据类型，这里是一个序列和一个附加元素的操作：

--- State ---
| data: seq Complex
-------

--- Add1 ---
| ΔState
| real?, img?: ℤ
----
| ∃ c:Complex · c.real = real? ∧ c.img = img? ∧ data' = data^<c>
-------

您还可以使用 theta-operator 创建该类型的实例。变量的值取自当前上下文（+ 可选装饰）：

--- Add2 ---
| ΔState
| real?, img?: ℤ
----
| data' = data^< θComplex? >
-------

θComplex?是一个实例，其中和Complex的值取自局部变量和。realimgreal?img?

我们也可以使用原来的schema来声明输入变量，把操作写得更简洁（Add3和Add2一样）：

--- Add3 ---
| ΔState
| Complex?
----
| data' = data^< θComplex? >
-------

（我删除了原来的答案，因为我误解了你的问题。）

Answer 2

像这样

--- Agent---
| state: AgentState
-------

--- Shape ---
| agents :F Agent
----
| ∃ agt:agents · agt.state = stationary                                                         
 -------