latex - LaTeX 中的 Z 规范

Question

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

Answer 1

有一个包，叫做zed-csp。这是有关如何使用它的参考。

这是一个示例架构：

\begin{schema}{InitJunction1}
\Delta Sys\\
junc?: JUNCTION\\
road1?: ROAD\\
road2?: ROAD
\where
road1? \neq road2?\\
junc? \notin juncList\\
\forall j: juncList @ \neg ((road1? \in roadsInJunc(j)) \land (road2? \in roadsInJunc(j))\\
roadsInJunc' = roadsInJunc \cup \{junc? \mapsto \{road1,road2\}\}\\
juncList' = juncList \cup \{junc?\}
\end{schema}

请参阅我关于该主题的问答： LyX 中的 Zed Notation

Answer 2

有很多包支持在 LaTeX 中编写 Z 规范。尽管许多具有非常相似的语法并且有些提供额外的功能。

• Cadiz.sty：https ://www.cs.york.ac.uk/hise/cadiz/latexmarkuptut.html
• oz.sty：https ://www.ctan.org/tex-archive/macros/latex/contrib/objectz?lang=en
• fuzz.sty：https ://www.cs.cmu.edu/afs/cs/academic/class/15671-f95/ftp/fuzz.sty
• zed.sty：http ://tug.ctan.org/macros/latex209/contrib/zed/zed.sty
• zeves.sty： http: //www.informatik.uni-bremen.de/agbkb/lehre/ss12/foma/Z/z-eves.sty
• zed-csp.sty：http ://ctan.mackichan.com/macros/latex/contrib/zed-csp/zed-csp.sty

可以在此处找到有关这些软件包的更多信息：http: //czt.sourceforge.net/latex/

它解释说 fuzz.sty 是第一个并且包含重要的宏但与 ISO-Z 标准不兼容，zed.sty 和 zed-csp.sty 是牛津版本，改进了 fuzz.sty 等

Answer 3

这是我的软件工程教授在创建 Z 模式和操作时用于 LaTeX 格式的内容：

\usepackage{oz, amsfonts}
...
\begin{schema}{MusicStore}
member: \pset NAME\\
orders: \pset (NAME\times ALBUM)\\
owns: \pset (NAME\times ALBUM)
\ST
{\bf dom}\mbox{ } orders \subseteq member\\
{\bf dom}\mbox{ } owns \subseteq member\\
\forall (m, a)\in orders.(m, a)\notin owns
\end{schema}

我希望它会有所帮助。