Z notation

zed.md

Z Notation (zed)

\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{zed-csp}
\usepackage{amsthm}

\theoremstyle{definition}
\newtheorem{definition}{Definition}[section]

\theoremstyle{remark}
\newtheorem*{remark}{Remark}

\begin{document}
Unnumbered theorem-like environments are also possible.

\begin{remark}
This statement is true, I guess.
\end{remark}

And the next is a somewhat informal definition

\theoremstyle{definition}
\begin{definition}[Fibration]
A fibration is a mapping between two topological spaces that has the homotopy lifting property for every space $X$.
\end{definition}


\begin{zed}
  \Ftf[{P \parallel[A] Q}].
\end{zed}

\begin{zed}
  \{~x: \nat | x \leq 10 @ x * x~\}
\end{zed}

\begin{zed}
  \{1, 2, 3\}
\end{zed}

\begin{zed}
  directory’ = directory \cup {} \\
\t3 \{new\_name? \mapsto new\_number?\}
\end{zed}

\[
  \exists PhoneDB @ \\
\t1     known = \empty
\]

Doing \bf{bold} things.

\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{schema*}
  x, y: \nat
\where
  x>y
\end{schema*}

\begin{axdef}
  limit: \nat
\where
  limit \leq 65535
\end{axdef}


\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{zed}
  [NAME, DATE]
\also
  REPORT ::= ok | unknown \ldata NAME \rdata
\also
  \exists n: NAME @ \\
\t1 birthday(n) \in December.
\end{zed}


\begin{syntax}
  OP & ::= & plus | minus | times | divide
\also
  EXP & ::= & const \ldata \nat \rdata \\
      & | & binop \ldata OP \cross EXP \cross EXP \rdata
\end{syntax}

\begin{argue}
  S \dres (T \dres R) \\
\t1   = \id S \comp \id T \comp R \\
\t1   = \id (S \cap T) \comp R & law about $\id$ \\ 
\t1   = (S \cap T) \dres R.
\end{argue}


\begin{infrule}
  \Gamma \shows P
\derive[x \notin freevars(\Gamma)]
  \Gamma \shows \forall x @ P
\end{infrule}

\end{document}