问题标签 [z-notation]

我只是回想起我的大学课程，想知道这里是否有人甚至在专业环境中使用“Z 符号”。老实说，这是我一生中参加过的最无聊的一堂课。可能是因为老师的原因，但当时我们真的都觉得太浪费时间了。我可能错了，这就是为什么我想听听你的意见。

如果您使用它或某些派生语言 (Z++)，我只想知道它对您有什么用处。只是想知道 Z 或您的应用程序的一些众所周知的应用程序。

对于那些不熟悉的人： http: //staff.washington.edu/jon/z/z-examples.html

是否可以在 LyX 中创建 Zed 表示法方案？如何做呢？

是否有任何支持编写 Z 规范的 LaTeX 软件包？我对模式的水平和垂直格式都感兴趣。

我已经在 wiki 上阅读了这两个概念的定义，但区别仍然不清楚。有人可以举一些例子和一些简单的解释吗？

我是 Z 表示法的完整初学者。我需要在 Z 中表示一个图类型。我的想法是使用关联矩阵，以便我可以轻松地在节点和边之间自由遍历。

唯一的问题是，我不知道如何在 Z 中指定关联矩阵。我认为我需要一个 2D 数组，但是通过可用于 Z 表示法的参考资料，数组通常使用 seq 表示。还有另一种方法来指定多维数组吗？

提前致谢。

有没有办法将 UML 转换（形式化）为 Z 表示法？我的意思是有什么方法可以将 UML 需求重写为像 z 这样的正式语言？

对不起我的英语不好，我的母语不是英语。谢谢你。

抱歉，如果这不属于溢出，但我真的很想继续使用 Z 制定规范，因为我在今年大学期间开始学习它。

我想知道是否可以在 Mac 电脑上下载它，因为我目前了解它通常在 Linux 或 SunOS 上使用，但我家里没有。我将非常感谢可以下载它的资源，因为我无法通过谷歌搜索找到任何资源。我也想安装 zans animator 和 ztc 类型检查器。

提前致谢。

我有这个代码：

如您所见，taking是s映射到的关系的名称m。上面的关系显示了添加过程（联合），我在该关系中添加了一个新的 maptlet。

但是，我需要获取s此关系中可用的数量。我怎么才能得到它？以下是我所做的

但我不确定这一点。

如何使用 Z 表示法指定数学表达式？我认为自由类型适合这种情况，因为表达式具有递归性质。请考虑我们的表达式中可以有括号和变量。并且只允许 ( + , - , / , * )。例如：A + 2 * ( 3 - B ) / 4

请帮我 ...

我们有一个接受以下内容的操作 Bus_Arrives

一个 LINE、一个 BUS_ID 和一个 BUSROAD

• 给定线路的公共汽车到达车站并分配一条空的公共汽车路（如果有的话）。否则进入队列。

--------New_Bus_Arrives-------------------------------------------- -------------------------------------------------- ----

| Δ Bus_Station

| 公交线路？：LINE

| 总线？：BUS_ID

| br?: BUSROAD

===============================================

| 先决条件在这里（实现了将其添加到队列的情况，但我没有添加它，因为它与问题无关。）以下是此操作完成后系统如何更改。

| 免费' = 免费 \ {br?}

| 路由' = 路由

| 出发' = 出发 U {br? |--> 公交车？}

| 访问' = 访问 U {br? |--> 路由(|line?|) }

我的问题是：如果访问被正确表示为 Z，例如，当调用路由（线路？）关系时，它返回一组站元素 {station1，station2，station3}。但是，当我将其映射到访问关系以更新它时，我正在这样做：br？映射到 {station1,station2,station3}。这是可能的还是我不得不说这个？分别映射到集合的每个元素。此外，如果是这种情况，它如何在 Z 中表示？

关于所描述内容的额外信息：

路线：对于每条对应的公交线路，公交车经过哪些站点才能到达那里（即 - 8 号线前往洛杉矶、纽约和迈阿密）。

路由：LINE <--> STATION（关系）

免费：有哪些公交线路可用。

免费：Π BUSROAD（动力装置）

出发：对于每辆公共汽车它从哪条公交线路出发（例如从 A 出发的公共汽车 AY123）。

出发：LINE --> BUS_ID（函数）

访问：对于当前分配了公共汽车的每条公共汽车道路，它将访问哪些站点。一条公共汽车路可以有一辆且只有一辆公共汽车，也可以是可用的。

访问：BUS_ROAD <--> STATION（关系）