![Typesetting Z specifications with zed-csp](https://writelatex.s3.amazonaws.com/published_ver/5457.jpeg?X-Amz-Expires=14400&X-Amz-Date=20240727T035621Z&X-Amz-Algorithm=AWS4-HMAC-SHA256&X-Amz-Credential=AKIAWJBOALPNFPV7PVH5/20240727/us-east-1/s3/aws4_request&X-Amz-SignedHeaders=host&X-Amz-Signature=21150ff4425fb4525f12e6b13d4619bf6d20c2fd07472dc63ceeda333b737e8b)
Examples from the zed-csp
documentation.
\documentclass[12pt]{article}
\usepackage[utf8]{inputenc}
\usepackage[b5paper,margin=1cm]{geometry}
\usepackage{zed-csp}
\begin{document}
\title{Typesetting Z specifications with \texttt{zed-csp}}
\author{}\date{}
\maketitle
\thispagestyle{empty}
\begin{schema}{PhoneDB}
known: \power NAME \\ phone: NAME \pfun PHONE
\where
known = \dom phone
\end{schema}
\begin{schema}{Document[CHAR]}
left, right: \seq CHAR
\end{schema}
\begin{axdef}
policy: \power_1 RESOURCE \fun RESOURCE
\where
\forall S: \power_1 RESOURCE @ \\
\t1 policy(S) \in S
\end{axdef}
\begin{gendef}[X,Y]
first: X \cross Y \fun X
\where
\forall x: X; y: Y @ \\
\t1 first(x,y) = x
\end{gendef}
\begin{schema}{AddPhone}
\Delta PhoneDB \\ name?: NAME \\ number?: PHONE
\where
name? \notin known
\also
phone' = phone \oplus \{name? \mapsto number?\}
\end{schema}
\begin{syntax}
OP & ::= & plus | minus | times | divide
\also
EXP & ::= & const \ldata \nat \rdata \\
& | & binop \ldata OP \cross EXP \cross EXP \rdata
\end{syntax}
\end{document}