programming-languages - 已知 "Z notation"应用程序？

Question

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

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

不熟悉的人:http://staff.washington.edu/jon/z/z-examples.html

Answer 1

值得一看 B 方法 ( http://en.wikipedia.org/wiki/B-Method )。它是 Z 的一个更实用的后代。这个想法是，您实际上可以通过改进步骤(在隐藏在幕后的定理证明器的帮助下)履行一堆证明义务，然后最终直接从您的规范中生成代码。我相信它已被用于许多“现实世界”项目中。