Search code examples
latexlyxz-notation

Z specifications in LaTeX

Is there any package for LaTeX which will support writing Z specifications? I am interested in both horizontal and vertical formats for schemas.

Solution

  • 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