问题标签 [z-notation]

完全公开，这是针对大学课程的。我不希望直接得到答案，但我们将不胜感激。

我需要使用 Z 表示法对 Item 实体进行建模。这是描述：

项目：每个项目都有一个名称和一个唯一的 ID，可用于唯一地描述该项目。一个项目也有一个价格（正浮动）和一个类别。

部分要求是在没有量词的情况下对这些实体进行建模。

这是我最终得到的，但我不确定它是否正确：

项目的架构

想法是名称是字符串的某种组合，ID 是正整数和所述名称的元组，价格和类别都映射到总函数。

第一个谓词是确保价格为正，第二个谓词是确保 ID 的唯一性，即将域减少到所有尚未分配的整数。不过，我不认为这是正确的。

我正在使用 latex 来使用Z-Notation对一些函数进行建模，但是，我在显示输出字符串时遇到了问题。在这个简化的示例代码中，引号中的文本与我所期望的格式不同。我可以使用什么来保持引号内的文本格式与代码片段中的相同？

编辑：overDraftMessage应该是messageOutput，在创建简化示例时错过了更改此设置。

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

一个属性可以链接一个或多个值，一个值可以链接一个或多个属性，形成多对多关系，R ⊆ 属性 × 值。

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

版本 A：

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

版本 B：

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

我有一个操作模式 C，它由两个顺序操作模式 A 和 B 组成。必须在 B 之前执行 A。我被困在如何表示模式激活的顺序上。

我可以使用模式连词，即 C == A ∧ B 吗？或者有没有办法从A“调用”模式B？

我是 Z 表示法的新手，任何帮助将不胜感激！

我有一个 Z 规范，我必须将它翻译成 Prolog 代码。我尝试但它不起作用所以有人可以帮助我吗？

我目前正在尝试为 CreditCard 类运行 object-Z 规范的示例，但是在声明可见性列表和 INIT 模式时遇到了问题。有什么办法可以解决这个问题吗？感谢您阅读

可见性列表表示这些项目不是该类的特征

未申报名称：余额

我正在阅读名为“The Way of Z: Practical Programming with Formal Methods by Jonathan Jacky”的书，在第 18 章（8 Queen 问题）中，作者为著名的 8 Queen 问题提供了基于 Z 符号的正式解决方案。他试图通过将它连接到一个直线方程来求解对角线部分。解决方案中使用的变量是：

那么求解对角线部分的直线方程为： 其中file在这里代表一行，rank代表一列。为帮助我们理解对角线而提供的图像是：

该解决方案的工作原理如下：文件（行）编号 1 以蓝色突出显示。rank(column) 1 以红色突出显示。解决方案从下到上，从左到右。

我想计算 file(row)=4 和 rank(column)=6 的正方形的 up 和 down 函数值（以黄色突出显示）。

所以，

向上 = 等级 - 文件 = 6 - 4 = 2

下降 = 等级 + 文件 = 6 + 4 = 10

如上图所示，上对角线确实在点 2 处切割 y 截距的左边缘。但下对角线在点 9（而不是 10）处切割 y 截距。有 1 的差异。这个差异适用于所有正方形。我想知道在这种情况下我缺少什么？为什么在向下箭头的情况下（而不是在向上箭头的情况下）总是存在差异？

我还附上了完整的基于 Z 符号的解决方案以供参考：

我正在尝试使用 Z 符号来证明逻辑表达式。但是，我是 Z 语言的新手。请帮我证明上面的逻辑表达式。

我只想说这是一个大学项目。我不期待答案，而是更多的“提示”。

我有一个包含一系列队列的超市模式：

这是我定义队列的方式：

我希望定义一个模式来返回排队等候的客户总数。到目前为止，我有：

我正在努力定义total函数。它需要“循环”每个队列中的每个客户并对他们length的 s 求和。这是我到目前为止所拥有的：total = q: Queue ⦁ q.length ↦ q.length

任何想法？

我有一个关系R如下：

要获得a的图像集，我们可以用R(|{a}|) = {1,2}Z 表示法编写，使用粗括号符号 (| |)。

是否有一个数学符号来表示这一点而不是使用 Z 符号？我们可以像我们通常做的那样得到 R(a) 来获得给定值的函数图像，例如 f(a) 吗？