The oz package^{∗}

edited by Sebastian Rahtz S.Rahtz@elsevier.co.uk

1997/09/17

Contents

1 Introduction 1 1.1 Modification History . . . . . . . . . . . . . . . . . . . . . . . . . . 2

2 Z fonts 3

3 Z symbols 5

4 Utility macros for Z symbols 6

5 Amstex symbol definitions 7

6 Object-Z Notations 17

7 Z environments 17 7.1 Margin stack . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 7.2 Utility macros for Z environments . . . . . . . . . . . . . . . . . . 19

7.2.1 Format and control macros . . . . . . . . . . . . . . . . . . 19 7.3 Macros for margins . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 7.4 Macros for drawing boxes . . . . . . . . . . . . . . . . . . . . . . . 20 7.5 Macros for setting up Z environments . . . . . . . . . . . . . . . . 20 7.6 Spacing commands . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 7.7 Environment-breaking commands . . . . . . . . . . . . . . . . . . . 22

8 Utility macros for Object-Z 22

9 Non-box environments 23 9.1 Boxed environments . . . . . . . . . . . . . . . . . . . . . . . . . . 23 9.2 Other environments . . . . . . . . . . . . . . . . . . . . . . . . . . 25

1 Introduction

This file provides macros to type Object Z schemas.

∗This file has version number 2.43, last revised 1997/09/17.

1.1 Modification History

The original zed.sty file was written by Mike Spivey. These macros have been extensively modified to include extra symbols and environments for Object-Z and now have little resemblence to the original macros. Mike Spivey has also extended his macros along different lines for Z — the latest version of macros are called fuzz.sty and come with a syntax checker for Z. They can be purchased for a small

fee from: mike@prg.oxford.ac.uk

87  original zed.sty file — Mike Spivey

88 modified to include extra symbols and environ-

ments — Paul King

88 modified to include macros for UQ editor — Ray

Neucom

May 89 modified to include object-oriented constructs —

PK

Jun 89 modified to automatically change Z symbol size

— PK

27 Jul 89 removed spurious space from \@setsize — PK
3 Aug 89 adjust style of equation number field — PK

24 Aug 89 add optional field to topline and zedline for proofs

— PK

15 Sep 89 added extra qed symbols, updated classcom and

comment — PK

25 Sep 89 renamed z@[bB]ig to z[bB]ig and changed tempo-

ral symbols — PK

30 Sep 89 added \znewpage, \Infrule, removed space above state box — PK

12 Mar 90 changed \@setsize to work better for double-

spaced text — PK

31 Mar 90 added definition for @ and \bool and redefined

‘;’ — PK

9 May 90 changed \sdef to \varsdef, \sdef & \defs to

Spivey’s latest — PK

27 May 90 added \c{n}{text} — a tab like \t{n} with text

at left — PK

29 May 90 added ‘corners’ to boxes and \zedcornerheight

— PK

11 Jul 90 added \rename*[y/x] and \zseq \zset ...,

changed \zeq \zimp — PK

2 Aug 90 added subseq — PK
2 Aug 90 added \subseq, \iseq - PK

9 Nov 90 changed \M to hopefully interact better with spac-

ing — PK

18 Dec 90 changed to new AMS 2.0 fonts - PK (with help from Adrian Lee)

11 Feb 91 added \poly\widen and modified \gendef - PK

10 Apr 91 added \fuzzcompatible - PK

1 Apr 91 added \gengendef - Steve Atkinson
24 Feb 92 changed to work with NFSS — Sebastian Rahtz
29 Dec 92 changed to work with NFSS2 — Sebastian Rahtz
23 Dec 93 checked for \LaTeXe

6 Jan 94 checked again for \LaTeXe with help of David

Carlisle

7 Apr 94 checked again, bundle files added

13 Aug 94 removed hard-wired number of family for math letters removed definition of \c as it prevents cedilla from working

22 Feb 95 updated for AMSLaTeX 2.1 and Lucida compat-

ibility

30 Aug 96 added Object-Z notations in Section 2A - SA

17 Sep 97 re-added \zedbaselinestretch (L^{A}TEX 2ε) – David Leadbetter

Please post any updates that you may make to this file to: Formal Methods Group – fmg@it.uq.edu.au

1 ⟨∗package⟩

2 \NeedsTeXFormat{LaTeX2e}[1994/12/01]
3 \ProvidesPackage{oz}[\filedate\space\fileversion\space Object Z macros]

The L^{A}TEX 2ε parbox code is much more complicated, so we get back a simpler world from L^{A}TEX209.

