Z test page

This page exercises most of the translations provided by the Z2HTML tool.


Most Z symbols are represented by GIF's. Symbols which are not yet supported appear as untranslated LaTeX commands.

Logic true false \lnot \land \lor \implies \iff \forall \exists \exists1 let \vdash \models
Sets etc. = \neq \in \notin \emptyset \subseteq \subset { } | @ \lambda \mu \cap \cup \ \bigcup \bigcap \power \cross first second if then else \ldata \rdata
Relations \rel \mapsto dom ran \comp \circ \dres \ndres \rres \nrres \limg \rimg ~ + * \oplus R id
Functions \pfun \fun \pinj \inj \bij \psurj \surj \ffun \finj
Numbers etc. \num \nat \nat1 + - * div mod \leq < \geq > .. min max # \finset \finset1
Sequences seq seq1 iseq \langle \rangle \cat \dcat head tail last front rev in \filter \extract disjoint partition
  squash prefix suffix
Bags bag \lbag \rbag count \bcount \otimes \inbag \subbageq \uplus \uminus items
Schema calc. \defs [ | ] ; . \lnot \land \lor \theta \semi >> \ \project pre \lblot \rblot
Conventions     ? ! ' \Delta \Xi

Z paragraphs

Inline math

ConsoleOp \defs SelectDisplay \lor SelectPatientList \lor SelectFieldList \lor ... \lor IgnoreOthers

Axiomatic definition

Inline axiomatic definition and Z

no_name: NAME

no_patient == no_name; no_field == no_name

Multiline Z, axiomatic definition boxes

cal_factor: cal_const \fun VALUE

ACCUMULATION == counter \fun VALUE
PRESCRIPTION == prescrip \fun VALUE

Preset: studies \fun (FIELD \pfun PRESCRIPTION)
Prescribed: patients \fun (FIELD \pfun PRESCRIPTION)
Accumulated: patients \fun (FIELD \pfun ACCUMULATION)
\forall s: studies @ no_field \notin dom (Preset s)
\forall p: patients @ no_field \notin dom (Prescribed p)
    \land dom (Prescribed p) = dom (Accumulated p)

Schema boxes

\begin{schema}{ TherapyControl }


The CheckOut operation has two input parameters, the person p? and the document d?.

\begin{schema}{ CheckOut }

\Delta Documents
d? \notin dom checked_out
(d?, p?) \in permission
checked_out' = checked_out \cup {(d?, p?)}

Generic definition box

Q \comp R - Relational composition: Q composed with R
R \circ Q - Backward relational composition, same as Q \comp R

\begin{gendef} [X,Y,Z]

_ \comp _ : (X \rel Y) \cross (Y \rel Z) \fun (X \rel Z)
_ \circ _ : (Y \rel Z) \cross (X \rel Y) \fun (X \rel Z)
\forall Q: X \rel Y; R: Y \rel Z @
    Q \comp R = R \circ Q = {  x: X; y: Y; z: Z | x Q y \land y R z @ x \mapsto z  }

Argue environment

\exists Editor' @ Insert Definition of precondition
    \iff \exists left', right': TEXT | ... @ ... Expand schemas
    \iff \exists left', right': TEXT @ ... \land ... Restricted \exists-quantifier
    \iff pr \land # ((left \cat \langle ch? \rangle) \cat right) \leq maxsize One-point rule
    \iff pr \land # left + # \langle ch? \rangle + # right \leq maxsize # (s \cat t) = # s + #t
    \iff pr \land # left + 1 + # right \leq maxsize # \langle x \rangle = 1
    \iff pr \land # left + # right < maxsize Arithmetic

This completes the calculation. The precondition of Insert is   ch? \in printing \land # left + # right < maxsize. When the input is a printing character, the number of characters to the left and right of the cursor must be less than the buffer size.

Other formatting

Here is some emphasized text, boldface text,   typewriter font text, and an enclosed mbox. You must ensure that these don't break across a line, {\em like this). Footnotes don't appear at the bottom of the page (Instead footnotes are translated inline, as you see here.). Footnotes are the only one of these environments that can extend across lines.

Quotes are indented.

Cross references

The TherapyControl schema in section [sect:schema] is from [jacky95].


 TherapyControl or any other formal text at the beginning of a line is handled properly. ... That's about all.