Z test page

This page looks best when this and this X are about the same size: X. See these viewing tips.

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

Logic	`true false ₁ let`
Sets etc.	`= { } \| \ first second if then else`
Relations	`dom ran ^~ ⁺ ^* R id`
Functions
Numbers etc.	`₁ + - * div mod < > .. min max # ₁`
Sequences	`seq seq₁ iseq head tail last front rev in disjoint partition`
	`squash prefix suffix`
Bags	`bag count items`
Schema calc.	`[ \| ] ; . >> \ pre`
Conventions	`? ! '`

Z paragraphs

Inline math

ConsoleOp $\defs$ SelectDisplay $\lor$ SelectPatientList $\lor$ SelectFieldList $\lor$ ... $\lor$ 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 $\fun$ VALUE
	$\end{axdef}$

ACCUMULATION == counter $\fun$ VALUE

PRESCRIPTION == prescrip $\fun$ VALUE

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

	$\where$

		$\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)
	$\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



		$\Delta$ Documents
		p?: PERSON
		d?: DOCUMENT

	$\where$

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

	$\end{schema}$

Generic definition box

`Q R`	-	Relational composition: `Q` composed with `R`
`R Q`	-	Backward relational composition, same as `Q 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)

	$\where$

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

	$\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.

Cross references

Miscellaneous

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