当前位置：文江博客话题详情

LaTeX 中的 Z 规范

发布于 2024-09-06 03:36:28 字数 44 浏览 3 评论 0原文

LaTeX 有没有支持编写 Z 规范的包？我对模式的水平和垂直格式感兴趣。

原文

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

謸气贵蔟 2024-09-13 03:36:28

有一个包，叫做 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 表示法

There is a package, it is called zed-csp. Here's a reference on how to use it.

Here's an example schema:

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

See my question and answer on the subject:
Zed Notation in LyX

回复收藏 0 原文

农村范ル 2024-09-13 03:36:28

有相当多的软件包支持在 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 等

回复收藏 0 原文

巨坚强 2024-09-13 03:36:28

这是我的软件工程教授在创建 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}

我希望它有帮助。

This is what my Software Engineering Professor used for the LaTeX-formatting when creating the Z-Schemas and Operations:

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

I hope it's helpful.

回复收藏 0 原文

~没有更多了~