我只是回想起我的大学课程，想知道这里是否有人甚至在专业环境中使用“Z 符号”。老实说，这是我一生中参加过的最无聊的一堂课。可能是因为老师的原因，但当时我们真的都觉得太浪费时间了。我可能错了，这就是为什么我想听听你的意见。
如果您使用它或某些派生语言 (Z++)，我只想知道它对您有什么用处。只是想知道 Z 或您的应用程序的一些众所周知的应用程序。
对于那些不熟悉的人： http: //staff.washington.edu/jon/z/z-examples.html
问问题
3632 次
6 回答
3
Z（正如您所指出的）是一种规范符号，而不是旨在促进形式验证的编程语言。
Mondex 智能卡平台中使用的协议是使用该符号指定的较大（众所周知）项目之一。最近有一个复兴，以通过多个团队的机械检查来确定原始手动打样的正确性，其中包括对原始 Z 规范的验证。毫不奇怪，没有发现新的基本错误，尽管大多数团队的一些假设被证明是无效的。
在 Spark Ada 子集中实施之前，国家安全局Tokeneer 项目在 Z 中指定。
鉴于符号的表现力，它不太可能被扩展。这也会使证明更加复杂并且适得其反。
于 2010-05-19T20:47:02.263 回答
3
值得一看 B 方法（http://en.wikipedia.org/wiki/B-Method）。它是 Z 的一个更实用的后代。这个想法是，您实际上可以通过改进步骤（借助隐藏在幕后的定理证明器）来履行一堆证明义务，然后最终直接从您的规范生成代码。我相信它已被用于许多“现实世界”项目中。
于 2010-05-15T22:41:48.340 回答
2
Web 服务描述语言 (WSDL)是使用 Z 表示法开发的。您可以在此处找到带有 Z 符号的规范：http: //www.w3.org/TR/wsdl20/wsdl20-z.html。该规范指出
Z 表示法用于提高定义组件模型的规范文本的质量，并帮助确保测试套件涵盖组件模型隐含的所有重要规则。
于 2014-12-18T22:08:42.610 回答
2
当我读到 XCB（X11中原始 Xlib API 的替代品）被Z-notation 证明是正确的时，我第一次遇到 Z 表示法。
于 2010-05-13T02:09:15.497 回答
0
我必须在大学做Z！带回回忆，如果你有一个方便的 Linux 安装，试试这个应用程序CADiZ ...
于 2009-07-14T07:38:38.417 回答
0
'Z++' 被称为object-Z。自 90 年代初以来，我就没有在 Z 中活跃过（部分在 CADiZ 的 Windows 端口上工作，它似乎已经消失了），所以不知道它当前的社区是否，但一些最近的论文已经发表在使用 object-Z 来形式化 UML。
于 2010-05-19T21:23:33.720 回答