乳胶中的z规格

Question

是否有乳胶的包裹可以支持编写Z规格？我对模式的水平和垂直格式感兴趣。

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符号

Answer 2

有很多软件包为在乳胶中编写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/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/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-Schemas和操作时用于乳胶形式的方法：

\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}

我希望这有用。