Z test page

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

Symbols

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

Logic true false ¬ Ù Ú Þ Û " $ $₁ let $\vdash$ $\models$
Sets etc. = ¹ Î Ï Æ Í Ì { } | · l m Ç È \ $\bigcup$ $\bigcap$ $\power$ ´ first second if then else $\ldata$ $\rdata$
Relations « $\mapsto$ dom ran $\comp$ ° $\dres$ $\ndres$ $\rres$ $\nrres$ $\limg$ $\rimg$ ^~ ⁺ ^* Å R id
Functions $\pfun$ ® $\pinj$ $\inj$ $\bij$ $\psurj$ $\surj$ $\ffun$ $\finj$
Numbers etc. $\num$ $\nat$ $\nat$ ₁ + - * div mod £ < ³ > .. min max # $\finset$ $\finset$ ₁
Sequences seq seq₁ iseq á ñ ^ $\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$ [ | ] ; . ¬ Ù Ú q $\semi$ >> \ $\project$ pre $\lblot$ $\rblot$
Conventions ? ! ' D X

Z paragraphs

Inline math

ConsoleOp $\defs$ SelectDisplay Ú SelectPatientList Ú SelectFieldList Ú ... Ú IgnoreOthers

Axiomatic definition

Inline axiomatic definition and Z

$\begin{axdef}$

no_name: NAME
$\end{axdef}$

no_patient == no_name; no_field == no_name

Multiline Z, axiomatic definition boxes

$\begin{axdef}$

cal_factor: cal_const ® VALUE
$\end{axdef}$

ACCUMULATION == counter ® VALUE

PRESCRIPTION == prescrip ® VALUE

$\begin{axdef}$

Preset: studies ® (FIELD $\pfun$ PRESCRIPTION)
Prescribed: patients ® (FIELD $\pfun$ PRESCRIPTION)
Accumulated: patients ® (FIELD $\pfun$ ACCUMULATION)

$\where$

" s: studies · no_field Ï dom (Preset s)
" p: patients · no_field Ï dom (Prescribed p)
Ù dom (Prescribed p) = dom (Accumulated p)
$\end{axdef}$

Schema boxes

$\begin{schema}{$ TherapyControl

Session
Field
Intlk
...
Console

$\end{schema}$

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

$\begin{schema}{$ CheckOut

D Documents
p?: PERSON
d?: DOCUMENT

$\where$

d? Ï dom checked_out
(d?, p?) Î permission
checked_out' = checked_out È {(d?, p?)}

$\end{schema}$

Generic definition box

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

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

_ $\comp$ _ : (X « Y) ´ (Y « Z) ® (X « Z)
_ ° _ : (Y « Z) ´ (X « Y) ® (X « Z)

$\where$

" Q: X « Y; R: Y « Z ·
Q $\comp$ R = R ° Q = { x: X; y: Y; z: Z | x Q y Ù y R z · x $\mapsto$ z }

$\end{gendef}$

Argue environment

$ Editor' · Insert Definition of precondition
Û $ left', right': TEXT | ... · ... Expand schemas
Û $ left', right': TEXT · ... Ù ... Restricted $-quantifier
Û pr Ù # ((left ^ á ch? ñ) ^ right) £ maxsize One-point rule
Û pr Ù # left + # á ch? ñ + # right £ maxsize # (s ^ t) = # s + #t
Û pr Ù # left + 1 + # right £ maxsize # á x ñ = 1
Û pr Ù # left + # right < maxsize Arithmetic

This completes the calculation. The precondition of Insert is ch? Î printing Ù # 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].

Miscellaneous

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

Logic	true false ¬ Ù Ú Þ Û " $ $₁ let $\vdash$ $\models$
Sets etc.	= ¹ Î Ï Æ Í Ì { } \| · l m Ç È \ $\bigcup$ $\bigcap$ $\power$ ´ first second if then else $\ldata$ $\rdata$
Relations	« $\mapsto$ dom ran $\comp$ ° $\dres$ $\ndres$ $\rres$ $\nrres$ $\limg$ $\rimg$ ^~ ⁺ ^* Å R id
Functions	$\pfun$ ® $\pinj$ $\inj$ $\bij$ $\psurj$ $\surj$ $\ffun$ $\finj$
Numbers etc.	$\num$ $\nat$ $\nat$ ₁ + - * div mod £ < ³ > .. min max # $\finset$ $\finset$ ₁
Sequences	seq seq₁ iseq á ñ ^ $\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$ [ \| ] ; . ¬ Ù Ú q $\semi$ >> \ $\project$ pre $\lblot$ $\rblot$
Conventions	? ! ' D X

$\begin{axdef}$
		Preset: studies ® (FIELD $\pfun$ PRESCRIPTION)
		Prescribed: patients ® (FIELD $\pfun$ PRESCRIPTION)
		Accumulated: patients ® (FIELD $\pfun$ ACCUMULATION)

	$\where$

		" s: studies · no_field Ï dom (Preset s)
		" p: patients · no_field Ï dom (Prescribed p)
		Ù dom (Prescribed p) = dom (Accumulated p)
	$\end{axdef}$

$\begin{schema}{$		TherapyControl



		Session
		Field
		Intlk
		...
		Console

	$\end{schema}$

$\begin{schema}{$		CheckOut



		D Documents
		p?: PERSON
		d?: DOCUMENT

	$\where$

		d? Ï dom checked_out
		(d?, p?) Î permission
		checked_out' = checked_out È {(d?, p?)}

	$\end{schema}$

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

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





		_ $\comp$ _ : (X « Y) ´ (Y « Z) ® (X « Z)
		_ ° _ : (Y « Z) ´ (X « Y) ® (X « Z)

	$\where$

		" Q: X « Y; R: Y « Z ·
		Q $\comp$ R = R ° Q = { x: X; y: Y; z: Z \| x Q y Ù y R z · x $\mapsto$ z }

	$\end{gendef}$

$ Editor' · Insert	Definition of precondition
Û $ left', right': TEXT \| ... · ...	Expand schemas
Û $ left', right': TEXT · ... Ù ...	Restricted $-quantifier
Û pr Ù # ((left ^ á ch? ñ) ^ right) £ maxsize	One-point rule
Û pr Ù # left + # á ch? ñ + # right £ maxsize	# (s ^ t) = # s + #t
Û pr Ù # left + 1 + # right £ maxsize	# á x ñ = 1
Û pr Ù # left + # right < maxsize	Arithmetic