Z спецификации в LaTeX - PullRequest
Новая
       36

Z спецификации в LaTeX

6 голосов
/ 19 июня 2010

Есть ли пакет для LaTeX, который будет поддерживать написание спецификаций Z? Меня интересуют как горизонтальные, так и вертикальные форматы схем.

Ответы [ 3 ]

9 голосов
/ 19 июня 2010

Есть пакет, он называется 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}

См. Мой вопрос и ответ по теме: Zed НотацияLyX

1 голос
/ 30 июля 2015

Существует довольно много пакетов, которые предлагают поддержку для написания Z-спецификации в LaTeX. Хотя многие имеют очень похожий синтаксис, а некоторые предлагают дополнительные функции.

Более подробную информацию об этих пакетах можно найти здесь: http://czt.sourceforge.net/latex/

Это объясняет, что это был fuzz.sty, который был первым и содержит важные макросы, но не совместим со стандартом ISO-Z, zed.sty и zed-csp.sty были оксфордской версией, которая улучшила fuzz.sty и т. Д.

0 голосов
/ 02 апреля 2016

Это то, что мой профессор программной инженерии использовал для форматирования LaTeX при создании Z-схем и операций: 

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

Надеюсь, это полезно.

...