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