问题标签 [z-notation]

我应该找到 z 表示法解析器或编译器。如果可以，请你帮助我。

What are applications of Objective-Z?

I have read about Objective-Z, but I cannot imagine to what it would be applied.

This question may be too broad, but I do not think that there are too many answers.

我正在使用 HOL-Z 中的数学工具包来释放一些 Isabelle 谓词。具体来说，我使用部分函数定义来定义我正在编写的 Z 规范中的一些关系，在其中我将模式转换为规范语句，以便我可以生成简单的 HOL 谓词。

来自 HOL-Z 工具包的定义

当我在谓词中编写以下内容时：

其中 balance 和 Bbalance 都是偏函数（在 Z 中），在 Isabelle 中的形式为 ('a <=> 'b)，我认为它表现良好。

我如何定义另一个函数，我说这两个部分函数对于所有 'x' 都是完全不相交的。我的意思是相同值在两个偏函数“balance”和“Bbalance”上的关系应用永远不会产生相同的值。就像是...

抱歉解释不佳。我们通过专家建议学习:)。

我正在尝试编写一个谓词，“如果某个常数为真”（在这种情况下，如果 'sec=ok'）那么谓词将评估为 False，因为我已经在那个特定的结果中编写了一个表达式与谓词其他地方的另一个表达式相矛盾的暗示。(f%^x ≠ g%^x) ∧ (f%^ci = g%^ci) 应该是矛盾的，因为 x 和 ci 都是普遍量化的并且具有相同的类型。

但是，Nitpick 产生了一个我无法理解的反例。我希望是否有人可以检查这个引理，看看是否可以证明矛盾。或者让我知道我哪里出错了。所以简要说明如下；

• f 和 g 是从任意类型 'a 到 'b 的两个偏函数。

• 'sec' 是一个常量，其值为 'ok' 和 'notok'

  /li>

我还看到了两个 Z 数学工具包之间关于函数应用的“细微”差异。我都试过了，但问题仍然存在。

可以在这里看到 Nitpick 错误 http://i58.tinypic.com/316te1t.png

注意：作为参考，请从 HOL-Z 中找到我当前使用的部分函数的定义。

我发现的所有示例都只有 2 个声明such as name and date OR members and telephone。但是，我的情况是这样的：

我想创建一个名为 AppointmentDB 的 Z 模式。AppointmentDB 保留约会的详细信息，例如目的、参加者和日程安排

我的看法（已编辑）：

有 5 个声明和 1 个谓词

如您所见，我正在尝试将 APPOINTMENT 链接到它的所有其他属性。我的架构是否正确或完整，或者如何进一步优化它？另外，我怎么知道我应该从关系中考虑哪个关系来定义谓词部分？

这是我的约会数据库的 Z 模式。

我想创建一个搜索功能，根据attendees.

1. 我希望搜索功能返回约会对象的所有详细信息。

我该如何设计它？

这是我的看法：

我是 Z 表示法的新手，

假设我有一个函数 f 定义为 X |--> Y ，其中 X 是字符串，Y 是数字。

如何在此函数中获得最高 Y 值？形式方法中是否存在“循环”，所以我可以使用循环来解决它？

我知道 Z 表示法中有递归，但根据提供的材料，我发现它只适用于 multiset 或 bag，它可以适用于函数吗？

“循环”或递归应用程序的任何额外参考应用程序将不胜感激。对不起我的英语不好。

我想知道这里是否有人甚至在专业环境中使用过“Z 符号”。只是想知道 Z 或您的应用程序的一些众所周知的应用程序。

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

我想知道“在 Z 表示法中，如何定义整数的除法运算”

我有一个Array跟踪模式序列的Data模式。使用提升，我可以提升Increment操作以使用Array.

ArrayIncrement里面只增加一个数据Array。我怎样才能使它每增加一次 ？Data\ran data

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