4 \def\oz@parbox{\@ifnextchar [{\oz@iparbox}{\oz@iparbox[c]}}
5 \long\def\oz@iparbox[#1]#2#3{\leavevmode \@pboxswfalse
6 \if #1b\vbox
7  \else \if #1t\vtop
8  \else \vbox
9  %\ifmmode \vcenter \else \@pboxswtrue $\vcenter \fi
10  \fi
11  \fi
12 {\hsize #2\@parboxrestore #3}
13  %\if@pboxsw \m@th$\fi

14 }

2 Z fonts

The AMS extra symbol fonts are loaded if we are not using Lucida New Math. Note: msam and msbm sometimes called euxm and euym respectively NOTE: the new AMSFONTS 2.0 call these fonts msam and msbm repectively (the fonts below need to be renamed if you want to use the new fonts)

15 \@ifpackageloaded{lucbr}{}{%
16 \DeclareMathVersion{oz}
17 \SetMathAlphabet{\mathrm}{oz}{\encodingdefault}{\rmdefault}{m}{n}%
18 \SetMathAlphabet{\mathbf}{oz}{\encodingdefault}{\rmdefault}{bx}{n}%
19 \SetMathAlphabet{\mathsf}{oz}{\encodingdefault}{\sfdefault}{m}{n}%
20 \DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}%

21 \DeclareSymbolFontAlphabet{\mathrm}{operators}
22 \DeclareSymbolFontAlphabet{\mathit}{letters}
23 \DeclareSymbolFontAlphabet{\mathcal}{symbols}
24 \DeclareSymbolFontAlphabet{\ozit}{italics}
25 \DeclareSymbolFont{lasy}{U}{lasy}{m}{n}
26 \DeclareSymbolFont{AMSa}{U}{msa}{m}{n}
27 \DeclareSymbolFont{AMSb}{U}{msb}{m}{n}
28 \let\mho\undefined
29 \let\Join\undefined
30 \let\Box\undefined
31 \let\Diamond\undefined
32 \let\leadsto\undefined
33 \let\sqsubset\undefined
34 \let\sqsupset\undefined
35 \let\lhd\undefined
36 \let\unlhd\undefined
37 \let\rhd\undefined
38 \let\unrhd\undefined
39 \DeclareMathSymbol{\mho}{\mathord}{lasy}{"30}
40 \DeclareMathSymbol{\Join}{\mathrel}{lasy}{"31}
41 \DeclareMathSymbol{\Box}{\mathord}{lasy}{"32}
42 \DeclareMathSymbol{\Diamond}{\mathord}{lasy}{"33}
43 \DeclareMathSymbol{\leadsto}{\mathrel}{lasy}{"3B}
44 \DeclareMathSymbol{\sqsubset}{\mathrel}{lasy}{"3C}
45 \DeclareMathSymbol{\sqsupset}{\mathrel}{lasy}{"3D}
46 \DeclareMathSymbol{\lhd}{\mathrel}{lasy}{"01}
47 \DeclareMathSymbol{\unlhd}{\mathrel}{lasy}{"02}
48 \DeclareMathSymbol{\rhd}{\mathrel}{lasy}{"03}
49 \DeclareMathSymbol{\unrhd}{\mathrel}{lasy}{"04}
50 \DeclareSymbolFontAlphabet{\mathbb}{AMSb}
51 \DeclareSymbolFontAlphabet{\bbold}{AMSb}
52 \mathversion{oz}

53 }

Allow change of size within schemas. This is a sod to get right; my principle (eventually!) was to go out of math temporarily, change size, go into an inner math, do the business, then get out of math and back to outer math.

54 \newbox\strutbox@
55 \def\strut@{\copy\strutbox@}
56 \addto@hook\every@math@size{%
57  \setbox\strutbox@\hbox{\lower.5\normallineskiplimit
58 \vbox{\kern-\normallineskiplimit\copy\strutbox}}}

59

60 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
61 % NOTE: bBigg is used to define the font size for zbig etc
62 % however it defines these as fixed sizes.
63 % The 209 definitions set the font size dependent on the
64 % current point size.

65 %

66 % Hence in 209 you can do \Large\cnj and the symbol is bigger
67 % But in 2e it remains a fixed size!

68 %

69 % This is a problem for the Object-Z operators as originally
70 % defined in the 209 oz.sty `96 file.

71 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

72

73 \def\bBigg@#1#2{%
74 \mbox{\ifcase#1\or\large\or\Large\or\LARGE\or\small\or\footnotesize\fi
75 $#2$}\nulldelimiterspace\z@ \m@th}
76 \addto@hook\every@math@size{\setbox\z@\vbox{\hbox{$($}\kern\z@}%
77 \big@size 1.2\ht\z@}
78 \newdimen\big@size
79 \def\zBIG{\bBigg@{3}}
80 \def\zBig{\bBigg@{2}}
81 \def\zbig{\bBigg@{1}}
82 \def\zsmall{\bBigg@{4}}
83 \def\zSmall{\bBigg@{5}}

WORD STYLES these need handling a bit differently in NFSS from the original.

84 \def\String#1{\hbox{`\texttt{#1}'}}
85 \def\STRING#1{\hbox{``\texttt{#1}''}}
86 \def\infix#1{\z@rel{{\underline{#1}}}}
87 \def\word#1{\z@op{#1}}
88 \def\keyword#1{\z@op{\mbox{\textrm{#1}}}}
89 \def\boldword#1{\z@op{\mbox{\textbf{#1}}}}
90 \def\underword#1{\z@op{{\underline{#1}}}}
91 \def\underkeyword#1{\z@op{{\underline{\mbox{\textrm{#1}}}}}}
92 \def\underboldword#1{\z@op{{\underline{\mbox{\textbf{#1}}}}}}

3 Z symbols

The mathcodes for the letters A, ..., Z, a, ..., z are changed to generate text italic rather than math italic by default. This makes multi-letter identifiers look better. The mathcode for character c is set to "7000 (variable family) + "400 (text italic) + c.

93 \def\@setmcodes#1#2#3{{\count0=#1 \count1=#3
94  \loop \global\mathcode\count0=\count1 \ifnum \count0<#2
95  \advance\count0 by1 \advance\count1 by1 \repeat}}

Use \hexnumber@\symitalics in case other families are loaded before. (from D. Roegel, July 13, 1994)

96 \@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41}
97 \@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61}

Also, the mathcode for semicolon is set to "8000, so it behaves as an active character in math mode; it is defined to insert a thick space. \semicolon is a semicolon as an ordinary symbol.

98 \let\@mc=\mathchardef
99 \mathcode`\;="8000 % Makes ; active in math mode
100 {\catcode`\;=\active \gdef;{\semicolon\;}}
101 \@mc\semicolon="603B

4 Utility macros for Z symbols

\z@op makes a large math operator
\z@rel makes a math relation
\z@bin makes a binary operator

Each use a mathstrut to defeat TeX’s vertical adjustment. \z@bigXXX is a big version of symbol

102 \def\z@op#1{\mathop{\mathstrut{#1}}\nolimits}
103 \def\z@bin#1{\mathbin{\mathstrut{#1}}}
104 \def\z@rel#1{\mathrel{\mathstrut{#1}}}

105 %

106 \def\z@bigop#1{\z@op{\zbig{#1}}}
107 \def\z@bigbin#1{\z@bin{\zbig{#1}}}
108 \def\z@bigrel#1{\z@rel{\zbig{#1}}}

109 %

110 \def\z@Bigop#1{\z@op{\zBig{#1}}}
111 \def\z@Bigbin#1{\z@bin{\zBig{#1}}}
112 \def\z@Bigrel#1{\z@rel{\zBig{#1}}}

113 %

114 \def\z@smallop#1{\z@op{\zsmall{#1}}}
115 \def\z@smallbin#1{\z@bin{\zsmall{#1}}}
116 \def\z@smallrel#1{\z@rel{\zsmall{#1}}}

This underscore doesn’t have the little kern — you get an italic correction anyway in math mode.

117 \def\_{\leavevmode \vbox{\hrule width0.4em}}

Save \q as \xq for quantifiers q.

118 \let\xforall=\forall
119 \let\xexists=\exists
120 \let\xlambda=\lambda
121 \let\xmu=\mu

Save other symbols

122 \let\xsucc\succ
123 \let\xprec\prec
124 \let\dotaccent=\dot
125 \let\sectionsymbol=\S
126 \let\integral=\int
127 \let\product\prod

\p and \f make arrows with 1 and 2 crossings resp.

128 \def\p#1{\mathrel{\ooalign{\hfil$\mapstochar\mkern 5mu$\hfil\cr$#1$}}}
129 \def\f#1{\mathrel{\ooalign{\hfil
130  $\mapstochar\mkern 3mu\mapstochar\mkern 5mu$\hfil\cr$#1$}}}
131 \@ifpackageloaded{lucbr}{%
132 \DeclareMathSymbol{\doublebarwedge}{\mathbin}{symbols}{"D4}
133 \DeclareMathSymbol{\lll}{\mathrel}{letters}{"DE}
134 \DeclareMathSymbol{\ggg}{\mathrel}{letters}{"DF}
135 \DeclareMathSymbol{\eth}{\mathrel}{operators}{"F0}
136 }{%

5 Amstex symbol definitions

Do these before Z symbols so that we can use them in our special symbols. AMSa font:

137 \let\rightleftharpoons\undefined
138 \let\angle\undefined
139 \DeclareMathSymbol\boxdot{\mathbin}{AMSa}{"00}
140 \DeclareMathSymbol\boxplus{\mathbin}{AMSa}{"01}
141 \DeclareMathSymbol\boxtimes{\mathbin}{AMSa}{"02}
142 \DeclareMathSymbol\square{\mathord}{AMSa}{"03}
143 \DeclareMathSymbol\blacksquare{\mathord}{AMSa}{"04}
144 \DeclareMathSymbol\centerdot{\mathbin}{AMSa}{"05}
145 \DeclareMathSymbol\lozenge{\mathord}{AMSa}{"06}
146 \DeclareMathSymbol\blacklozenge{\mathord}{AMSa}{"07}
147 \DeclareMathSymbol\circlearrowright{\mathrel}{AMSa}{"08}
148 \DeclareMathSymbol\circlearrowleft{\mathrel}{AMSa}{"09}
149 \DeclareMathSymbol\rightleftharpoons{\mathrel}{AMSa}{"0A}
150 \DeclareMathSymbol\leftrightharpoons{\mathrel}{AMSa}{"0B}
151 \DeclareMathSymbol\boxminus{\mathbin}{AMSa}{"0C}
152 \DeclareMathSymbol\Vdash{\mathrel}{AMSa}{"0D}
153 \DeclareMathSymbol\Vvdash{\mathrel}{AMSa}{"0E}
154 \DeclareMathSymbol\vDash{\mathrel}{AMSa}{"0F}
155 \DeclareMathSymbol\twoheadrightarrow{\mathrel}{AMSa}{"10}
156 \DeclareMathSymbol\twoheadleftarrow{\mathrel}{AMSa}{"11}
157 \DeclareMathSymbol\leftleftarrows{\mathrel}{AMSa}{"12}
158 \DeclareMathSymbol\rightrightarrows{\mathrel}{AMSa}{"13}
159 \DeclareMathSymbol\upuparrows{\mathrel}{AMSa}{"14}
160 \DeclareMathSymbol\downdownarrows{\mathrel}{AMSa}{"15}
161 \DeclareMathSymbol\upharpoonright{\mathrel}{AMSa}{"16}
162 \DeclareMathSymbol\downharpoonright{\mathrel}{AMSa}{"17}
163 \DeclareMathSymbol\upharpoonleft{\mathrel}{AMSa}{"18}
164 \DeclareMathSymbol\downharpoonleft{\mathrel}{AMSa}{"19}
165 \DeclareMathSymbol\rightarrowtail{\mathrel}{AMSa}{"1A}
166 \DeclareMathSymbol\leftarrowtail{\mathrel}{AMSa}{"1B}
167 \DeclareMathSymbol\leftrightarrows{\mathrel}{AMSa}{"1C}
168 \DeclareMathSymbol\rightleftarrows{\mathrel}{AMSa}{"1D}
169 \DeclareMathSymbol\Lsh{\mathrel}{AMSa}{"1E}
170 \DeclareMathSymbol\Rsh{\mathrel}{AMSa}{"1F}
171 \DeclareMathSymbol\rightsquigarrow{\mathrel}{AMSa}{"20}
172 \DeclareMathSymbol\leftrightsquigarrow{\mathrel}{AMSa}{"21}
173 \DeclareMathSymbol\looparrowleft{\mathrel}{AMSa}{"22}
174 \DeclareMathSymbol\looparrowright{\mathrel}{AMSa}{"23}
175 \DeclareMathSymbol\circeq{\mathrel}{AMSa}{"24}
176 \DeclareMathSymbol\succsim{\mathrel}{AMSa}{"25}
177 \DeclareMathSymbol\gtrsim{\mathrel}{AMSa}{"26}
178 \DeclareMathSymbol\gtrapprox{\mathrel}{AMSa}{"27}
179 \DeclareMathSymbol\multimap{\mathrel}{AMSa}{"28}
180 \DeclareMathSymbol\therefore{\mathrel}{AMSa}{"29}
181 \DeclareMathSymbol\because{\mathrel}{AMSa}{"2A}
182 \DeclareMathSymbol\doteqdot{\mathrel}{AMSa}{"2B}
183 \DeclareMathSymbol\triangleq{\mathrel}{AMSa}{"2C}
184 \DeclareMathSymbol\precsim{\mathrel}{AMSa}{"2D}
185 \DeclareMathSymbol\lesssim{\mathrel}{AMSa}{"2E}
186 \DeclareMathSymbol\lessapprox{\mathrel}{AMSa}{"2F}

187 \DeclareMathSymbol\eqslantless{\mathrel}{AMSa}{"30}
188 \DeclareMathSymbol\eqslantgtr{\mathrel}{AMSa}{"31}
189 \DeclareMathSymbol\curlyeqprec{\mathrel}{AMSa}{"32}
190 \DeclareMathSymbol\curlyeqsucc{\mathrel}{AMSa}{"33}
191 \DeclareMathSymbol\preccurlyeq{\mathrel}{AMSa}{"34}
192 \DeclareMathSymbol\leqq{\mathrel}{AMSa}{"35}
193 \DeclareMathSymbol\leqslant{\mathrel}{AMSa}{"36}
194 \DeclareMathSymbol\lessgtr{\mathrel}{AMSa}{"37}
195 \DeclareMathSymbol\backprime{\mathord}{AMSa}{"38}
196 \DeclareMathSymbol\risingdotseq{\mathrel}{AMSa}{"3A}
197 \DeclareMathSymbol\fallingdotseq{\mathrel}{AMSa}{"3B}
198 \DeclareMathSymbol\succcurlyeq{\mathrel}{AMSa}{"3C}
199 \DeclareMathSymbol\geqq{\mathrel}{AMSa}{"3D}
200 \DeclareMathSymbol\geqslant{\mathrel}{AMSa}{"3E}
201 \DeclareMathSymbol\gtrless{\mathrel}{AMSa}{"3F}
202 \DeclareMathSymbol\sqsubset{\mathrel}{AMSa}{"40}
203 \DeclareMathSymbol\sqsupset{\mathrel}{AMSa}{"41}
204 \DeclareMathSymbol\vartriangleright{\mathrel}{AMSa}{"42}
205 \DeclareMathSymbol\vartriangleleft{\mathrel}{AMSa}{"43}
206 \DeclareMathSymbol\trianglerighteq{\mathrel}{AMSa}{"44}
207 \DeclareMathSymbol\trianglelefteq{\mathrel}{AMSa}{"45}
208 \DeclareMathSymbol\bigstar{\mathord}{AMSa}{"46}
209 \DeclareMathSymbol\between{\mathrel}{AMSa}{"47}
210 \DeclareMathSymbol\blacktriangledown{\mathord}{AMSa}{"48}
211 \DeclareMathSymbol\blacktriangleright{\mathrel}{AMSa}{"49}
212 \DeclareMathSymbol\blacktriangleleft{\mathrel}{AMSa}{"4A}
213 \DeclareMathSymbol\vartriangle{\mathord}{AMSa}{"4D}
214 \DeclareMathSymbol\blacktriangle{\mathord}{AMSa}{"4E}
215 \DeclareMathSymbol\triangledown{\mathord}{AMSa}{"4F}
216 \DeclareMathSymbol\eqcirc{\mathrel}{AMSa}{"50}
217 \DeclareMathSymbol\lesseqgtr{\mathrel}{AMSa}{"51}
218 \DeclareMathSymbol\gtreqless{\mathrel}{AMSa}{"52}
219 \DeclareMathSymbol\lesseqqgtr{\mathrel}{AMSa}{"53}
220 \DeclareMathSymbol\gtreqqless{\mathrel}{AMSa}{"54}
221 \DeclareMathSymbol\Rrightarrow{\mathrel}{AMSa}{"56}
222 \DeclareMathSymbol\Lleftarrow{\mathrel}{AMSa}{"57}
223 \DeclareMathSymbol\veebar{\mathbin}{AMSa}{"59}
224 \DeclareMathSymbol\barwedge{\mathbin}{AMSa}{"5A}
225 \DeclareMathSymbol\doublebarwedge{\mathbin}{AMSa}{"5B}
226 \DeclareMathSymbol\angle{\mathord}{AMSa}{"5C}
227 \DeclareMathSymbol\measuredangle{\mathord}{AMSa}{"5D}
228 \DeclareMathSymbol\sphericalangle{\mathord}{AMSa}{"5E}
229 \DeclareMathSymbol\varpropto{\mathrel}{AMSa}{"5F}
230 \DeclareMathSymbol\smallsmile{\mathrel}{AMSa}{"60}
231 \DeclareMathSymbol\smallfrown{\mathrel}{AMSa}{"61}
232 \DeclareMathSymbol\Subset{\mathrel}{AMSa}{"62}
233 \DeclareMathSymbol\Supset{\mathrel}{AMSa}{"63}
234 \DeclareMathSymbol\Cup{\mathbin}{AMSa}{"64}
235 \DeclareMathSymbol\Cap{\mathbin}{AMSa}{"65}
236 \DeclareMathSymbol\curlywedge{\mathbin}{AMSa}{"66}
237 \DeclareMathSymbol\curlyvee{\mathbin}{AMSa}{"67}
238 \DeclareMathSymbol\leftthreetimes{\mathbin}{AMSa}{"68}
239 \DeclareMathSymbol\rightthreetimes{\mathbin}{AMSa}{"69}
240 \DeclareMathSymbol\subseteqq{\mathrel}{AMSa}{"6A}

241 \DeclareMathSymbol\supseteqq{\mathrel}{AMSa}{"6B}
242 \DeclareMathSymbol\bumpeq{\mathrel}{AMSa}{"6C}
243 \DeclareMathSymbol\Bumpeq{\mathrel}{AMSa}{"6D}
244 \DeclareMathSymbol\lll{\mathrel}{AMSa}{"6E}
245 \DeclareMathSymbol\ggg{\mathrel}{AMSa}{"6F}
246 \DeclareMathDelimiter\ulcorner{4}{AMSa}{"70}{AMSa}{"70}
247 \DeclareMathDelimiter\urcorner{5}{AMSa}{"71}{AMSa}{"71}
248 \DeclareMathDelimiter\llcorner{4}{AMSa}{"78}{AMSa}{"78}
249 \DeclareMathDelimiter\lrcorner{5}{AMSa}{"79}{AMSa}{"79}
250 \xdef\yen  {\noexpand\mathhexbox\hexnumber@\symAMSa 55 }
251 \xdef\checkmark{\noexpand\mathhexbox\hexnumber@\symAMSa 58 }
252 \xdef\circledR {\noexpand\mathhexbox\hexnumber@\symAMSa 72 }
253 \xdef\maltese  {\noexpand\mathhexbox\hexnumber@\symAMSa 7A }
254 \DeclareMathSymbol\circledS{\mathord}{AMSa}{"73}
255 \DeclareMathSymbol\pitchfork{\mathrel}{AMSa}{"74}
256 \DeclareMathSymbol\dotplus{\mathbin}{AMSa}{"75}
257 \DeclareMathSymbol\backsim{\mathrel}{AMSa}{"76}
258 \DeclareMathSymbol\backsimeq{\mathrel}{AMSa}{"77}
259 \DeclareMathSymbol\complement{\mathord}{AMSa}{"7B}
260 \DeclareMathSymbol\intercal{\mathbin}{AMSa}{"7C}
261 \DeclareMathSymbol\circledcirc{\mathbin}{AMSa}{"7D}
262 \DeclareMathSymbol\circledast{\mathbin}{AMSa}{"7E}
263 \DeclareMathSymbol\circleddash{\mathbin}{AMSa}{"7F}

AMSb font:

264 \DeclareMathSymbol\lvertneqq{\mathrel}{AMSb}{"00}
265 \DeclareMathSymbol\gvertneqq{\mathrel}{AMSb}{"01}
266 \DeclareMathSymbol\nleq{\mathrel}{AMSb}{"02}
267 \DeclareMathSymbol\ngeq{\mathrel}{AMSb}{"03}
268 \DeclareMathSymbol\nless{\mathrel}{AMSb}{"04}
269 \DeclareMathSymbol\ngtr{\mathrel}{AMSb}{"05}
270 \DeclareMathSymbol\nprec{\mathrel}{AMSb}{"06}
271 \DeclareMathSymbol\nsucc{\mathrel}{AMSb}{"07}
272 \DeclareMathSymbol\lneqq{\mathrel}{AMSb}{"08}
273 \DeclareMathSymbol\gneqq{\mathrel}{AMSb}{"09}
274 \DeclareMathSymbol\nleqslant{\mathrel}{AMSb}{"0A}
275 \DeclareMathSymbol\ngeqslant{\mathrel}{AMSb}{"0B}
276 \DeclareMathSymbol\lneq{\mathrel}{AMSb}{"0C}
277 \DeclareMathSymbol\gneq{\mathrel}{AMSb}{"0D}
278 \DeclareMathSymbol\npreceq{\mathrel}{AMSb}{"0E}
279 \DeclareMathSymbol\nsucceq{\mathrel}{AMSb}{"0F}
280 \DeclareMathSymbol\precnsim{\mathrel}{AMSb}{"10}
281 \DeclareMathSymbol\succnsim{\mathrel}{AMSb}{"11}
282 \DeclareMathSymbol\lnsim{\mathrel}{AMSb}{"12}
283 \DeclareMathSymbol\gnsim{\mathrel}{AMSb}{"13}
284 \DeclareMathSymbol\nleqq{\mathrel}{AMSb}{"14}
285 \DeclareMathSymbol\ngeqq{\mathrel}{AMSb}{"15}
286 \DeclareMathSymbol\precneqq{\mathrel}{AMSb}{"16}
287 \DeclareMathSymbol\succneqq{\mathrel}{AMSb}{"17}
288 \DeclareMathSymbol\precnapprox{\mathrel}{AMSb}{"18}
289 \DeclareMathSymbol\succnapprox{\mathrel}{AMSb}{"19}
290 \DeclareMathSymbol\lnapprox{\mathrel}{AMSb}{"1A}
291 \DeclareMathSymbol\gnapprox{\mathrel}{AMSb}{"1B}
292 \DeclareMathSymbol\nsim{\mathrel}{AMSb}{"1C}

293 \DeclareMathSymbol\ncong{\mathrel}{AMSb}{"1D}
294 %\DeclareMathSymbol\varsubsetneq{\mathrel}{AMSb}{"20}
295 %\DeclareMathSymbol\varsupsetneq{\mathrel}{AMSb}{"21}
296 \DeclareMathSymbol\nsubseteqq{\mathrel}{AMSb}{"22}
297 \DeclareMathSymbol\nsupseteqq{\mathrel}{AMSb}{"23}
298 \DeclareMathSymbol\subsetneqq{\mathrel}{AMSb}{"24}
299 \DeclareMathSymbol\supsetneqq{\mathrel}{AMSb}{"25}
300 %\DeclareMathSymbol\varsubsetneqq{\mathrel}{AMSb}{"26}
301 %\DeclareMathSymbol\varsupsetneqq{\mathrel}{AMSb}{"27}
302 \DeclareMathSymbol\subsetneq{\mathrel}{AMSb}{"28}
303 \DeclareMathSymbol\supsetneq{\mathrel}{AMSb}{"29}
304 \DeclareMathSymbol\nsubseteq{\mathrel}{AMSb}{"2A}
305 \DeclareMathSymbol\nsupseteq{\mathrel}{AMSb}{"2B}
306 \DeclareMathSymbol\nparallel{\mathrel}{AMSb}{"2C}
307 \DeclareMathSymbol\nmid{\mathrel}{AMSb}{"2D}
308 \DeclareMathSymbol\nshortmid{\mathrel}{AMSb}{"2E}
309 \DeclareMathSymbol\nshortparallel{\mathrel}{AMSb}{"2F}
310 \DeclareMathSymbol\nvdash{\mathrel}{AMSb}{"30}
311 \DeclareMathSymbol\nVdash{\mathrel}{AMSb}{"31}
312 \DeclareMathSymbol\nvDash{\mathrel}{AMSb}{"32}
313 \DeclareMathSymbol\nVDash{\mathrel}{AMSb}{"33}
314 \DeclareMathSymbol\ntrianglerighteq{\mathrel}{AMSb}{"34}
315 \DeclareMathSymbol\ntrianglelefteq{\mathrel}{AMSb}{"35}
316 \DeclareMathSymbol\ntriangleleft{\mathrel}{AMSb}{"36}
317 \DeclareMathSymbol\ntriangleright{\mathrel}{AMSb}{"37}
318 \DeclareMathSymbol\nleftarrow{\mathrel}{AMSb}{"38}
319 \DeclareMathSymbol\nrightarrow{\mathrel}{AMSb}{"39}
320 \DeclareMathSymbol\nLeftarrow{\mathrel}{AMSb}{"3A}
321 \DeclareMathSymbol\nRightarrow{\mathrel}{AMSb}{"3B}
322 \DeclareMathSymbol\nLeftrightarrow{\mathrel}{AMSb}{"3C}
323 \DeclareMathSymbol\nleftrightarrow{\mathrel}{AMSb}{"3D}
324 \DeclareMathSymbol\divideontimes{\mathbin}{AMSb}{"3E}
325 \DeclareMathSymbol\varnothing{\mathord}{AMSb}{"3F}
326 \DeclareMathSymbol\mho{\mathord}{AMSb}{"66}
327 \DeclareMathSymbol\eth{\mathord}{AMSb}{"67}
328 \DeclareMathSymbol\eqsim{\mathrel}{AMSb}{"68}
329 \DeclareMathSymbol\beth{\mathord}{AMSb}{"69}
330 \DeclareMathSymbol\gimel{\mathord}{AMSb}{"6A}
331 \DeclareMathSymbol\daleth{\mathord}{AMSb}{"6B}
332 \DeclareMathSymbol\lessdot{\mathrel}{AMSb}{"6C}
333 \DeclareMathSymbol\gtrdot{\mathrel}{AMSb}{"6D}
334 \DeclareMathSymbol\ltimes{\mathbin}{AMSb}{"6E}
335 \DeclareMathSymbol\rtimes{\mathbin}{AMSb}{"6F}
336 \DeclareMathSymbol\shortmid{\mathrel}{AMSb}{"70}
337 \DeclareMathSymbol\shortparallel{\mathrel}{AMSb}{"71}
338 \DeclareMathSymbol\smallsetminus{\mathbin}{AMSb}{"72}
339 \DeclareMathSymbol\thicksim{\mathrel}{AMSb}{"73}
340 \DeclareMathSymbol\thickapprox{\mathrel}{AMSb}{"74}
341 \DeclareMathSymbol\approxeq{\mathrel}{AMSb}{"75}
342 \DeclareMathSymbol\succapprox{\mathrel}{AMSb}{"76}
343 \DeclareMathSymbol\precapprox{\mathrel}{AMSb}{"77}
344 \DeclareMathSymbol\curvearrowleft{\mathrel}{AMSb}{"78}
345 \DeclareMathSymbol\curvearrowright{\mathrel}{AMSb}{"79}
346 \DeclareMathSymbol\digamma{\mathord}{AMSb}{"7A}

347 \DeclareMathSymbol\varkappa{\mathord}{AMSb}{"7B}
348 \DeclareMathSymbol\hslash{\mathord}{AMSb}{"7D}
349 \DeclareMathSymbol\hbar{\mathord}{AMSb}{"7E}
350 \DeclareMathSymbol\backepsilon{\mathrel}{AMSb}{"7F}

351 }

352 \def\interleave{{\parallel\!\!\vert}}
353 \def\shortinterleave{\z@rel{\mathord\shortmid\mathord\shortparallel}}
354 \def\napprox{\not\approx}
355 \let\restriction\upharpoonright
356 \let\Doteq\doteqdot
357 \let\doublecup\Cup
358 \let\llless\lll
359 \let\gggtr\ggg
360 \let\doublecap\Cap

Numbers

361 \def \nat   {{\mathbb N}}
362 \def \integer   {{\mathbb Z}}
363 \def \natone    {{\mathbb N}_1}
364 \def \real  {{\mathbb R}}
365 \def \bool  {{\mathbb B}}
366 \let \divides   \div
367 \def \div   {\z@bin{\mathrm{div}}}
368 \def \mod   {\z@bin{\mathrm{mod}}}
369 \def \succ  {\word{succ}}
370 \def \expon {^}

aliases

371 \let \num   \integer
372 \let \nplus \natone

Logic

373 \def \lnot  {\neg\;}
374 \def \land  {\z@rel{\wedge}}
375 \def \lor   {\z@rel{\vee}}
376 \let \imp   \Rightarrow
377 \let\iff    \Leftrightarrow
378 \def \all   {\z@op{\xforall}}
379 \def \exi   {\z@op{\xexists}}
380 \def \exione    {\exists_1}
381 \@ifpackageloaded{lucbr}{%
382 \DeclareMathSymbol{\nexi}{0}{arrows}{"20}
383 }{%
384 \DeclareMathSymbol{\nexi}{\mathord}{AMSb}{"40}

385 }

386 \def \dot   {\z@rel{\bullet}}
387 \def \true  {\keyword{true}}
388 \def \false {\keyword{false}}
389 \let \cond  \rightarrow

aliases

390 \let \spot  \dot
391 \mathcode`\@="8000% make @ active in mathmode
392 {\catcode`\@=\active \gdef@{\dot}}
393 \let \implies   \imp
394 \let \forall    \all

395 \let \exists    \exi
396 \let \nexists   \nexi

SETS

397 \let \emptyset  \varnothing
398 \def \varemptyset  {\{\,\}}
399 \def \pset  {\z@op{\mathbb P}}
400 \def \psetone   {\pset_1}
401 \def \fset  {\z@op{\mathbb F}}
402 \def \fsetone   {\fset_1}
403 \def \sset  {\z@op{\mathbb S}}
404 \let \mem   \in
405 \def \nem   {\not\mem}
406 \def \uni   {\z@bin\cup}
407 \def \int   {\z@bin\cap}
408 \let \prod  \times
409 \def \min   {\word{min}}
410 \def \max   {\word{max}}
411 \def \duni  {\z@Bigop{\lower0.25ex\hbox{$\uni$}}}
412 \def \dint  {\z@Bigop{\lower0.25ex\hbox{$\int$}}}
413 \def \upto  {\z@bin{\ldotp\ldotp}}
414 \let \psubs \subset
415 \let \subs  \subseteq
416 \let \psups \supset
417 \let \sups  \supseteq
418 \def \diff  {\z@bin{\backslash}}

aliases

419 \let \cross \prod
420 \let \notin \nem
421 \let \nmem  \nem
422 \let \union \uni
423 \let \inter \int
424 \let \power \pset
425 \let \finset    \fset
426 \let \dunion    \duni
427 \let \dinter    \dint

428 %

RELATIONS & FUNCTIONS

429 \def \lambda    {\z@op{\xlambda}}
430 \def \mu    {\z@op{\xmu}}
431 \def \dom   {\keyword{dom}}
432 \def \ran   {\keyword{ran}}
433 \def \id    {\keyword{id}}
434 \@ifpackageloaded{lucbr}{%
435 \DeclareMathSymbol{\dres}{\mathbin}{letters}{"2F}
436 \DeclareMathSymbol{\rres}{\mathbin}{letters}{"2E}
437 }{%
438 \DeclareMathSymbol{\dres}{\mathbin}{AMSa}{"43}
439 \DeclareMathSymbol{\rres}{\mathbin}{AMSa}{"42}

440 }

441 \def \dsub  {\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\dres}}}
442 \def \rsub  {\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\rres}}}
443 \let \fovr  \oplus

444 \let \cmp   \circ
445 \def \fcmp  {\mathbin{\raise 0.6ex\hbox{\oalign{\hfil$\scriptscriptstyle
446  \mathrm{o}$\hfil\cr\hfil$\scriptscriptstyle\mathrm{9}$\hfil}}}}
447 \def \inv   {^\sim}
448 \def \limg  {(\!|}
449 \def \rimg  {|\!)}
450 \let \map   \mapsto
451 \let \rel   \leftrightarrow
452 \let \tfun  \rightarrow
453 \let \tinj  \rightarrowtail
454 \def \tsur  {\mathrel{\ooalign{$\tfun$\hfil\cr$\mkern4mu\tfun$}}}
455 \def \pfun  {\p\tfun}
456 \def \pinj  {\p\tinj}
457 \def \psur  {\p\tsur}
458 \def \ffun  {\f\tfun}
459 \def \finj  {\f\tinj}
460 \def \bij   {\mathrel{\ooalign{$\tinj$\hfil\cr$\mkern5mu\tfun$}}}
461 \def \tcl   {^+}
462 \def \rtcl  {^*}
463 \def \iter  {^}

aliases

464 \let \comp  \fcmp
465 \let \ndres \dsub
466 \let \nrres \rsub
467 \let \fun   \tfun
468 \let \inj   \tinj
469 \let \surj  \tsur
470 \let \psurj \psur
471 \let \llless    \lll
472 \let \gggtr \ggg
473 \def \interleave    {{\parallel\!\!\vert}}
474 \def \shortinterleave   {\z@rel{\mathord\shortmid\mathord\shortparallel}}
475 \let \restriction   \upharpoonright
476 \def \napprox   {\not\approx}

SEQUENCES

477 \def \seq   {\keyword{seq}}
478 \def \iseq {\keyword{iseq}}
479 \def \seqone    {\seq_1}
480 \def \emptyseq  {\lseq\,\rseq}
481 \let \lseq  \langle
482 \let \rseq  \rangle
483 \def \head  {\word{head}}
484 \def \tail  {\word{tail}}
485 \def \front {\word{front}}
486 \def \last  {\word{last}}
487 \def \rev   {\word{rev}}
488 \def \squash    {\word{squash}}
489 \def \next  {\keyword{next}}
490 \def \inseq {\keyword{in}}
491 \@ifpackageloaded{lucbr}{%
492 \DeclareMathSymbol{\sres}{2}{arrows}{"75}
493 \DeclareMathSymbol{\ires}{2}{arrows}{"76}
494 \DeclareMathSymbol{\@@cat}{\mathbin}{operators}{"5F}

495 }{%
496 \DeclareMathSymbol{\@@cat}{\mathbin}{AMSa}{"61}
497 \DeclareMathSymbol{\sres}{\mathbin}{AMSa}{"16}
498 \DeclareMathSymbol{\ires}{\mathbin}{AMSa}{"18}

499 }

500 \def \cat   {\mathbin{\raise 0.8ex\hbox{$\mathchar\@@cat$}}}
501 \def \ssub  {\z@bin{\rlap{$-$}{\sres}}}
502 \def \isub  {\z@bin{\rlap{$-$}{\ires}}}
503 \def \dcat  {\z@op{\cat/}}
504 \def \dovr  {\z@op{\fovr/}}
505 \def \dcmp  {\z@op{\fcmp/}}
506 \let \prefix    \subseteq
507 \def \suffix    {\keyword{suffix}}
508 \def \seqi  {\keyword{seq_\infty}}
509 \def \partitions    {\keyword{partitions}}
510 \def \partition {\keyword{partitions}}
511 \def \disjoint  {\keyword{disjoint}}
512 \def \subseq    {\keyword{subseq}}

aliases

513 \let \filter    \sres

Schemas:

514 \def \lsch  {\z@bigop{[}}
515 \def \rsch  {\z@bigop{]}}
516 \def \dparallel {\z@bigop{\parallel}\limits}
517 \def \zand  {\z@bigbin\land}
518 \def \zor   {\z@bigbin\lor}
519 \def \zcmp  {\z@bigbin\fcmp}
520 \def \zexi  {\z@bigop\exists}
521 \def \zall  {\z@bigop\forall}
522 \def \znot  {\z@bigop\neg}
523 \def \zbar  {\z@bigbin\cbar}
524 \def \zfor  {/}
525 \def \zhide {\z@bigbin\backslash}
526 \def \zimp  {\z@bigrel\imp}
527 \def \zeq   {\z@bigrel\iff}
528 \def \zovr  {\z@bigrel\oplus}
529 \def \zpipe {\z@bigbin{\mathord>\!\!\mathord>}}
530 \def \pre   {\keyword{pre}}
531 \def \pred  {\keyword{pred}}
532 \def \post  {\keyword{post}}
533 \def \zproject  {\z@bigbin\sres}
534 \def\rename{\@ifnextchar*{\z@rename}{\z@@rename}}
535 \def\z@rename*[#1/#2]{\left[#1 \over #2\right]}
536 \def\z@@rename[#1/#2]{\left[#1 \zfor #2\right]}

aliases

537 \let \project   \zproject
538 \let \import    \sres
539 \let \semi  \zcmp
540 \let \hide  \zhide

BAGS

541 \let\buni\uplus
542 \def \emptybag  {\lbag\:\rbag}

543 \def \lbag  {[\![}
544 \def \rbag  {]\!]}
545 \def \bag   {\keyword{bag}}
546 \def \items {\word{items}}
547 \let \inbag \inseq
548 \def \bagcount  {\word{count}}

Definitions & declarations

549 \def \ddef  {\z@rel{\;::=\;}}
550 \def \bbar  {\z@bigrel{|}}
551 \let \cbar  \mid
552 \def \lang  {\langle\!\langle}
553 \def \rang  {\rangle\!\rangle}
554 \def \sdef  {\z@rel{\widehat=}}
555 \def \defs  {\z@smallrel{==}}
556 \def \varsdef   {\z@rel\triangleq}

aliases

557 \let \sdefs \sdef
558 \mathcode`\|=\mid
559 \let \ldata \lang
560 \let \rdata \rang

MISCELLANEOUS

561 \def \lblot {\langle\!|}
562 \def \rblot {|\!\rangle}
563 \def \IMP   {\boldword{Import}}
564 \let \env   \Rrightarrow
565 \def \zlet  {\boldword{let}}
566 \def \zin   {\boldword{in}}
567 \def \zwhere    {\boldword{where}}

QZED SUPPORT

568 \def\HOLE{\z@op{\hbox{$\lll\star\star\star\ggg$}}}
569 \def\landd{} % to support qzed editor
570 \def\semid{} % to support qzed editor
571 \def\qzed{\ifz@inclass\else\zed\fi}
572 \def\endqzed{\ifz@inclass\else\endzed\fi}

CLASSES

573 \def\qua{\mbox{::}}
574 \def\redef{\mbox{\textbf{~redef}}}
575 \def\Init{I\!\mbox{\footnotesize\emph{NIT}}}
576 \def\Exit{E\!\mbox{\footnotesize\emph{XIT}}}
577 \def\Internal{I\!\mbox{\footnotesize\emph{NTERNAL}}}
578 \def\Aux{A\!\mbox{\footnotesize\emph{UX}}}
579 \def\intern{\mbox{\textsf{i}}}

PROOFS

580 \def\thrm{\z@rel\vdash}
581 \def\qed{\zsmall\Box}
582 \let\Qed\Box
583 \let\QED\square
584 \def\BLACKQED{\zsmall\blacksquare}
585 \let\ETH\qed

586 \def\TH{\boldword{Theorem}}
587 \def\LE{\boldword{Lemma}}
588 \def\PR{\boldword{Proof}}
589 \def\refines{\z@rel\sqsupseteq}
590 \def\defines{\z@rel\sqsubseteq}
591 \def\weakrefine{\z@rel{\raise0.2ex\rlap{\hbox{$\sqsupset$}}\lower1ex\hbox{$\sim$}}}
592 \def\weakdefine{\z@rel{\raise0.2ex\rlap{\hbox{$\sqsubset$}}\lower1ex\hbox{$\sim$}}}

aliases

593 \let\shows\thrm

OBJECT THEORY

594 \def\childof{\z@rel\xsucc}
595 \def\parentof{\z@rel\xprec}
596 \let\weaksubclass\succsim
597 \let\weaksupclass\precsim
598 \def\hasa{\z@rel{\mathord\xsucc\!\!\!\mathord\xsucc}}
599 \def\instancein{\z@rel{\mathord\xprec\!\!\!\mathord\xprec}}
600 \def\subtype{\z@rel\sqsubset}
601 \def\subtypeeq{\z@rel\sqsubseteq}
602 \def\suptype{\z@rel\sqsupset}
603 \def\suptypeeq{\z@rel\sqsupseteq}

aliases

604 \let\inherits\childof
605 \let\subclass\childof
606 \let\isa\childof
607 \let\supclass\parentof
608 \let\instantiates\hasa
609 \let\islikea\weaksubclass
610 \def\poly{\mathord\downarrow}
611 \def\widen#1{\z@op{{\overline{#1}}}}

TEMPORAL LOGIC

612 \def\atnext{\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\zSmall\bigcirc$}\kern0.01em\zSmall\bigcirc}
613 \def\atlast{\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\kern0.01em\mathord-$}\zSmall\bigcirc}
614 \def\always{\lower0.37ex\hbox{$\zbig\Box$}}
615 \def\uptilnow{\rlap{$\kern0.02em\mathord-$}\lower0.37ex\hbox{$\zbig\Box$}}
616 \def\eventually{\lower0.37ex\hbox{$\zbig\Diamond$}}
617 \def\previously{\rlap{$\kern0.04em\mathord-$}\lower0.37ex\hbox{$\zbig\Diamond$}}

aliases

618 \let\henceforth\always

ORDERS

619 \def \mono  {\keyword{monotonic}}
620 \def \porder    {\keyword{partial\_order}}
621 \def \torder    {\keyword{total\_order}}
622 \newbox\z@combox\newdimen\z@wdcalc
623 \def\comment{\@ifnextchar*{\z@leftcomment}{\z@comment}}
624 \def\z@comment#1{$\z@stopfield\z@addfield\z@startfield$%
625 \global\setbox\z@combox\hbox{\quad[{\sf #1}]}\z@wdcalc=\wd\z@combox%
626 \advance\z@wdcalc by \wd\z@curline\advance\z@wdcalc by \z@curindent%
627 \advance\z@wdcalc by \zedleftsep\advance\z@wdcalc by \zedlinethickness%
628 \advance\z@wdcalc by 2\zedindent\ifdim\z@wdcalc>\displaywidth\\%
629 \fi&\box\z@combox\ignorespaces}
630 \def\z@leftcomment*#1{\hbox{[{\sf #1}]}}

6 Object-Z Notations

KEYWORDS AND KEYSYMBOLS

631 \def \oid {{\bbold O}}
632 \def \self   {\word{self}}
633 \def \contained {\word{contained}}
634 \let \classuni    \uni
635 \def \visibility {\zproject}
636 \def \invisibility {{\project\hspace{-0.63 em}\cross}}

CONTAINMENT AND CONTROL ADORNMENTS

637 \def \cid {{\bigcirc\mbox{\scriptsize{\hspace{-0.78em}}\mbox{\tiny{C}}}}}
638 \def \sid {{\bigcirc\mbox{\scriptsize{\hspace{-0.74em}}\mbox{\tiny{S}}}}}
639 \def \eid {{\bigcirc\mbox{\scriptsize{\hspace{-0.74em}}\mbox{\tiny{E}}}}}

BINARY COMPOSITION OPERATORS

640 \def \pll {~\parallel~}
641 \def \plo {~\parallel_{!}~}
642 \def \sqc {~\semi~}
643 \def \cnj {~\zand~}
644 \def \gch {~[\mbox{\hspace{-0.25mm}}]~}
645 \def \enh {~\dot~}

DISTRIBUTED COMPOSITION OPERATORS

646 % Redefined because of \zbig problem
647 % \def \dsqc {\mbox{{\Large $\zcmp~$}}}
648 \def \dsqc {\mbox{{\Large $\fcmp~$}}}
649 \def \dgch {\mbox{\hspace{-2.5mm}{\Large $\gch$}}}
650 % Redefined because of \zbig problem
651 % \def \dcnj {\mbox{{\Large $\zand$}}}
652 \def \dcnj {\mbox{{\Large $\land$}}}
653 \def \dpll {\mbox{{\Large $\parallel$}}}
654 \def \dplo {\mbox{{\Large $\parallel_{!}$}}}

7 Z environments

7.1 Margin stack

Define a stack of dimensions (50 elements) This can probably be made smaller when qzed filters its TEX output better

655 \newcount\z@stackmin
656 \newcount\z@stackmax
657 \newcount\z@stacktop
658 \newdimen\@gtempa \z@stackmin=\allocationnumber
659 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
660 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
661 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
662 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
663 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
664 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
665 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
666 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
667 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa

668 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
669 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
670 \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
671 \newdimen\@gtempa
672 \z@stackmax=\allocationnumber
673 \dimen\z@stackmin=0pt

Define a box to contain the current line & a variable to contain it’s indentation

674 \newbox\z@curline
675 \newdimen\z@curindent
676 \dimen\z@curindent=0pt

Space between operands of a function application

677 \def\z@space{{}\;{}}

Define a box to contain the current field

678 \newbox\z@curfield

Define a mini-tabbing environment for use inside ‘zed’

679 \def\z@startline{\setbox\z@curline\hbox{}%
680  \global\z@curindent\dimen\z@stacktop
681  \z@startfield\ignorespaces}
682 \def\z@stopline{\z@stopfield
683  \z@addfield
684  \hbox{\hskip\z@curindent \box\z@curline}}

685

686 \def\z@startfield{\global\setbox\z@curfield\hbox\bgroup}
687 \def\z@stopfield{\egroup}
688 \def\z@addfield{\global\setbox\z@curline\hbox{\unhbox
689  \z@curline\unhbox\z@curfield}}

690

691 \def\z@pushmargin{\hbox{\kern0pt}$%
692 \z@stopfield
693 \z@addfield
694 \ifnum \z@stacktop < \z@stackmax
695  \global\advance\z@stacktop \@ne
696 \else
697  \@latexerr{Z margin stack overflow (too many \string\M's)}
698  \@ehd
699 \fi
700 \global\dimen\z@stacktop\z@curindent
701 \global\advance\dimen\z@stacktop \wd\z@curline
702 \z@startfield\ignorespaces
703 $\relax}
704 \def\z@popmargin{\ifnum \z@stacktop > \z@stackmin
705  \global\advance\z@stacktop \m@ne \ignorespaces
706 \else
707  \@latexerr{Z Margin stack underflow (too many \string\O's)}
708  \@ehd
709 \fi}
710 \def\M{\z@pushmargin} \def\O{\z@popmargin} \def\S{\z@space}
711 \z@stacktop\z@stackmin

7.2 Utility macros for Z environments

Here are environments for the various sorts of displays which occur in Z documents. All displays are set flush left, indented by \zedindent, by default \leftmargini. Schemas, etc, are made just wide enough to give equal margins left and right.

Some environments (schema, etc.) must only be split at \zbreak, and others (e.g. argue) may be split arbitrarily. All generate alignment displays, and penalties are used to control page breaks.

7.2.1 Format and control macros

712 \newdimen\zedindent \zedindent=\leftmargini
713 \newdimen\zedleftsep    \zedleftsep=1em
714 \newdimen\zedtab    \zedtab=2em
715 \newdimen\zedbar    \zedbar=8em
716 \newdimen\zedlinethickness  \zedlinethickness=0.4pt
717 \newdimen\zedcornerheight   \zedcornerheight=0pt
718 \newcount\z@cols
719 \newif\ifz@firstline    \z@firstlinefalse
720 \newif\ifz@inclass  \z@inclassfalse
721 \newif\ifz@inenv    \z@inenvfalse
722 \newif\ifz@leftmargin   \z@leftmargintrue
723 \newif\ifz@incols   \z@incolsfalse
724 \newif\ifleftnames  \leftnamesfalse
725 \def\leftschemas{\leftnamestrue}
726 \newif\ifz@inbox    \z@inboxfalse
727 \newskip\zedbaselineskip    \zedbaselineskip\baselineskip
728 \newbox\zstrutbox   \setbox\zstrutbox=\copy\strutbox
729 \def\zstrut{\relax\ifmmode\copy\zstrutbox\else\unhcopy\zstrutbox\fi}
730 \def\zedbaselinestretch{1}

Penalties

731 \newcount\interzedlinepenalty   \interzedlinepenalty=10000  %never break
732 \newcount\preboxpenalty \preboxpenalty=0    %break easily
733 \newcount\forcepagepenalty  \forcepagepenalty=-10000    %always break
734 \interdisplaylinepenalty=100    %break sometimes

Macros for changing the size of schema text

735 \def\zedsize#1{\def\z@size{#1}}
736 \def\z@size{}
737 \newskip\z@adskip\newskip\z@bdskip\newskip\z@adsskip\newskip\z@bdsskip
738 \def\z@changesize{%
739 \z@adskip\abovedisplayskip\z@bdskip\belowdisplayskip% save skips
740 \z@adsskip\abovedisplayshortskip\z@bdsskip\belowdisplayshortskip
741 \z@size % change size
742 \abovedisplayskip\z@adskip\belowdisplayskip\z@bdskip% restore skips
743 \abovedisplayshortskip\z@adsskip\belowdisplayshortskip\z@bdsskip}

744 % 745 %

746 \def\z@zeroskips{\abovedisplayskip\z@\belowdisplayskip\z@
747  \abovedisplayshortskip\z@\belowdisplayshortskip\z@}
748 \def\@setfontsize#1#2#3{\@nomath#1%
749  \ifx\protect\@typeset@protect
750  \let\@currsize#1%
751  \fi

752  \fontsize{#2}{#3}\selectfont
753  \zedbaselineskip#3pt
754  \zedbaselineskip\zedbaselinestretch\zedbaselineskip
755  \setbox\zstrutbox\hbox{\vrule height.7\zedbaselineskip
756  depth.3\zedbaselineskip width\z@}

757 }

7.3 Macros for margins

\z@narrow, \z@wide — make the margins narrower, wider

758 \def\z@narrow{\advance\linewidth by -\zedindent}
759 \def\z@wide{\advance\linewidth by \zedindent}

7.4 Macros for drawing boxes

\z@hrulefill — line with correct thickness

760 \def\z@hrulefill{\leaders\hrule height\zedlinethickness\hfill}

\z@topline draws the top horizontal line of boxed environments \z@dbltopline draws a double ruled top line \z@botline draws the bottom horizontal line of boxed environments \zedline[comment] draws a long horizontal line ending in comment \where draws a short horizontal line

761 \def\z@topline#1{\omit\@ifnextchar[{\z@@topline{#1}}{\z@@topline{#1}[]}}
762 \def\z@@topline#1[#2]{\hbox to\linewidth{\zstrut\ifleftnames\else
763  \vrule height\zedlinethickness width\zedlinethickness
764  \hbox to\zedleftsep{\z@hrulefill}\fi#1\z@hrulefill
765  \smash{\vrule height\zedlinethickness width\zedlinethickness
766  depth\zedcornerheight}\hbox{\sf #2}}\cr}
767 \def\z@dbltopline#1{\omit\@ifnextchar[{\z@@dbltopline{#1}}{\z@@dbltopline{#1}[]}}
768 \def\z@@dbltopline#1[#2]{\z@@topline{#1}[#2]%
769 \noalign{\kern-\baselineskip
770  \kern-\zedlinethickness
771  \kern-\doublerulesep \nobreak}%
772 \omit\z@@topline{\hphantom{#1}}[\hphantom{#2}]%
773 \noalign{\kern\doublerulesep
774  \kern\zedlinethickness \nobreak}}
775 \def\z@botline{\also\omit\hbox to\linewidth{\z@hrulefill
776 \smash{\vrule height\zedcornerheight width\zedlinethickness
777  depth 0pt}}\cr}
778 \def\z@@botline[#1]{\hbox to\linewidth{\vrule\z@hrulefill\hbox{\sf\smash{#1}}}\also}
779 \def\zedline{\also\omit\@ifnextchar[{\z@@botline}{\z@@botline[]}}
780 \def\where{\also \omit \hbox to\zedbar{\z@hrulefill}\cr\also}
781 \let \ST    \where

\z@left is placed at the left of each z line: in non-box environments it will do nothing. in boxed environments it will do a vertical line with the same height as the maximum height of the line.

782 \def\z@left{\ifz@inbox\vrule width\zedlinethickness\hskip\zedleftsep\fi}

7.5 Macros for setting up Z environments

783 \def\z@env{\global\z@firstlinetrue\z@changesize

784 $$

785  \z@inenvtrue
786  \baselineskip\zedbaselineskip
787  \parskip=0pt\lineskip=0pt\z@narrow
788  \advance\displayindent by \zedindent
789  \def\\{\crcr}% Must have \def and not \let for nested alignments.
790  \everycr={\noalign{\ifz@firstline \global\z@firstlinefalse
791  \else \penalty\interzedlinepenalty \fi}}
792  \tabskip=0pt}
793 \def\endz@env{$$
794 \global\@ignoretrue

795 }

Z lines are formated in two (overlapping) columns; the first flush left having the same width as the environment, and, the second flush right ending at the right end of the environment.

796 \def\z@format{\halign to\linewidth\bgroup%
797  \zstrut\z@left\z@startline\ignorespaces$\@lign##$\z@stopline\hfil%
798  \tabskip=0pt plus1fil%
799  &\hbox to 0pt{\hss\@lign##}\tabskip=0pt\cr}
800 \def\z@boxenv{\z@narrow\let\also=\als@ \let\Also=\Als@ \let\ALSO=\ALS@
801  \z@inboxtrue \predisplaypenalty=\preboxpenalty \z@env\z@format}
802 \def\z@outnonbox{\z@outclasscheck\z@leavevmode\z@env}
803 \def\z@inoutbox{\z@leavevmode\z@makeouter\z@inclassfalse\z@boxenv}

7.6 Spacing commands

no vertical glue between abutted lines

804 \def\@but{\noalign{\nointerlineskip}}

no \par extra vertical spacing after Z environments

    \def\z@nopar{\ifz@inclass\else\vskip-\parskip\fi}\def\z@nopar{\global\parskip0pt\global\everypar{\parskip30mm\everypar{}}}
805 \def\z@nopar{\global\@endpetrue}

\z@leavevmode – Enter horizontal mode, taking account of possible interaction with lists and section heads:

1. After a \item, use \indent to get the label (this fails to run in even short labels).

2. After a run-in heading, use \indent.

3. After an ordinary heading, throw away the \everypar tokens, reset

      \@nobreak, and use \noindent with \parskip zero.

4. Otherwise, use \noindent with \parskip zero

Use when entering displayed environments to get correct spacing

806 \def\z@leavevmode{\ifvmode\if@inlabel\indent\else\if@noskipsec\indent\else
807  \if@nobreak\global\@nobreakfalse\everypar={}\fi
808  {\parskip=0pt\noindent}\fi\fi\fi}

extra vertical space in non-box environments

809 \def\also{\crcr\noalign{\vskip\jot}}
810 \def\Also{\crcr\noalign{\vskip2\jot}}
811 \def\ALSO{\Also\Also}

extra vertical space in boxed environments

812 \def\als@{\crcr\@but\omit\vrule height\jot width\zedlinethickness \cr \@but}
813 \def\Als@{\crcr\@but\omit\vrule height2\jot width\zedlinethickness \cr \@but}
814 \def\ALS@{\crcr\@but\omit\vrule height4\jot width\zedlinethickness \cr \@but}

7.7 Environment-breaking commands

815 \def\znewpage{\also\noalign{\penalty\forcepagepenalty}\also}
816 \def\zbreak{\also\noalign{\penalty\interdisplaylinepenalty\vskip-\jot}\also}
817 \def\Zbreak{\also\noalign{\penalty\interdisplaylinepenalty}\also}
818 \def\ZBREAK{\Also\noalign{\penalty\interdisplaylinepenalty}\Also}
819 \def\t#1{\hskip #1\zedtab}
820 %\def\c#1#2{\hbox to #1\zedtab{$#2$\hfil}}
821 \def\flushr#1{\crcr&#1\quad\cr}

8 Utility macros for Object-Z

822 \def\z@inclasscheck{\ifz@inclass\else
823  \@latexerr{This Z environment is only allowed within a class}
824 {Perhaps you forgot to include a \string\begin\string{class\string}
825 somewhere^^Jor you are trying to print a file that needs updating.^^J\@ehc} \fi}
826 \def\z@outclasscheck{\ifz@inclass
827  \@latexerr{This Z environment is not allowed inside a class}
828 {This environment doesn't really make sense within a class.^^J%
829 If you really want it then I'll try my best to fit in in.^^J\@ehc}\else
830 \ifz@inenv \@latexerr{New Z environment declared before previous
831 one is completed}
832 {I suspect that you've forgotten to finish the last environment.^^J%
833 You are trying to nest environments and this can only be done inside classes^^J%
834 besides, the environment you have started isn't valid within classes any way.^^JI suggest that you type \space X <return> \space to quit and then correct your document.}
835 \fi\fi}

836 %

837 \def\z@makeouter{%
838 \ifz@inenv
839 \ifz@inclass\z@inenvfalse
840  \hskip-\zedleftsep \advance\linewidth by -\zedlinethickness
841  \zedindent=\zedleftsep \zedleftsep=0.8\zedleftsep
842  \zedbar=0.8\zedbar \zedtab=0.8\zedtab
843  \oz@parbox{\linewidth}\bgroup
844  \z@zeroskips
845 \else
846 \@latexerr{Incorrect place for Z environment; nesting is
847 allowed only inside classes}
848 {You've either forgotten to finish the last environment,^^J%
849 you've forgotten to include a
850 \string\begin\string{class\string} somewhere^^J%
851 or you are trying to print a file that needs updating.^^J%
852 (Then again, you might just be trying to do something^^J%
853  that the author of these macros didn't intend you to do)^^J\@ehc}
854 \fi
855 \else
856 \bgroup
857 \fi

858 }

860 \def \z@makeinner{\egroup
861 \global\z@curindent\z@

862 } 863 %

864 \def \classbreak{\also\egroup$$\vskip -\ht\zstrutbox
865  \vskip -\abovedisplayskip\vskip -\belowdisplayskip\z@wide\z@boxenv\also}

9 Non-box environments

ZED for non-box multiline formulas

866 \def\zed{\z@outnonbox\z@inboxfalse\z@format}
867 \def\endzed{\crcr\egroup\endz@env}
868 \let\[=\zed
869 \def\]{\crcr\egroup$$\ignorespaces}

ARGUE for algebraic arguments

used for algebraic proofs expressed as extended equations. like zed but with extra spacing between lines Generates an alignment display, which may be split across pages.

870 \def\argue{\z@outnonbox\interzedlinepenalty=\interdisplaylinepenalty
871  \openup 1\jot \z@format
872  \noalign{\vskip-\jot}}% equal vspace above and below argue display
873 \let\endargue=\endzed

INFRULE for inference rules

used for inference rules. The horizontal line is generated by \derive: an optional argument contains the side-conditions of the rule.

874 \def\infrule{\z@outnonbox\halign\bgroup
875  \zstrut\quad$\@lign##$\quad\hfil&\quad\@lign##\hfil\cr}
876 \let\endinfrule=\endzed
877 \def\derive{\crcr\also\@but\omit\z@hrulefill%
878  \@ifnextchar[{\z@sidecondition}{\cr\also\@but}}
879 \def\Derive{\crcr\also\@but\omit\z@hrulefill\cr\@but
880  \noalign{\kern-\dp\zstrutbox
881  \kern\doublerulesep \nobreak}%
882 \omit\derive}
883 \def\z@sidecondition[#1]{&$\smash{\lower 0.2ex\hbox{$[\;#1\;]$}}$\cr\also\@but}

SYNTAX for syntax rules

‘syntax’ environment: used for syntax rules — even (once!) for VDM.

884 \def\syntax{\z@outnonbox\halign\bgroup
885  \zstrut$\@lign##$\hfil &\hfil$\@lign{}##{}$\hfil
886  &$\@lign##$\hfil &\qquad\@lign-- ##\hfil\cr}
887 \let\endsyntax=\endzed

9.1 Boxed environments

SCHEMA schema definitions

888 \def\schema#1{\z@inoutbox\z@topline{$\,#1\,$}}
889 \def\endschema{\z@botline \endzed \z@makeinner \z@nopar}

ANONSCHEMA schema with no name

890 \@namedef{anonschema}{\leftnamesfalse\z@inoutbox\z@topline{}}
891 \expandafter\let\csname endanonschema\endcsname=\endschema

GENSCHEMA generic schema definitions

892 \def\genschema#1#2{\z@inoutbox\z@topline{$\,#1\:[#2]\,$}}
893 \let\endgenschema=\endschema

AXDEF ‘liberal’ axiomatic definitions

894 \def\axdef{\z@inoutbox}
895 \def\endaxdef{\endzed\z@makeinner}

UNIQDEF ‘unique’ axiomatic definitions

896 \def\uniqdef{\leftnamesfalse\z@inoutbox\z@dbltopline{}}
897 \let\enduniqdef=\endschema

GENDEF ’generic’ axiomatic definitions

HACK TO MAKE IT COMPATIBLE WITH FUZZ.STY

898 \def\gendef{\@ifnextchar[{\z@gendef}{\z@@gendef}}
899 \def\z@gendef[#1]{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,[#1]\,$}}
900 \def\z@@gendef#1{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,[#1]\,$}}
901 \let\endgendef=\endschema

GENGENDEF generic contents ’generic’ axiomatic definitions Hack to provide syntax-oriented display boxes

902 \def\gengendef{\@ifnextchar[{\z@gengendef}{\z@@gengendef}}
903 \def\z@gengendef[#1]{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,#1\,$}}
904 \def\z@@gengendef#1{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,#1\,$}}
905 \let\endgengendef=\endschema

CLASS

906 \def\class#1{\z@leavevmode\z@makeouter\z@inclasstrue
907  \z@boxenv\z@topline{$\,#1\,$}}
908 \let\endclass\endschema

OP

909 \def\op{\z@inclasscheck\schema}
910 \let\endop\endschema

STATE

911 \def\state{\z@inclasscheck\vbox\bgroup\vskip-\ht\zstrutbox\vbox\bgroup\hbox\bgroup\@nameuse{anonschema}}
912 \def\endstate{\endschema\egroup\egroup\egroup}

INIT

913 \def\init{\z@inclasscheck\schema{\Init}}
914 \let\endinit\endschema

CONST

915 \let\const\axdef
916 \let\endconst\endaxdef

TYPE

917 \def\type{\z@inclasscheck}
918 \let\endtype\relax

9.2 Other environments

SIDEBYSIDE

This should support an arbitary number of columns \zedindent’s proportion of \linewidth gives a practical limit

919 \def\sidebyside{\@ifnextchar[{\z@columns}{\z@columns[2]}}
920 \def\z@columns[#1]{\z@leavevmode\z@cols#1 \z@makeouter\z@narrow%
921  $$\lineskip=0pt\z@incolstrue
922  \predisplaysize\maxdimen
923  \ifz@leftmargin\hskip-\zedindent\z@leftmarginfalse\fi
924  \setbox0=\hbox to \linewidth\bgroup\z@zeroskips%
925  \divide\zedbar by \z@cols \divide\zedleftsep by \z@cols
926  \divide\zedtab by \z@cols \divide\linewidth by \z@cols
927 \oz@parbox[t]{\linewidth}\bgroup\z@wide}

928 %

929 \def\nextside{\egroup\hss\oz@parbox[t]{\linewidth}\bgroup\z@wide}

930 %

931 \newdimen\z@temp
932 \def\endsidebyside{\egroup\egroup
933  \z@temp\ht0 \advance\z@temp by \dp0\advance\z@temp by-\dp\zstrutbox
934  \hbox{\raise\z@temp\box0}\endz@env\z@makeinner\z@nopar}

ZPAR

935 \def\zpar{\z@leavevmode
936  \ifz@inenv\z@inclasstrue\fi% fudge to let zpar in all boxes
937  \z@makeouter\z@changesize
938  \advance\linewidth by -\z@curindent
939  \advance\linewidth by -\wd\z@curline
940  \hskip-\wd\z@curline\advance\linewidth by -\zedindent$$
941  \ifz@leftmargin\hskip-\zedindent\fi% adjustment for first column
942  \advance\displayindent by \zedindent
943  \advance\displaywidth by -\zedindent
944  \advance\displayindent by \z@curindent
945  \advance\displayindent by \wd\z@curline
946  \advance\displaywidth by -\z@curindent
947  \advance\displaywidth by -\wd\z@curline
948  \global\setbox\z@curline\hbox{}
949  \z@narrow\oz@parbox[b]{\linewidth}\bgroup\hfil\break}
950 \def\endzpar{\egroup$$\z@makeinner\z@nopar}

CLASSCOM

951 \def \classcom{\zpar\sf}
952 \let \endclasscom=\endzpar

PROOF

953 \def\proof{\zpar$\PR$\zpar}
954 \def\endproof{\endzpar\endzpar}

Additional auxiliary macros

955 \def\zseq#1{\lseq #1 \rseq}
956 \def\zset#1{\{ #1 \}}
957 \def\zimg#1{\limg #1 \rimg}
958 \def\zsch#1{\lsch #1 \rsch}
959 \def\zimgset#1{\zimg\zset{#1}}

OZ FUZZ

    \defs == \sdef \defs
960 \def\fuzzcompatible{%
961 \let\defs\sdef
962 \let\empty\emptyset

963 } 964 % 965 ⟨/package⟩