# Z test page

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

Links to more Z examples.

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

## Symbols

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

 Logic true false 1 let Sets etc. = { } | \ first second if then else Relations dom ran ~ + * R id Functions Numbers etc. 1 + - * div mod < > .. min max # 1 Sequences seq seq1 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 SelectDisplay SelectPatientList SelectFieldList ... 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 VALUE

 ACCUMULATION == counter VALUE PRESCRIPTION == prescrip VALUE

 Preset: studies (FIELD PRESCRIPTION) Prescribed: patients (FIELD PRESCRIPTION) Accumulated: patients (FIELD ACCUMULATION) s: studies no_field dom (Preset s) p: patients no_field dom (Prescribed p) dom (Prescribed p) = dom (Accumulated p)

### Schema boxes

 TherapyControl Session Field Intlk ... Console

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

 CheckOut Documents p?: PERSON d?: DOCUMENT d? dom checked_out (d?, p?) permission checked_out' = checked_out {(d?, p?)}

### Generic definition box

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

 [X,Y,Z] _ _ : (X Y) (Y Z) (X Z) _ _ : (Y Z) (X Y) (X Z) Q: X Y; R: Y Z Q R = R Q = {  x: X; y: Y; z: Z | x Q y y R z x z  }

### 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.