From e0c6872cf40896c7be36b11dcc744620f10adf1d Mon Sep 17 00:00:00 2001 From: Norbert Preining Date: Mon, 2 Sep 2019 13:46:59 +0900 Subject: Initial commit --- macros/latex/contrib/objectz/catalog | 7 + macros/latex/contrib/objectz/makefile | 6 + macros/latex/contrib/objectz/manifest | 9 + macros/latex/contrib/objectz/oz.dtx | 1613 ++++++++++++++++++++++++++++++ macros/latex/contrib/objectz/oz.ins | 53 + macros/latex/contrib/objectz/ozguide.pdf | Bin 0 -> 279519 bytes macros/latex/contrib/objectz/ozguide.tex | 1311 ++++++++++++++++++++++++ macros/latex/contrib/objectz/oztest.tex | 206 ++++ macros/latex/contrib/objectz/readme | 45 + 9 files changed, 3250 insertions(+) create mode 100644 macros/latex/contrib/objectz/catalog create mode 100644 macros/latex/contrib/objectz/makefile create mode 100644 macros/latex/contrib/objectz/manifest create mode 100644 macros/latex/contrib/objectz/oz.dtx create mode 100644 macros/latex/contrib/objectz/oz.ins create mode 100644 macros/latex/contrib/objectz/ozguide.pdf create mode 100644 macros/latex/contrib/objectz/ozguide.tex create mode 100644 macros/latex/contrib/objectz/oztest.tex create mode 100644 macros/latex/contrib/objectz/readme (limited to 'macros/latex/contrib/objectz') diff --git a/macros/latex/contrib/objectz/catalog b/macros/latex/contrib/objectz/catalog new file mode 100644 index 0000000000..7edc81a9fc --- /dev/null +++ b/macros/latex/contrib/objectz/catalog @@ -0,0 +1,7 @@ +Name: objectz +Problems-To: s.rahtz@elsevier.co.uk +Author: Sebastian Rahtz +Date: 199r/01/06 +Version: 2.42 +Description: LaTeX package for typesetting Object Z schemas + diff --git a/macros/latex/contrib/objectz/makefile b/macros/latex/contrib/objectz/makefile new file mode 100644 index 0000000000..edb8e0f58a --- /dev/null +++ b/macros/latex/contrib/objectz/makefile @@ -0,0 +1,6 @@ +oz: + tex oz.ins + latex oz.dtx + +clean: + -rm *.aux *.toc *.sty *.dvi *.log *.tmp diff --git a/macros/latex/contrib/objectz/manifest b/macros/latex/contrib/objectz/manifest new file mode 100644 index 0000000000..e68ae4938e --- /dev/null +++ b/macros/latex/contrib/objectz/manifest @@ -0,0 +1,9 @@ +total 112 +-rw-r--r-- 1 srahtz 191 Aug 6 10:27 catalog +-rw-r--r-- 1 srahtz 79 Aug 6 10:27 makefile +-rw-r--r-- 1 srahtz 0 Jan 7 11:49 manifest +-rw-r--r-- 1 srahtz 54861 Nov 22 11:12 oz.dtx +-rw-r--r-- 1 srahtz 1272 Aug 6 10:27 oz.ins +-rw-r--r-- 1 srahtz 41883 Aug 6 10:27 ozguide.tex +-rw-r--r-- 1 srahtz 10865 Aug 6 10:27 oztest.tex +-rw-r--r-- 1 srahtz 1763 Jan 7 11:45 readme diff --git a/macros/latex/contrib/objectz/oz.dtx b/macros/latex/contrib/objectz/oz.dtx new file mode 100644 index 0000000000..e272cf1572 --- /dev/null +++ b/macros/latex/contrib/objectz/oz.dtx @@ -0,0 +1,1613 @@ +\def\fileversion{2.46} +\def\filedate{1999/05/24} +\def\docdate {1994/08/13} +% +% \iffalse +%% File: oz.dtx Copyright (C) 1995-1999 Sebastian Rahtz +% Permission is hereby granted, free of charge, to any person obtaining +% a copy of this software and associated documentation files (the +% ``Software''), to deal in the Software without restriction, including +% without limitation the rights to use, copy, modify, merge, publish, +% distribute, sublicense, and/or sell copies of the Software, and to +% permit persons to whom the Software is furnished to do so, subject to +% the following conditions: +% +% The above copyright notice and this permission notice shall be included +% in all copies or substantial portions of the Software. +% +% THE SOFTWARE IS PROVIDED ``AS IS'', WITHOUT WARRANTY OF ANY KIND, EXPRESS +% OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +% MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. +% IN NO EVENT SHALL SEBASTIAN RAHTZ BE LIABLE FOR ANY CLAIM, DAMAGES OR +% OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, +% ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR +% OTHER DEALINGS IN THE SOFTWARE. +% +%<*driver> +\documentclass{ltxdoc} +\begin{document} + \title{The \textsf{oz} package\thanks{This file + has version number \fileversion, last + revised \filedate.}} + \author{edited by Sebastian Rahtz\\S.Rahtz@elsevier.co.uk} + \date{\filedate} + \maketitle + \tableofcontents + \DocInput{oz.dtx} +\end{document} +% +% \fi +% \CheckSum{3387} +% +% \section{Introduction} +% +% This file provides macros to typeset Object Z schemas. +%\subsection{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: +% \texttt{mike@prg.oxford.ac.uk} +% +% \begin{quote} +% \begin{tabular}{lp{.6\textwidth}} +% 87 &original zed.sty file --- Mike Spivey\\ +% 88 &modified to include extra symbols and environments --- +% 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 temporal 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| \& |\def|s 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\\ +% \end{tabular} +% +% \begin{tabular}{lp{.6\textwidth}} +% 9 Nov 90 &changed |\M| to hopefully interact better with spacing --- +% 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 compatibility\\ +% 30 Aug 96 &added Object-Z notations in Section 2A - SA\\ +% 17 Sep 97 &re-added |\zedbaselinestretch| -- David Leadbetter\\ +% 20 July 98 &|state| environment can be used in |sidebyside| \\ +% &changed to work with |slides| class -- DL\\ +% 4 Nov 98 & fixed |\zedbaselinestretch| -- DL\\ +% 17 Nov 98 & fixed |\Init|, etc -- DL\\ +% 24 May 99 & removed extra space output by |\fontsize| -- Ian Hayes and DL +% \end{tabular} +% \end{quote} +% +%\subsection{Known Problems} +% +%\begin{enumerate} +% \item |\bBigg| defines |\zBig|, etc as fixed font sizes - +% in the original oz.sty (for \LaTeX 2.09) these sizing commands change +% the font size relative to the current font size (so a |\zBig| +% in the scope of a |\large| is bigger than a |\zBig| +% in the scope of a |\normalsize|); +% \item |sidebyside| works very poorly with the |class| environment +% - indentation of operation schemas is wrong; +% \item the |calc| package is needed for |\zedbaselinestretch|. +%\end{enumerate} +% +% +%\subsection{The Object-Z Homepage} +% +% The Object-Z homepage (http://svrc.it.uq.edu.au/Object-Z/) contains: +% +% \begin{itemize} +% \item Papers and Tech-reports on Object-Z; +% \item {\bf wizard} - the Object-Z type checker. +% \end{itemize} +% +% \noindent Please post any updates that you may make to this file to the +% Formal Methods Group -- fmg@it.uq.edu.au +% +% +% +% \newpage +% +% \StopEventually{} +% +% \begin{macrocode} +%<*package> +\NeedsTeXFormat{LaTeX2e}[1994/12/01] +\ProvidesPackage{oz}[\filedate\space\fileversion\space Object Z macros] +\message{`Object-Z Macros' \fileversion\space <\filedate>} +\RequirePackage{calc} +% \end{macrocode} +% The \LaTeXe\ parbox code is much more complicated, so we get back +% a simpler world from \LaTeX 209. +% \begin{macrocode} +\def\oz@parbox{\@ifnextchar [{\oz@iparbox}{\oz@iparbox[c]}} +\long\def\oz@iparbox[#1]#2#3{\leavevmode \@pboxswfalse + \if #1b\vbox + \else \if #1t\vtop + \else \vbox + %\ifmmode \vcenter \else \@pboxswtrue $\vcenter \fi + \fi + \fi +{\hsize #2\@parboxrestore #3} + %\if@pboxsw \m@th$\fi +} +% \end{macrocode} +% +%\section{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) +% +% \begin{macrocode} +\@ifpackageloaded{lucbr}{}{% +\DeclareMathVersion{oz} +\SetMathAlphabet{\mathrm}{oz}{\encodingdefault}{\rmdefault}{m}{n}% +\SetMathAlphabet{\mathbf}{oz}{\encodingdefault}{\rmdefault}{bx}{n}% +\SetMathAlphabet{\mathsf}{oz}{\encodingdefault}{\sfdefault}{m}{n}% +\DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}% +\DeclareSymbolFontAlphabet{\mathrm}{operators} +\DeclareSymbolFontAlphabet{\mathit}{letters} +\DeclareSymbolFontAlphabet{\mathcal}{symbols} +\DeclareSymbolFontAlphabet{\ozit}{italics} +\DeclareSymbolFont{lasy}{U}{lasy}{m}{n} +\DeclareSymbolFont{AMSa}{U}{msa}{m}{n} +\DeclareSymbolFont{AMSb}{U}{msb}{m}{n} +\let\mho\undefined +\let\Join\undefined +\let\Box\undefined +\let\Diamond\undefined +\let\leadsto\undefined +\let\sqsubset\undefined +\let\sqsupset\undefined +\let\lhd\undefined +\let\unlhd\undefined +\let\rhd\undefined +\let\unrhd\undefined +\DeclareMathSymbol{\mho}{\mathord}{lasy}{"30} +\DeclareMathSymbol{\Join}{\mathrel}{lasy}{"31} +\DeclareMathSymbol{\Box}{\mathord}{lasy}{"32} +\DeclareMathSymbol{\Diamond}{\mathord}{lasy}{"33} +\DeclareMathSymbol{\leadsto}{\mathrel}{lasy}{"3B} +\DeclareMathSymbol{\sqsubset}{\mathrel}{lasy}{"3C} +\DeclareMathSymbol{\sqsupset}{\mathrel}{lasy}{"3D} +\DeclareMathSymbol{\lhd}{\mathrel}{lasy}{"01} +\DeclareMathSymbol{\unlhd}{\mathrel}{lasy}{"02} +\DeclareMathSymbol{\rhd}{\mathrel}{lasy}{"03} +\DeclareMathSymbol{\unrhd}{\mathrel}{lasy}{"04} +\DeclareSymbolFontAlphabet{\mathbb}{AMSb} +\DeclareSymbolFontAlphabet{\bbold}{AMSb} +\mathversion{oz} +} +% \end{macrocode} +% +% 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. +% +% \begin{macrocode} +\newbox\strutbox@ +\def\strut@{\copy\strutbox@} +\addto@hook\every@math@size{% + \setbox\strutbox@\hbox{\lower.5\normallineskiplimit + \vbox{\kern-\normallineskiplimit\copy\strutbox}}} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% NOTE: bBigg is used to define the font size for zbig etc +%% however it defines these as fixed sizes. +%% The 209 definitions set the font size dependent on the +%% current point size. +%% +%% Hence in 209 you can do \Large\cnj and the symbol is bigger +%% But in 2e it remains a fixed size! +%% +%% This is a problem for the Object-Z operators as originally +%% defined in the 209 oz.sty `96 file. +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\def\bBigg@#1#2{% +\mbox{\ifcase#1\or\large\or\Large\or\LARGE\or\small\or\footnotesize\fi +$#2$}\nulldelimiterspace\z@ \m@th} +\addto@hook\every@math@size{\setbox\z@\vbox{\hbox{$($}\kern\z@}% + \big@size 1.2\ht\z@} +\newdimen\big@size +\def\zBIG{\bBigg@{3}} +\def\zBig{\bBigg@{2}} +\def\zbig{\bBigg@{1}} +\def\zsmall{\bBigg@{4}} +\def\zSmall{\bBigg@{5}} +% \end{macrocode} +% +% WORD STYLES +% these need handling a bit differently in NFSS from the original. +% +% \begin{macrocode} +\def\String#1{\hbox{`\texttt{#1}'}} +\def\STRING#1{\hbox{``\texttt{#1}''}} +\def\infix#1{\z@rel{{\underline{#1}}}} +\def\word#1{\z@op{#1}} +\def\keyword#1{\z@op{\mbox{\textrm{#1}}}} +\def\boldword#1{\z@op{\mbox{\textbf{#1}}}} +\def\underword#1{\z@op{{\underline{#1}}}} +\def\underkeyword#1{\z@op{{\underline{\mbox{\textrm{#1}}}}}} +\def\underboldword#1{\z@op{{\underline{\mbox{\textbf{#1}}}}}} +% \end{macrocode} +% +%\section{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|. +% +% \begin{macrocode} +\def\@setmcodes#1#2#3{{\count0=#1 \count1=#3 + \loop \global\mathcode\count0=\count1 \ifnum \count0<#2 + \advance\count0 by1 \advance\count1 by1 \repeat}} +% \end{macrocode} +% Use |\hexnumber@\symitalics| +% in case other families are loaded before. +% (from D. Roegel, July 13, 1994) +% \begin{macrocode} +\@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41} +\@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61} +% \end{macrocode} +% +% 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. +% +% \begin{macrocode} +\let\@mc=\mathchardef +\mathcode`\;="8000 % Makes ; active in math mode +{\catcode`\;=\active \gdef;{\semicolon\;}} +\@mc\semicolon="603B +% \end{macrocode} +% +%\section{Utility macros for Z symbols} +%\begin{tabular}{ll} +% |\z@op |& makes a large math operator\\ +% |\z@rel|& makes a math relation\\ +% |\z@bin|& makes a binary operator\\ +%\end{tabular} +% +% Each use a mathstrut to defeat TeX's vertical adjustment. +% |\z@bigXXX| is a big version of symbol +% +% \begin{macrocode} +\def\z@op#1{\mathop{\mathstrut{#1}}\nolimits} +\def\z@bin#1{\mathbin{\mathstrut{#1}}} +\def\z@rel#1{\mathrel{\mathstrut{#1}}} +% +\def\z@bigop#1{\z@op{\zbig{#1}}} +\def\z@bigbin#1{\z@bin{\zbig{#1}}} +\def\z@bigrel#1{\z@rel{\zbig{#1}}} +% +\def\z@Bigop#1{\z@op{\zBig{#1}}} +\def\z@Bigbin#1{\z@bin{\zBig{#1}}} +\def\z@Bigrel#1{\z@rel{\zBig{#1}}} +% +\def\z@smallop#1{\z@op{\zsmall{#1}}} +\def\z@smallbin#1{\z@bin{\zsmall{#1}}} +\def\z@smallrel#1{\z@rel{\zsmall{#1}}} +% \end{macrocode} +% +% This underscore doesn't have the little kern --- you get an italic +% correction anyway in math mode. +% \begin{macrocode} +\def\_{\leavevmode \vbox{\hrule width0.4em}} +% \end{macrocode} +% Save |\q| as |\xq| for quantifiers q. +% \begin{macrocode} +\let\xforall=\forall +\let\xexists=\exists +\let\xlambda=\lambda +\let\xmu=\mu +% \end{macrocode} +% Save other symbols +% \begin{macrocode} +\let\xsucc\succ +\let\xprec\prec +\let\dotaccent=\dot +\let\sectionsymbol=\S +\let\integral=\int +\let\product\prod +% \end{macrocode} +% |\p| and |\f| make arrows with 1 and 2 crossings resp. +% \begin{macrocode} +\def\p#1{\mathrel{\ooalign{\hfil$\mapstochar\mkern 5mu$\hfil\cr$#1$}}} +\def\f#1{\mathrel{\ooalign{\hfil + $\mapstochar\mkern 3mu\mapstochar\mkern 5mu$\hfil\cr$#1$}}} +\@ifpackageloaded{lucbr}{% + \DeclareMathSymbol{\doublebarwedge}{\mathbin}{symbols}{"D4} + \DeclareMathSymbol{\lll}{\mathrel}{letters}{"DE} + \DeclareMathSymbol{\ggg}{\mathrel}{letters}{"DF} + \DeclareMathSymbol{\eth}{\mathrel}{operators}{"F0} +}{% +% \end{macrocode} +%\section{Amstex symbol definitions} +% +% Do these before Z symbols so that we can use them in our special symbols. +% AMSa font: +% \begin{macrocode} +\let\rightleftharpoons\undefined +\let\angle\undefined +\DeclareMathSymbol\boxdot{\mathbin}{AMSa}{"00} +\DeclareMathSymbol\boxplus{\mathbin}{AMSa}{"01} +\DeclareMathSymbol\boxtimes{\mathbin}{AMSa}{"02} +\DeclareMathSymbol\square{\mathord}{AMSa}{"03} +\DeclareMathSymbol\blacksquare{\mathord}{AMSa}{"04} +\DeclareMathSymbol\centerdot{\mathbin}{AMSa}{"05} +\DeclareMathSymbol\lozenge{\mathord}{AMSa}{"06} +\DeclareMathSymbol\blacklozenge{\mathord}{AMSa}{"07} +\DeclareMathSymbol\circlearrowright{\mathrel}{AMSa}{"08} +\DeclareMathSymbol\circlearrowleft{\mathrel}{AMSa}{"09} +\DeclareMathSymbol\rightleftharpoons{\mathrel}{AMSa}{"0A} +\DeclareMathSymbol\leftrightharpoons{\mathrel}{AMSa}{"0B} +\DeclareMathSymbol\boxminus{\mathbin}{AMSa}{"0C} +\DeclareMathSymbol\Vdash{\mathrel}{AMSa}{"0D} +\DeclareMathSymbol\Vvdash{\mathrel}{AMSa}{"0E} +\DeclareMathSymbol\vDash{\mathrel}{AMSa}{"0F} +\DeclareMathSymbol\twoheadrightarrow{\mathrel}{AMSa}{"10} +\DeclareMathSymbol\twoheadleftarrow{\mathrel}{AMSa}{"11} +\DeclareMathSymbol\leftleftarrows{\mathrel}{AMSa}{"12} +\DeclareMathSymbol\rightrightarrows{\mathrel}{AMSa}{"13} +\DeclareMathSymbol\upuparrows{\mathrel}{AMSa}{"14} +\DeclareMathSymbol\downdownarrows{\mathrel}{AMSa}{"15} +\DeclareMathSymbol\upharpoonright{\mathrel}{AMSa}{"16} +\DeclareMathSymbol\downharpoonright{\mathrel}{AMSa}{"17} +\DeclareMathSymbol\upharpoonleft{\mathrel}{AMSa}{"18} +\DeclareMathSymbol\downharpoonleft{\mathrel}{AMSa}{"19} +\DeclareMathSymbol\rightarrowtail{\mathrel}{AMSa}{"1A} +\DeclareMathSymbol\leftarrowtail{\mathrel}{AMSa}{"1B} +\DeclareMathSymbol\leftrightarrows{\mathrel}{AMSa}{"1C} +\DeclareMathSymbol\rightleftarrows{\mathrel}{AMSa}{"1D} +\DeclareMathSymbol\Lsh{\mathrel}{AMSa}{"1E} +\DeclareMathSymbol\Rsh{\mathrel}{AMSa}{"1F} +\DeclareMathSymbol\rightsquigarrow{\mathrel}{AMSa}{"20} +\DeclareMathSymbol\leftrightsquigarrow{\mathrel}{AMSa}{"21} +\DeclareMathSymbol\looparrowleft{\mathrel}{AMSa}{"22} +\DeclareMathSymbol\looparrowright{\mathrel}{AMSa}{"23} +\DeclareMathSymbol\circeq{\mathrel}{AMSa}{"24} +\DeclareMathSymbol\succsim{\mathrel}{AMSa}{"25} +\DeclareMathSymbol\gtrsim{\mathrel}{AMSa}{"26} +\DeclareMathSymbol\gtrapprox{\mathrel}{AMSa}{"27} +\DeclareMathSymbol\multimap{\mathrel}{AMSa}{"28} +\DeclareMathSymbol\therefore{\mathrel}{AMSa}{"29} +\DeclareMathSymbol\because{\mathrel}{AMSa}{"2A} +\DeclareMathSymbol\doteqdot{\mathrel}{AMSa}{"2B} +\DeclareMathSymbol\triangleq{\mathrel}{AMSa}{"2C} +\DeclareMathSymbol\precsim{\mathrel}{AMSa}{"2D} +\DeclareMathSymbol\lesssim{\mathrel}{AMSa}{"2E} +\DeclareMathSymbol\lessapprox{\mathrel}{AMSa}{"2F} +\DeclareMathSymbol\eqslantless{\mathrel}{AMSa}{"30} +\DeclareMathSymbol\eqslantgtr{\mathrel}{AMSa}{"31} +\DeclareMathSymbol\curlyeqprec{\mathrel}{AMSa}{"32} +\DeclareMathSymbol\curlyeqsucc{\mathrel}{AMSa}{"33} +\DeclareMathSymbol\preccurlyeq{\mathrel}{AMSa}{"34} +\DeclareMathSymbol\leqq{\mathrel}{AMSa}{"35} +\DeclareMathSymbol\leqslant{\mathrel}{AMSa}{"36} +\DeclareMathSymbol\lessgtr{\mathrel}{AMSa}{"37} +\DeclareMathSymbol\backprime{\mathord}{AMSa}{"38} +\DeclareMathSymbol\risingdotseq{\mathrel}{AMSa}{"3A} +\DeclareMathSymbol\fallingdotseq{\mathrel}{AMSa}{"3B} +\DeclareMathSymbol\succcurlyeq{\mathrel}{AMSa}{"3C} +\DeclareMathSymbol\geqq{\mathrel}{AMSa}{"3D} +\DeclareMathSymbol\geqslant{\mathrel}{AMSa}{"3E} +\DeclareMathSymbol\gtrless{\mathrel}{AMSa}{"3F} +\DeclareMathSymbol\sqsubset{\mathrel}{AMSa}{"40} +\DeclareMathSymbol\sqsupset{\mathrel}{AMSa}{"41} +\DeclareMathSymbol\vartriangleright{\mathrel}{AMSa}{"42} +\DeclareMathSymbol\vartriangleleft{\mathrel}{AMSa}{"43} +\DeclareMathSymbol\trianglerighteq{\mathrel}{AMSa}{"44} +\DeclareMathSymbol\trianglelefteq{\mathrel}{AMSa}{"45} +\DeclareMathSymbol\bigstar{\mathord}{AMSa}{"46} +\DeclareMathSymbol\between{\mathrel}{AMSa}{"47} +\DeclareMathSymbol\blacktriangledown{\mathord}{AMSa}{"48} +\DeclareMathSymbol\blacktriangleright{\mathrel}{AMSa}{"49} +\DeclareMathSymbol\blacktriangleleft{\mathrel}{AMSa}{"4A} +\DeclareMathSymbol\vartriangle{\mathord}{AMSa}{"4D} +\DeclareMathSymbol\blacktriangle{\mathord}{AMSa}{"4E} +\DeclareMathSymbol\triangledown{\mathord}{AMSa}{"4F} +\DeclareMathSymbol\eqcirc{\mathrel}{AMSa}{"50} +\DeclareMathSymbol\lesseqgtr{\mathrel}{AMSa}{"51} +\DeclareMathSymbol\gtreqless{\mathrel}{AMSa}{"52} +\DeclareMathSymbol\lesseqqgtr{\mathrel}{AMSa}{"53} +\DeclareMathSymbol\gtreqqless{\mathrel}{AMSa}{"54} +\DeclareMathSymbol\Rrightarrow{\mathrel}{AMSa}{"56} +\DeclareMathSymbol\Lleftarrow{\mathrel}{AMSa}{"57} +\DeclareMathSymbol\veebar{\mathbin}{AMSa}{"59} +\DeclareMathSymbol\barwedge{\mathbin}{AMSa}{"5A} +\DeclareMathSymbol\doublebarwedge{\mathbin}{AMSa}{"5B} +\DeclareMathSymbol\angle{\mathord}{AMSa}{"5C} +\DeclareMathSymbol\measuredangle{\mathord}{AMSa}{"5D} +\DeclareMathSymbol\sphericalangle{\mathord}{AMSa}{"5E} +\DeclareMathSymbol\varpropto{\mathrel}{AMSa}{"5F} +\DeclareMathSymbol\smallsmile{\mathrel}{AMSa}{"60} +\DeclareMathSymbol\smallfrown{\mathrel}{AMSa}{"61} +\DeclareMathSymbol\Subset{\mathrel}{AMSa}{"62} +\DeclareMathSymbol\Supset{\mathrel}{AMSa}{"63} +\DeclareMathSymbol\Cup{\mathbin}{AMSa}{"64} +\DeclareMathSymbol\Cap{\mathbin}{AMSa}{"65} +\DeclareMathSymbol\curlywedge{\mathbin}{AMSa}{"66} +\DeclareMathSymbol\curlyvee{\mathbin}{AMSa}{"67} +\DeclareMathSymbol\leftthreetimes{\mathbin}{AMSa}{"68} +\DeclareMathSymbol\rightthreetimes{\mathbin}{AMSa}{"69} +\DeclareMathSymbol\subseteqq{\mathrel}{AMSa}{"6A} +\DeclareMathSymbol\supseteqq{\mathrel}{AMSa}{"6B} +\DeclareMathSymbol\bumpeq{\mathrel}{AMSa}{"6C} +\DeclareMathSymbol\Bumpeq{\mathrel}{AMSa}{"6D} +\DeclareMathSymbol\lll{\mathrel}{AMSa}{"6E} +\DeclareMathSymbol\ggg{\mathrel}{AMSa}{"6F} +\DeclareMathDelimiter\ulcorner{4}{AMSa}{"70}{AMSa}{"70} +\DeclareMathDelimiter\urcorner{5}{AMSa}{"71}{AMSa}{"71} +\DeclareMathDelimiter\llcorner{4}{AMSa}{"78}{AMSa}{"78} +\DeclareMathDelimiter\lrcorner{5}{AMSa}{"79}{AMSa}{"79} +\xdef\yen {\noexpand\mathhexbox\hexnumber@\symAMSa 55 } +\xdef\checkmark{\noexpand\mathhexbox\hexnumber@\symAMSa 58 } +\xdef\circledR {\noexpand\mathhexbox\hexnumber@\symAMSa 72 } +\xdef\maltese {\noexpand\mathhexbox\hexnumber@\symAMSa 7A } +\DeclareMathSymbol\circledS{\mathord}{AMSa}{"73} +\DeclareMathSymbol\pitchfork{\mathrel}{AMSa}{"74} +\DeclareMathSymbol\dotplus{\mathbin}{AMSa}{"75} +\DeclareMathSymbol\backsim{\mathrel}{AMSa}{"76} +\DeclareMathSymbol\backsimeq{\mathrel}{AMSa}{"77} +\DeclareMathSymbol\complement{\mathord}{AMSa}{"7B} +\DeclareMathSymbol\intercal{\mathbin}{AMSa}{"7C} +\DeclareMathSymbol\circledcirc{\mathbin}{AMSa}{"7D} +\DeclareMathSymbol\circledast{\mathbin}{AMSa}{"7E} +\DeclareMathSymbol\circleddash{\mathbin}{AMSa}{"7F} +% \end{macrocode} +% +%AMSb font: +% +% \begin{macrocode} +\DeclareMathSymbol\lvertneqq{\mathrel}{AMSb}{"00} +\DeclareMathSymbol\gvertneqq{\mathrel}{AMSb}{"01} +\DeclareMathSymbol\nleq{\mathrel}{AMSb}{"02} +\DeclareMathSymbol\ngeq{\mathrel}{AMSb}{"03} +\DeclareMathSymbol\nless{\mathrel}{AMSb}{"04} +\DeclareMathSymbol\ngtr{\mathrel}{AMSb}{"05} +\DeclareMathSymbol\nprec{\mathrel}{AMSb}{"06} +\DeclareMathSymbol\nsucc{\mathrel}{AMSb}{"07} +\DeclareMathSymbol\lneqq{\mathrel}{AMSb}{"08} +\DeclareMathSymbol\gneqq{\mathrel}{AMSb}{"09} +\DeclareMathSymbol\nleqslant{\mathrel}{AMSb}{"0A} +\DeclareMathSymbol\ngeqslant{\mathrel}{AMSb}{"0B} +\DeclareMathSymbol\lneq{\mathrel}{AMSb}{"0C} +\DeclareMathSymbol\gneq{\mathrel}{AMSb}{"0D} +\DeclareMathSymbol\npreceq{\mathrel}{AMSb}{"0E} +\DeclareMathSymbol\nsucceq{\mathrel}{AMSb}{"0F} +\DeclareMathSymbol\precnsim{\mathrel}{AMSb}{"10} +\DeclareMathSymbol\succnsim{\mathrel}{AMSb}{"11} +\DeclareMathSymbol\lnsim{\mathrel}{AMSb}{"12} +\DeclareMathSymbol\gnsim{\mathrel}{AMSb}{"13} +\DeclareMathSymbol\nleqq{\mathrel}{AMSb}{"14} +\DeclareMathSymbol\ngeqq{\mathrel}{AMSb}{"15} +\DeclareMathSymbol\precneqq{\mathrel}{AMSb}{"16} +\DeclareMathSymbol\succneqq{\mathrel}{AMSb}{"17} +\DeclareMathSymbol\precnapprox{\mathrel}{AMSb}{"18} +\DeclareMathSymbol\succnapprox{\mathrel}{AMSb}{"19} +\DeclareMathSymbol\lnapprox{\mathrel}{AMSb}{"1A} +\DeclareMathSymbol\gnapprox{\mathrel}{AMSb}{"1B} +\DeclareMathSymbol\nsim{\mathrel}{AMSb}{"1C} +\DeclareMathSymbol\ncong{\mathrel}{AMSb}{"1D} +%\DeclareMathSymbol\varsubsetneq{\mathrel}{AMSb}{"20} +%\DeclareMathSymbol\varsupsetneq{\mathrel}{AMSb}{"21} +\DeclareMathSymbol\nsubseteqq{\mathrel}{AMSb}{"22} +\DeclareMathSymbol\nsupseteqq{\mathrel}{AMSb}{"23} +\DeclareMathSymbol\subsetneqq{\mathrel}{AMSb}{"24} +\DeclareMathSymbol\supsetneqq{\mathrel}{AMSb}{"25} +%\DeclareMathSymbol\varsubsetneqq{\mathrel}{AMSb}{"26} +%\DeclareMathSymbol\varsupsetneqq{\mathrel}{AMSb}{"27} +\DeclareMathSymbol\subsetneq{\mathrel}{AMSb}{"28} +\DeclareMathSymbol\supsetneq{\mathrel}{AMSb}{"29} +\DeclareMathSymbol\nsubseteq{\mathrel}{AMSb}{"2A} +\DeclareMathSymbol\nsupseteq{\mathrel}{AMSb}{"2B} +\DeclareMathSymbol\nparallel{\mathrel}{AMSb}{"2C} +\DeclareMathSymbol\nmid{\mathrel}{AMSb}{"2D} +\DeclareMathSymbol\nshortmid{\mathrel}{AMSb}{"2E} +\DeclareMathSymbol\nshortparallel{\mathrel}{AMSb}{"2F} +\DeclareMathSymbol\nvdash{\mathrel}{AMSb}{"30} +\DeclareMathSymbol\nVdash{\mathrel}{AMSb}{"31} +\DeclareMathSymbol\nvDash{\mathrel}{AMSb}{"32} +\DeclareMathSymbol\nVDash{\mathrel}{AMSb}{"33} +\DeclareMathSymbol\ntrianglerighteq{\mathrel}{AMSb}{"34} +\DeclareMathSymbol\ntrianglelefteq{\mathrel}{AMSb}{"35} +\DeclareMathSymbol\ntriangleleft{\mathrel}{AMSb}{"36} +\DeclareMathSymbol\ntriangleright{\mathrel}{AMSb}{"37} +\DeclareMathSymbol\nleftarrow{\mathrel}{AMSb}{"38} +\DeclareMathSymbol\nrightarrow{\mathrel}{AMSb}{"39} +\DeclareMathSymbol\nLeftarrow{\mathrel}{AMSb}{"3A} +\DeclareMathSymbol\nRightarrow{\mathrel}{AMSb}{"3B} +\DeclareMathSymbol\nLeftrightarrow{\mathrel}{AMSb}{"3C} +\DeclareMathSymbol\nleftrightarrow{\mathrel}{AMSb}{"3D} +\DeclareMathSymbol\divideontimes{\mathbin}{AMSb}{"3E} +\DeclareMathSymbol\varnothing{\mathord}{AMSb}{"3F} +\DeclareMathSymbol\mho{\mathord}{AMSb}{"66} +\DeclareMathSymbol\eth{\mathord}{AMSb}{"67} +\DeclareMathSymbol\eqsim{\mathrel}{AMSb}{"68} +\DeclareMathSymbol\beth{\mathord}{AMSb}{"69} +\DeclareMathSymbol\gimel{\mathord}{AMSb}{"6A} +\DeclareMathSymbol\daleth{\mathord}{AMSb}{"6B} +\DeclareMathSymbol\lessdot{\mathrel}{AMSb}{"6C} +\DeclareMathSymbol\gtrdot{\mathrel}{AMSb}{"6D} +\DeclareMathSymbol\ltimes{\mathbin}{AMSb}{"6E} +\DeclareMathSymbol\rtimes{\mathbin}{AMSb}{"6F} +\DeclareMathSymbol\shortmid{\mathrel}{AMSb}{"70} +\DeclareMathSymbol\shortparallel{\mathrel}{AMSb}{"71} +\DeclareMathSymbol\smallsetminus{\mathbin}{AMSb}{"72} +\DeclareMathSymbol\thicksim{\mathrel}{AMSb}{"73} +\DeclareMathSymbol\thickapprox{\mathrel}{AMSb}{"74} +\DeclareMathSymbol\approxeq{\mathrel}{AMSb}{"75} +\DeclareMathSymbol\succapprox{\mathrel}{AMSb}{"76} +\DeclareMathSymbol\precapprox{\mathrel}{AMSb}{"77} +\DeclareMathSymbol\curvearrowleft{\mathrel}{AMSb}{"78} +\DeclareMathSymbol\curvearrowright{\mathrel}{AMSb}{"79} +\DeclareMathSymbol\digamma{\mathord}{AMSb}{"7A} +\DeclareMathSymbol\varkappa{\mathord}{AMSb}{"7B} +\DeclareMathSymbol\hslash{\mathord}{AMSb}{"7D} +\DeclareMathSymbol\hbar{\mathord}{AMSb}{"7E} +\DeclareMathSymbol\backepsilon{\mathrel}{AMSb}{"7F} +} +\def\interleave{{\parallel\!\!\vert}} +\def\shortinterleave{\z@rel{\mathord\shortmid\mathord\shortparallel}} +\def\napprox{\not\approx} +\let\restriction\upharpoonright +\let\Doteq\doteqdot +\let\doublecup\Cup +\let\llless\lll +\let\gggtr\ggg +\let\doublecap\Cap +% \end{macrocode} +% +% Numbers +% +% \begin{macrocode} +\def \nat {{\mathbb N}} +\def \integer {{\mathbb Z}} +\def \natone {{\mathbb N}_1} +\def \real {{\mathbb R}} +\def \bool {{\mathbb B}} +\let \divides \div +\def \div {\z@bin{\mathrm{div}}} +\def \mod {\z@bin{\mathrm{mod}}} +\def \succ {\word{succ}} +\def \expon {^} +% \end{macrocode} +% aliases +% \begin{macrocode} +\let \num \integer +\let \nplus \natone +% \end{macrocode} +% +% Logic +% +% \begin{macrocode} +\def \lnot {\neg\;} +\def \land {\z@rel{\wedge}} +\def \lor {\z@rel{\vee}} +\let \imp \Rightarrow +\let\iff \Leftrightarrow +\def \all {\z@op{\xforall}} +\def \exi {\z@op{\xexists}} +\def \exione {\exists_1} +\@ifpackageloaded{lucbr}{% +\DeclareMathSymbol{\nexi}{0}{arrows}{"20} +}{% +\DeclareMathSymbol{\nexi}{\mathord}{AMSb}{"40} +} +\def \dot {\z@rel{\bullet}} +\def \true {\keyword{true}} +\def \false {\keyword{false}} +\let \cond \rightarrow +% \end{macrocode} +% aliases +% \begin{macrocode} +\let \spot \dot +\mathcode`\@="8000% make @ active in mathmode +{\catcode`\@=\active \gdef@{\dot}} +\let \implies \imp +\let \forall \all +\let \exists \exi +\let \nexists \nexi +% \end{macrocode} +% +% SETS +% +% \begin{macrocode} +\let \emptyset \varnothing +\def \varemptyset {\{\,\}} +\def \pset {\z@op{\mathbb P}} +\def \psetone {\pset_1} +\def \fset {\z@op{\mathbb F}} +\def \fsetone {\fset_1} +\def \sset {\z@op{\mathbb S}} +\let \mem \in +\def \nem {\not\mem} +\def \uni {\z@bin\cup} +\def \int {\z@bin\cap} +\let \prod \times +\def \min {\word{min}} +\def \max {\word{max}} +\def \duni {\z@Bigop{\lower0.25ex\hbox{$\uni$}}} +\def \dint {\z@Bigop{\lower0.25ex\hbox{$\int$}}} +\def \upto {\z@bin{\ldotp\ldotp}} +\let \psubs \subset +\let \subs \subseteq +\let \psups \supset +\let \sups \supseteq +\def \diff {\z@bin{\backslash}} +% \end{macrocode} +% aliases +% \begin{macrocode} +\let \cross \prod +\let \notin \nem +\let \nmem \nem +\let \union \uni +\let \inter \int +\let \power \pset +\let \finset \fset +\let \dunion \duni +\let \dinter \dint +% \end{macrocode} +% +% RELATIONS \& FUNCTIONS +% +% \begin{macrocode} +\def \lambda {\z@op{\xlambda}} +\def \mu {\z@op{\xmu}} +\def \dom {\keyword{dom}} +\def \ran {\keyword{ran}} +\def \id {\keyword{id}} +\@ifpackageloaded{lucbr}{% +\DeclareMathSymbol{\dres}{\mathbin}{letters}{"2F} +\DeclareMathSymbol{\rres}{\mathbin}{letters}{"2E} +}{% +\DeclareMathSymbol{\dres}{\mathbin}{AMSa}{"43} +\DeclareMathSymbol{\rres}{\mathbin}{AMSa}{"42} +} +\def \dsub {\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\dres}}} +\def \rsub {\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\rres}}} +\let \fovr \oplus +\let \cmp \circ +\def \fcmp {\mathbin{\raise 0.6ex\hbox{\oalign{\hfil$\scriptscriptstyle + \mathrm{o}$\hfil\cr\hfil$\scriptscriptstyle\mathrm{9}$\hfil}}}} +\def \inv {^\sim} +\def \limg {(\!|} +\def \rimg {|\!)} +\let \map \mapsto +\let \rel \leftrightarrow +\let \tfun \rightarrow +\let \tinj \rightarrowtail +\def \tsur {\mathrel{\ooalign{$\tfun$\hfil\cr$\mkern4mu\tfun$}}} +\def \pfun {\p\tfun} +\def \pinj {\p\tinj} +\def \psur {\p\tsur} +\def \ffun {\f\tfun} +\def \finj {\f\tinj} +\def \bij {\mathrel{\ooalign{$\tinj$\hfil\cr$\mkern5mu\tfun$}}} +\def \tcl {^+} +\def \rtcl {^*} +\def \iter {^} +% \end{macrocode} +% aliases +% \begin{macrocode} +\let \comp \fcmp +\let \ndres \dsub +\let \nrres \rsub +\let \fun \tfun +\let \inj \tinj +\let \surj \tsur +\let \psurj \psur +\let \llless \lll +\let \gggtr \ggg +\def \interleave {{\parallel\!\!\vert}} +\def \shortinterleave {\z@rel{\mathord\shortmid\mathord\shortparallel}} +\let \restriction \upharpoonright +\def \napprox {\not\approx} +% \end{macrocode} +% +% SEQUENCES +% \begin{macrocode} +\def \seq {\keyword{seq}} +\def \iseq {\keyword{iseq}} +\def \seqone {\seq_1} +\def \emptyseq {\lseq\,\rseq} +\let \lseq \langle +\let \rseq \rangle +\def \head {\word{head}} +\def \tail {\word{tail}} +\def \front {\word{front}} +\def \last {\word{last}} +\def \rev {\word{rev}} +\def \squash {\word{squash}} +\def \next {\keyword{next}} +\def \inseq {\keyword{in}} +\@ifpackageloaded{lucbr}{% +\DeclareMathSymbol{\sres}{2}{arrows}{"75} +\DeclareMathSymbol{\ires}{2}{arrows}{"76} +\DeclareMathSymbol{\@@cat}{\mathbin}{operators}{"5F} +}{% +\DeclareMathSymbol{\@@cat}{\mathbin}{AMSa}{"61} +\DeclareMathSymbol{\sres}{\mathbin}{AMSa}{"16} +\DeclareMathSymbol{\ires}{\mathbin}{AMSa}{"18} +} +\def \cat {\mathbin{\raise 0.8ex\hbox{$\mathchar\@@cat$}}} +\def \ssub {\z@bin{\rlap{$-$}{\sres}}} +\def \isub {\z@bin{\rlap{$-$}{\ires}}} +\def \dcat {\z@op{\cat/}} +\def \dovr {\z@op{\fovr/}} +\def \dcmp {\z@op{\fcmp/}} +\let \prefix \subseteq +\def \suffix {\keyword{suffix}} +\def \seqi {\keyword{seq_\infty}} +\def \partitions {\keyword{partitions}} +\def \partition {\keyword{partitions}} +\def \disjoint {\keyword{disjoint}} +\def \subseq {\keyword{subseq}} +% \end{macrocode} +% aliases +% \begin{macrocode} +\let \filter \sres +% \end{macrocode} +% +% Schemas: +% +% \begin{macrocode} +\def \lsch {\z@bigop{[}} +\def \rsch {\z@bigop{]}} +\def \dparallel {\z@bigop{\parallel}\limits} +\def \zand {\z@bigbin\land} +\def \zor {\z@bigbin\lor} +\def \zcmp {\z@bigbin\fcmp} +\def \zexi {\z@bigop\exists} +\def \zall {\z@bigop\forall} +\def \znot {\z@bigop\neg} +\def \zbar {\z@bigbin\cbar} +\def \zfor {/} +\def \zhide {\z@bigbin\backslash} +\def \zimp {\z@bigrel\imp} +\def \zeq {\z@bigrel\iff} +\def \zovr {\z@bigrel\oplus} +\def \zpipe {\z@bigbin{\mathord>\!\!\mathord>}} +\def \pre {\keyword{pre}} +\def \pred {\keyword{pred}} +\def \post {\keyword{post}} +\def \zproject {\z@bigbin\sres} +\def\rename{\@ifnextchar*{\z@rename}{\z@@rename}} +\def\z@rename*[#1/#2]{\left[#1 \over #2\right]} +\def\z@@rename[#1/#2]{\left[#1 \zfor #2\right]} +% \end{macrocode} +% aliases +% \begin{macrocode} +\let \project \zproject +\let \import \sres +\let \semi \zcmp +\let \hide \zhide +% \end{macrocode} +% +% BAGS +% +% \begin{macrocode} +\let\buni\uplus +\def \emptybag {\lbag\:\rbag} +\def \lbag {[\![} +\def \rbag {]\!]} +\def \bag {\keyword{bag}} +\def \items {\word{items}} +\let \inbag \inseq +\def \bagcount {\word{count}} +% \end{macrocode} +% +% Definitions \& declarations +% +% \begin{macrocode} +\def \ddef {\z@rel{\;::=\;}} +\def \bbar {\z@bigrel{|}} +\let \cbar \mid +\def \lang {\langle\!\langle} +\def \rang {\rangle\!\rangle} +\def \sdef {\z@rel{\widehat=}} +\def \defs {\z@smallrel{==}} +\def \varsdef {\z@rel\triangleq} +% \end{macrocode} +% aliases +% \begin{macrocode} +\let \sdefs \sdef +\mathcode`\|=\mid +\let \ldata \lang +\let \rdata \rang +% \end{macrocode} +% +% MISCELLANEOUS +% +% \begin{macrocode} +\def \lblot {\langle\!|} +\def \rblot {|\!\rangle} +\def \IMP {\boldword{Import}} +\let \env \Rrightarrow +\def \zlet {\boldword{let}} +\def \zin {\boldword{in}} +\def \zwhere {\boldword{where}} +% \end{macrocode} +% +% QZED SUPPORT +% +% \begin{macrocode} +\def\HOLE{\z@op{\hbox{$\lll\star\star\star\ggg$}}} +\def\landd{} % to support qzed editor +\def\semid{} % to support qzed editor +\def\qzed{\ifz@inclass\else\zed\fi} +\def\endqzed{\ifz@inclass\else\endzed\fi} +% \end{macrocode} +% +% CLASSES +% +% \begin{macrocode} +\def\qua{\mbox{::}} +\def\redef{\mbox{\textbf{~redef}}} +\def\Init{I\!{\scriptstyle{NIT}}} +\def\Exit{E\!{\scriptstyle{XIT}}} +\def\Internal{I\!{\scriptstyle{NTERNAL}}} +\def\Aux{A\!{\scriptstyle{UX}}} +\def\intern{\mbox{\textsf{i}}} +% \end{macrocode} +% +% PROOFS +% +% \begin{macrocode} +\def\thrm{\z@rel\vdash} +\def\qed{\zsmall\Box} +\let\Qed\Box +\let\QED\square +\def\BLACKQED{\zsmall\blacksquare} +\let\ETH\qed +\def\TH{\boldword{Theorem}} +\def\LE{\boldword{Lemma}} +\def\PR{\boldword{Proof}} +\def\refines{\z@rel\sqsupseteq} +\def\defines{\z@rel\sqsubseteq} +\def\weakrefine{\z@rel{\raise0.2ex\rlap{\hbox{$\sqsupset$}}\lower1ex\hbox{$\sim$}}} +\def\weakdefine{\z@rel{\raise0.2ex\rlap{\hbox{$\sqsubset$}}\lower1ex\hbox{$\sim$}}} +% \end{macrocode} +% aliases +% \begin{macrocode} +\let\shows\thrm +% \end{macrocode} +% +% OBJECT THEORY +% +% \begin{macrocode} +\def\childof{\z@rel\xsucc} +\def\parentof{\z@rel\xprec} +\let\weaksubclass\succsim +\let\weaksupclass\precsim +\def\hasa{\z@rel{\mathord\xsucc\!\!\!\mathord\xsucc}} +\def\instancein{\z@rel{\mathord\xprec\!\!\!\mathord\xprec}} +\def\subtype{\z@rel\sqsubset} +\def\subtypeeq{\z@rel\sqsubseteq} +\def\suptype{\z@rel\sqsupset} +\def\suptypeeq{\z@rel\sqsupseteq} +% \end{macrocode} +% aliases +% \begin{macrocode} +\let\inherits\childof +\let\subclass\childof +\let\isa\childof +\let\supclass\parentof +\let\instantiates\hasa +\let\islikea\weaksubclass +\def\poly{\mathord\downarrow} +\def\widen#1{\z@op{{\overline{#1}}}} +% \end{macrocode} +% +% TEMPORAL LOGIC +% +% \begin{macrocode} +\def\atnext{\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\zSmall\bigcirc$}\kern0.01em\zSmall\bigcirc} +\def\atlast{\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\kern0.01em\mathord-$}\zSmall\bigcirc} +\def\always{\lower0.37ex\hbox{$\zbig\Box$}} +\def\uptilnow{\rlap{$\kern0.02em\mathord-$}\lower0.37ex\hbox{$\zbig\Box$}} +\def\eventually{\lower0.37ex\hbox{$\zbig\Diamond$}} +\def\previously{\rlap{$\kern0.04em\mathord-$}\lower0.37ex\hbox{$\zbig\Diamond$}} +% \end{macrocode} +% aliases +% \begin{macrocode} +\let\henceforth\always +% \end{macrocode} +% +% ORDERS +% +% \begin{macrocode} +\def \mono {\keyword{monotonic}} +\def \porder {\keyword{partial\_order}} +\def \torder {\keyword{total\_order}} +\newbox\z@combox\newdimen\z@wdcalc +\def\comment{\@ifnextchar*{\z@leftcomment}{\z@comment}} +\def\z@comment#1{$\z@stopfield\z@addfield\z@startfield$% +\global\setbox\z@combox\hbox{\quad[{\sf #1}]}\z@wdcalc=\wd\z@combox% +\advance\z@wdcalc by \wd\z@curline\advance\z@wdcalc by \z@curindent% +\advance\z@wdcalc by \zedleftsep\advance\z@wdcalc by \zedlinethickness% +\advance\z@wdcalc by 2\zedindent\ifdim\z@wdcalc>\displaywidth\\% +\fi&\box\z@combox\ignorespaces} +\def\z@leftcomment*#1{\hbox{[{\sf #1}]}} +% \end{macrocode} +% +%\section{Object-Z Notations} +% +% KEYWORDS AND KEYSYMBOLS +% +% \begin{macrocode} +\def \oid {{\bbold O}} +\def \self {\word{self}} +\def \contained {\word{contained}} +\let \classuni \uni +\def \visibility {\zproject} +\def \invisibility {{\project\hspace{-0.63 em}\cross}} +% \end{macrocode} +% +% CONTAINMENT AND CONTROL ADORNMENTS +% +% \begin{macrocode} +\def \cid {{\bigcirc\mbox{\scriptsize{\hspace{-0.78em}}\mbox{\tiny{C}}}}} +\def \sid {{\bigcirc\mbox{\scriptsize{\hspace{-0.74em}}\mbox{\tiny{S}}}}} +\def \eid {{\bigcirc\mbox{\scriptsize{\hspace{-0.74em}}\mbox{\tiny{E}}}}} +% \end{macrocode} +% +% BINARY COMPOSITION OPERATORS +% +% \begin{macrocode} +\def \pll {~\parallel~} +\def \plo {~\parallel_{!}~} +\def \sqc {~\semi~} +\def \cnj {~\zand~} +\def \gch {~[\mbox{\hspace{-0.06em}}]~} +\def \enh {~\dot~} +% \end{macrocode} +% +% DISTRIBUTED COMPOSITION OPERATORS +% +% \begin{macrocode} +% Redefined because of \zbig problem +% \def \dsqc {\mbox{{\Large $\zcmp~$}}} +\def \dsqc {\mbox{{\Large $\fcmp~$}}} +\def \dgch {\mbox{{\Large $[\mbox{\hspace{-0.06em}}]$}}} +% Redefined because of \zbig problem +% \def \dcnj {\mbox{{\Large $\zand$}}} +\def \dcnj {\mbox{{\Large $\land$}}} +\def \dpll {\mbox{{\Large $\parallel$}}} +\def \dplo {\mbox{{\Large $\parallel_{!}$}}} +% \end{macrocode} +% +%\section{Z environments} +% +%\subsection{Margin stack} +% +% Define a stack of dimensions (50 elements) +% This can probably be made smaller when qzed filters its \TeX\ output better +% \begin{macrocode} +\newcount\z@stackmin +\newcount\z@stackmax +\newcount\z@stacktop +\newdimen\@gtempa \z@stackmin=\allocationnumber +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa +\newdimen\@gtempa +\z@stackmax=\allocationnumber +\dimen\z@stackmin=0pt +% \end{macrocode} +% Define a box to contain the current line +% \& a variable to contain it's indentation +% \begin{macrocode} +\newbox\z@curline +\newdimen\z@curindent +\dimen\z@curindent=0pt +% \end{macrocode} +% Space between operands of a function application +% \begin{macrocode} +\def\z@space{{}\;{}} +% \end{macrocode} +% Define a box to contain the current field +% \begin{macrocode} +\newbox\z@curfield +% \end{macrocode} +% Define a mini-tabbing environment for use inside `zed' +% \begin{macrocode} +\def\z@startline{\setbox\z@curline\hbox{}% + \global\z@curindent\dimen\z@stacktop + \z@startfield\ignorespaces} +\def\z@stopline{\z@stopfield + \z@addfield + \hbox{\hskip\z@curindent \box\z@curline}} + +\def\z@startfield{\global\setbox\z@curfield\hbox\bgroup} +\def\z@stopfield{\egroup} +\def\z@addfield{\global\setbox\z@curline\hbox{\unhbox + \z@curline\unhbox\z@curfield}} + +\def\z@pushmargin{\hbox{\kern0pt}$% + \z@stopfield + \z@addfield + \ifnum \z@stacktop < \z@stackmax + \global\advance\z@stacktop \@ne + \else + \@latexerr{Z margin stack overflow (too many \string\M's)} + \@ehd + \fi + \global\dimen\z@stacktop\z@curindent + \global\advance\dimen\z@stacktop \wd\z@curline + \z@startfield\ignorespaces + $\relax} +\def\z@popmargin{\ifnum \z@stacktop > \z@stackmin + \global\advance\z@stacktop \m@ne \ignorespaces + \else + \@latexerr{Z Margin stack underflow (too many \string\O's)} + \@ehd + \fi} +\def\M{\z@pushmargin} \def\O{\z@popmargin} \def\S{\z@space} +\z@stacktop\z@stackmin +% \end{macrocode} +% +%\subsection{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. +% +%\subsubsection{Format and control macros} +% +% \begin{macrocode} +\newdimen\zedindent \zedindent=\leftmargini +\newdimen\zedleftsep \zedleftsep=1em +\newdimen\zedtab \zedtab=2em +\newdimen\zedbar \zedbar=8em +\newdimen\zedlinethickness \zedlinethickness=0.4pt +\newdimen\zedcornerheight \zedcornerheight=0pt +\newcount\z@cols +\newif\ifz@firstline \z@firstlinefalse +\newif\ifz@inclass \z@inclassfalse +\newif\ifz@inenv \z@inenvfalse +\newif\ifz@leftmargin \z@leftmargintrue +\newif\ifz@incols \z@incolsfalse +\newif\ifleftnames \leftnamesfalse +\def\leftschemas{\leftnamestrue} +\newif\ifz@inbox \z@inboxfalse +\newskip\zedbaselineskip \zedbaselineskip\baselineskip +\newbox\zstrutbox \setbox\zstrutbox=\copy\strutbox +\def\zstrut{\relax\ifmmode\copy\zstrutbox\else\unhcopy\zstrutbox\fi} +\def\zedbaselinestretch{1} +\def\baselinestretch{1} +% \end{macrocode} +% +% Penalties +% +% \begin{macrocode} +\newcount\interzedlinepenalty \interzedlinepenalty=10000 %never break +\newcount\preboxpenalty \preboxpenalty=0 %break easily +\newcount\forcepagepenalty \forcepagepenalty=-10000 %always break +\interdisplaylinepenalty=100 %break sometimes +% \end{macrocode} +% +% Macros for changing the size of schema text +% +% \begin{macrocode} +\def\zedsize#1{\def\z@size{#1}} +\def\z@size{} +\newskip\z@adskip\newskip\z@bdskip\newskip\z@adsskip\newskip\z@bdsskip +\def\z@changesize{% +\z@adskip\abovedisplayskip\z@bdskip\belowdisplayskip% save skips +\z@adsskip\abovedisplayshortskip\z@bdsskip\belowdisplayshortskip +\z@size % change size +\abovedisplayskip\z@adskip\belowdisplayskip\z@bdskip% restore skips +\abovedisplayshortskip\z@adsskip\belowdisplayshortskip\z@bdsskip} +% +\def\z@zeroskips{\abovedisplayskip\z@\belowdisplayskip\z@ + \abovedisplayshortskip\z@\belowdisplayshortskip\z@} +% +% Make zedbaselinestretch have an automatic effect +% adapted from lfonts.tex +% +\def\@setfontsize#1#2#3{\@nomath#1% + \ifx\protect\@typeset@protect + \let\@currsize#1% + \fi + \fontsize{#2}{#3}\selectfont + \setlength{\zedbaselineskip}{\baselineskip/\real{\baselinestretch}}% + \zedbaselineskip\zedbaselinestretch\zedbaselineskip + \setbox\zstrutbox\hbox{\vrule height.7\zedbaselineskip + depth.3\zedbaselineskip width\z@}} +% \end{macrocode} +% +%\subsection{Macros for margins} +% +% |\z@narrow|, |\z@wide| --- make the margins narrower, wider +% +% \begin{macrocode} +\def\z@narrow{\advance\linewidth by -\zedindent} +\def\z@wide{\advance\linewidth by \zedindent} +% \end{macrocode} +% +%\subsection{Macros for drawing boxes} +% +% |\z@hrulefill| --- line with correct thickness +% +% \begin{macrocode} +\def\z@hrulefill{\leaders\hrule height\zedlinethickness\hfill} +% \end{macrocode} +% +% |\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 +% +% \begin{macrocode} +\def\z@topline#1{\omit\@ifnextchar[{\z@@topline{#1}}{\z@@topline{#1}[]}} +\def\z@@topline#1[#2]{\hbox to\linewidth{\zstrut\ifleftnames\else + \vrule height\zedlinethickness width\zedlinethickness + \hbox to\zedleftsep{\z@hrulefill}\fi#1\z@hrulefill + \smash{\vrule height\zedlinethickness width\zedlinethickness + depth\zedcornerheight}\hbox{\sf #2}}\cr} +\def\z@dbltopline#1{\omit\@ifnextchar[{\z@@dbltopline{#1}}{\z@@dbltopline{#1}[]}} +\def\z@@dbltopline#1[#2]{\z@@topline{#1}[#2]% +\noalign{\kern-\baselineskip + \kern-\zedlinethickness + \kern-\doublerulesep \nobreak}% +\omit\z@@topline{\hphantom{#1}}[\hphantom{#2}]% +\noalign{\kern\doublerulesep + \kern\zedlinethickness \nobreak}} +\def\z@botline{\also\omit\hbox to\linewidth{\z@hrulefill +\smash{\vrule height\zedcornerheight width\zedlinethickness + depth 0pt}}\cr} +\def\z@@botline[#1]{\hbox to\linewidth{\vrule\z@hrulefill\hbox{\sf\smash{#1}}}\also} +\def\zedline{\also\omit\@ifnextchar[{\z@@botline}{\z@@botline[]}} +\def\where{\also \omit \hbox to\zedbar{\z@hrulefill}\cr\also} +\let \ST \where +% \end{macrocode} +% +% |\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. +% +% \begin{macrocode} +\def\z@left{\ifz@inbox\vrule width\zedlinethickness\hskip\zedleftsep\fi} +% \end{macrocode} +% +% \subsection{Macros for setting up Z environments} +% +% \begin{macrocode} +\def\z@env{\global\z@firstlinetrue\z@changesize + $$ + \z@inenvtrue + \baselineskip\zedbaselineskip + \parskip=0pt\lineskip=0pt\z@narrow + \advance\displayindent by \zedindent + \def\\{\crcr}% Must have \def and not \let for nested alignments. + \everycr={\noalign{\ifz@firstline \global\z@firstlinefalse + \else \penalty\interzedlinepenalty \fi}} + \tabskip=0pt} +\def\endz@env{$$ + \global\@ignoretrue +} +% \end{macrocode} +% +% 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. +% +% \begin{macrocode} +\def\z@format{\halign to\linewidth\bgroup% + \zstrut\z@left\z@startline\ignorespaces$\@lign##$\z@stopline\hfil% + \tabskip=0pt plus1fil% + &\hbox to 0pt{\hss\@lign##}\tabskip=0pt\cr} +\def\z@boxenv{\z@narrow\let\also=\als@ \let\Also=\Als@ \let\ALSO=\ALS@ + \z@inboxtrue \predisplaypenalty=\preboxpenalty \z@env\z@format} +\def\z@outnonbox{\z@outclasscheck\z@leavevmode\z@env} +\def\z@inoutbox{\z@leavevmode\z@makeouter\z@inclassfalse\z@boxenv} +% \end{macrocode} +% +%\subsection{Spacing commands} +% +% no vertical glue between abutted lines +% +% \begin{macrocode} +\def\@but{\noalign{\nointerlineskip}} +% \end{macrocode} +% +% 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{}}}| +% \begin{macrocode} +\def\z@nopar{\global\@endpetrue} +% \end{macrocode} +% +% |\z@leavevmode| -- Enter horizontal mode, taking account of possible +% interaction with lists and section heads: +%\begin{enumerate} +% \item After a |\item|, use |\indent| to get the label (this +% fails to run in even short labels). +% \item After a run-in heading, use |\indent|. +% \item After an ordinary heading, throw away the |\everypar| +% tokens, reset |\@nobreak|, and use |\noindent| with |\parskip| +% zero. +% \item Otherwise, use |\noindent| with |\parskip| zero +%\end{enumerate} +% Use when entering displayed environments to get correct spacing +% +% \begin{macrocode} +\def\z@leavevmode{\ifvmode\if@inlabel\indent\else\if@noskipsec\indent\else + \if@nobreak\global\@nobreakfalse\everypar={}\fi + {\parskip=0pt\noindent}\fi\fi\fi} +% \end{macrocode} +% +% extra vertical space in non-box environments +% +% \begin{macrocode} +\def\also{\crcr\noalign{\vskip\jot}} +\def\Also{\crcr\noalign{\vskip2\jot}} +\def\ALSO{\Also\Also} +% \end{macrocode} +% +% extra vertical space in boxed environments +% +% \begin{macrocode} +\def\als@{\crcr\@but\omit\vrule height\jot width\zedlinethickness \cr \@but} +\def\Als@{\crcr\@but\omit\vrule height2\jot width\zedlinethickness \cr \@but} +\def\ALS@{\crcr\@but\omit\vrule height4\jot width\zedlinethickness \cr \@but} +% \end{macrocode} +% +%\subsection{Environment-breaking commands} +% +% \begin{macrocode} +\def\znewpage{\also\noalign{\penalty\forcepagepenalty}\also} +\def\zbreak{\also\noalign{\penalty\interdisplaylinepenalty\vskip-\jot}\also} +\def\Zbreak{\also\noalign{\penalty\interdisplaylinepenalty}\also} +\def\ZBREAK{\Also\noalign{\penalty\interdisplaylinepenalty}\Also} +\def\t#1{\hskip #1\zedtab} +%\def\c#1#2{\hbox to #1\zedtab{$#2$\hfil}} +\def\flushr#1{\crcr\quad\cr} +% \end{macrocode} +% +%\section{Utility macros for Object-Z} +% +% \begin{macrocode} +\def\z@inclasscheck{\ifz@inclass\else + \@latexerr{This Z environment is only allowed within a class} +{Perhaps you forgot to include a \string\begin\string{class\string} +somewhere^^Jor you are trying to print a file that needs updating.^^J\@ehc} \fi} +\def\z@outclasscheck{\ifz@inclass + \@latexerr{This Z environment is not allowed inside a class} +{This environment doesn't really make sense within a class.^^J% +If you really want it then I'll try my best to fit in in.^^J\@ehc}\else +\ifz@inenv \@latexerr{New Z environment declared before previous +one is completed} +{I suspect that you've forgotten to finish the last environment.^^J% +You are trying to nest environments and this can only be done inside classes^^J% +besides, the environment you have started isn't valid within classes any way.^^JI suggest that you type \space X \space to quit and then correct your document.} +\fi\fi} +% +\def\z@makeouter{% + \ifz@inenv + \ifz@inclass\z@inenvfalse + \hskip-\zedleftsep \advance\linewidth by -\zedlinethickness + \zedindent=\zedleftsep \zedleftsep=0.8\zedleftsep + \zedbar=0.8\zedbar \zedtab=0.8\zedtab + \oz@parbox{\linewidth}\bgroup + \z@zeroskips + \else + \@latexerr{Incorrect place for Z environment; nesting is + allowed only inside classes} + {You've either forgotten to finish the last environment,^^J% + you've forgotten to include a + \string\begin\string{class\string} somewhere^^J% + or you are trying to print a file that needs updating.^^J% + (Then again, you might just be trying to do something^^J% + that the author of these macros didn't intend you to do)^^J\@ehc} + \fi + \else + \bgroup + \fi +} +% +\def \z@makeinner{\egroup + \global\z@curindent\z@ +} +% +\def \classbreak{\also\egroup$$\vskip -\ht\zstrutbox + \vskip -\abovedisplayskip\vskip -\belowdisplayskip\z@wide\z@boxenv\also} +% \end{macrocode} +% +%\section{Non-box environments} +% +% +% ZED for non-box multiline formulas +% +% \begin{macrocode} +\def\zed{\z@outnonbox\z@inboxfalse\z@format} +\def\endzed{\crcr\egroup\endz@env} +\let\[=\zed +\def\]{\crcr\egroup$$\ignorespaces} +% \end{macrocode} +% +% 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. +% +% \begin{macrocode} +\def\argue{\z@outnonbox\interzedlinepenalty=\interdisplaylinepenalty + \openup 1\jot \z@format + \noalign{\vskip-\jot}}% equal vspace above and below argue display +\let\endargue=\endzed +% \end{macrocode} +% +% 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. +% +% \begin{macrocode} +\def\infrule{\z@outnonbox\halign\bgroup + \zstrut\quad$\@lign##$\quad\hfil&\quad\@lign##\hfil\cr} +\let\endinfrule=\endzed +\def\derive{\crcr\also\@but\omit\z@hrulefill% + \@ifnextchar[{\z@sidecondition}{\cr\also\@but}} +\def\Derive{\crcr\also\@but\omit\z@hrulefill\cr\@but + \noalign{\kern-\dp\zstrutbox + \kern\doublerulesep \nobreak}% +\omit\derive} +\def\z@sidecondition[#1]{&$\smash{\lower 0.2ex\hbox{$[\;#1\;]$}}$\cr\also\@but} +% \end{macrocode} +% +% SYNTAX for syntax rules +% +% `syntax' environment: used for syntax rules --- even (once!) for VDM. +% \begin{macrocode} +\def\syntax{\z@outnonbox\halign\bgroup + \zstrut$\@lign##$\hfil &\hfil$\@lign{}##{}$\hfil + &$\@lign##$\hfil &\qquad\@lign-- ##\hfil\cr} +\let\endsyntax=\endzed +% \end{macrocode} +% +% \subsection{Boxed environments} +% +% +% SCHEMA schema definitions +% +% \begin{macrocode} +\def\schema#1{\z@inoutbox\z@topline{$\,#1\,$}} +\def\endschema{\z@botline \endzed \z@makeinner \z@nopar} +% \end{macrocode} +% +% ANONSCHEMA schema with no name +% +% \begin{macrocode} +\@namedef{anonschema}{\leftnamesfalse\z@inoutbox\z@topline{}} +\expandafter\let\csname endanonschema\endcsname=\endschema +% \end{macrocode} +% +% GENSCHEMA generic schema definitions +% +% \begin{macrocode} +\def\genschema#1#2{\z@inoutbox\z@topline{$\,#1\:[#2]\,$}} +\let\endgenschema=\endschema +% \end{macrocode} +% +% AXDEF `liberal' axiomatic definitions +% +% \begin{macrocode} +\def\axdef{\z@inoutbox} +\def\endaxdef{\endzed\z@makeinner} +% \end{macrocode} +% +% UNIQDEF `unique' axiomatic definitions +% +% \begin{macrocode} +\def\uniqdef{\leftnamesfalse\z@inoutbox\z@dbltopline{}} +\let\enduniqdef=\endschema +% \end{macrocode} +% +% GENDEF 'generic' axiomatic definitions +% +% HACK TO MAKE IT COMPATIBLE WITH FUZZ.STY +% \begin{macrocode} +\def\gendef{\@ifnextchar[{\z@gendef}{\z@@gendef}} +\def\z@gendef[#1]{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,[#1]\,$}} +\def\z@@gendef#1{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,[#1]\,$}} +\let\endgendef=\endschema +% \end{macrocode} +% +% GENGENDEF generic contents 'generic' axiomatic definitions +% +% Hack to provide syntax-oriented display boxes +% \begin{macrocode} +\def\gengendef{\@ifnextchar[{\z@gengendef}{\z@@gengendef}} +\def\z@gengendef[#1]{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,#1\,$}} +\def\z@@gengendef#1{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,#1\,$}} +\let\endgengendef=\endschema +% \end{macrocode} +% +% CLASS +% +% \begin{macrocode} +\def\class#1{\z@leavevmode\z@makeouter\z@inclasstrue + \z@boxenv\z@topline{$\,#1\,$}} +\let\endclass\endschema +% \end{macrocode} +% +% OP +% +% \begin{macrocode} +\def\op{\z@inclasscheck\schema} +\let\endop\endschema +% \end{macrocode} +% +% STATE +% +% \begin{macrocode} +\def\state{\z@inclasscheck\anonschema} +\let\endstate\endschema +% \end{macrocode} +% +% INIT +% +% \begin{macrocode} +\def\init{\z@inclasscheck\schema{\Init}} +\let\endinit\endschema +% \end{macrocode} +% +% CONST +% +% \begin{macrocode} +\let\const\axdef +\let\endconst\endaxdef +% \end{macrocode} +% +% TYPE +% +% \begin{macrocode} +\def\type{\z@inclasscheck} +\let\endtype\relax +% \end{macrocode} +% +%\subsection{Other environments} +% +% SIDEBYSIDE +% +% This should support an arbitary number of columns +% |\zedindent|'s proportion of |\linewidth| gives a practical limit +% +% \begin{macrocode} +\def\sidebyside{\@ifnextchar[{\z@columns}{\z@columns[2]}} +\def\z@columns[#1]{\z@leavevmode\z@cols#1 \z@makeouter\z@narrow% + $$\lineskip=0pt\z@incolstrue + \predisplaysize\maxdimen + \ifz@leftmargin\hskip-\zedindent\z@leftmarginfalse\fi + \setbox0=\hbox to \linewidth\bgroup\z@zeroskips% + \divide\zedbar by \z@cols \divide\zedleftsep by \z@cols + \divide\zedtab by \z@cols \divide\linewidth by \z@cols + \oz@parbox[t]{\linewidth}\bgroup\z@wide} +% +\def\nextside{\egroup\hss\oz@parbox[t]{\linewidth}\bgroup\z@wide} +% +\newdimen\z@temp +\def\endsidebyside{\egroup\egroup + \z@temp\ht0 \advance\z@temp by \dp0\advance\z@temp by-\dp\zstrutbox + \hbox{\raise\z@temp\box0}\endz@env\z@makeinner\z@nopar} +% \end{macrocode} +% +% ZPAR +% +% \begin{macrocode} +\def\zpar{\z@leavevmode + \ifz@inenv\z@inclasstrue\fi% fudge to let zpar in all boxes + \z@makeouter\z@changesize + \advance\linewidth by -\z@curindent + \advance\linewidth by -\wd\z@curline + \hskip-\wd\z@curline\advance\linewidth by -\zedindent$$ + \ifz@leftmargin\hskip-\zedindent\fi% adjustment for first column + \advance\displayindent by \zedindent + \advance\displaywidth by -\zedindent + \advance\displayindent by \z@curindent + \advance\displayindent by \wd\z@curline + \advance\displaywidth by -\z@curindent + \advance\displaywidth by -\wd\z@curline + \global\setbox\z@curline\hbox{} + \z@narrow\oz@parbox[b]{\linewidth}\bgroup\hfil\break} +\def\endzpar{\egroup$$\z@makeinner\z@nopar} +% \end{macrocode} +% +% CLASSCOM +% +% \begin{macrocode} +\def \classcom{\zpar\sf} +\let \endclasscom=\endzpar +% \end{macrocode} +% +% PROOF +% +% \begin{macrocode} +\def\proof{\zpar$\PR$\zpar} +\def\endproof{\endzpar\endzpar} +% \end{macrocode} +% +% Additional auxiliary macros +% +% \begin{macrocode} +\def\zseq#1{\lseq #1 \rseq} +\def\zset#1{\{ #1 \}} +\def\zimg#1{\limg #1 \rimg} +\def\zsch#1{\lsch #1 \rsch} +\def\zimgset#1{\zimg\zset{#1}} +% \end{macrocode} +% +% OZ FUZZ +% +% |\defs| == +% |\sdef| |\defs| +% +% \begin{macrocode} +\def\fuzzcompatible{% +\let\defs\sdef +\let\empty\emptyset +} +% +% +% \end{macrocode} +% \Finale +\endinput diff --git a/macros/latex/contrib/objectz/oz.ins b/macros/latex/contrib/objectz/oz.ins new file mode 100644 index 0000000000..5e8ce21167 --- /dev/null +++ b/macros/latex/contrib/objectz/oz.ins @@ -0,0 +1,53 @@ +% \iffalse +% LaTex2e Oz style for typesetting Object Z +% \fi +\def\fileversion{1} +\def\filedate{1993/12/23} +% +% \StopEventually{} +% +% As always we begin by identifying the latest version of this file +% on the VDU and in the {\sf log} file. +% \begin{macrocode} +\def\batchfile{oz.ins} +\input docstrip.tex +\preamble + +Copyright (C) 1993 by Sebastian Rahtz +All rights reserved. + +This file is part of the PSNFSS2e package. +\endpreamble + +\def\batchfile{oz.dst} % ignored in distribution +\input docstrip.tex % ignored in distribution + +\keepsilent + +\preamble +Copyright (C) 1993 Sebastian Rahtz. All rights reserved. +This is a generated file for Object Z. Permission is granted to to +customize the declarations in this file to serve the needs of your +installation. However, no permission is granted to distribute a +modified version of this file under its original name. + +\endpreamble + +\Msg{*** Generating style file for Oz ***} + +\generateFile{oz.sty}{f}{ + \from{oz.dtx}{package}} + + +\Msg{***********************************************************} +\Msg{*} +\Msg{* To finish the installation you have to move the} +\Msg{* file oz.sty into a directory searched by TeX} +\Msg{*} +\Msg{***********************************************************} + + +\endinput + + + diff --git a/macros/latex/contrib/objectz/ozguide.pdf b/macros/latex/contrib/objectz/ozguide.pdf new file mode 100644 index 0000000000..0a54b26d83 Binary files /dev/null and b/macros/latex/contrib/objectz/ozguide.pdf differ diff --git a/macros/latex/contrib/objectz/ozguide.tex b/macros/latex/contrib/objectz/ozguide.tex new file mode 100644 index 0000000000..9932d6dc0e --- /dev/null +++ b/macros/latex/contrib/objectz/ozguide.tex @@ -0,0 +1,1311 @@ +\errorcontextlines=20 +\documentclass[a4paper]{article} +\advance\textwidth by 1in +\advance\textheight by 1in +\advance\oddsidemargin by -0.5in +\advance\topmargin by -0.5in +\usepackage{oz} +\usepackage{example} +\usepackage{multicol} +% +% just ignore any over- or under-full hboxes +% this document uses most of the (physical) page and isn't spread +% out either. This may make it slightly harder to read first time +% through, but makes it more suitable for later reference. +% +% before we start, let's make a few definitions +% +\makeatletter +%\def\example{\begin{sidebyside}} +%\def\verbpart{\nextside\small\vspace*{-1ex}\begin{quote}\begin{verbatim}} +%\def\endexample{\end{quote}\vspace*{-2ex}\end{sidebyside}\vspace*{-3ex}\ignorespaces} +\def\symbol#1{#1 & \tt\string#1} +\def\symbols{\@ifnextchar[{\@symbols}{\@symbols[0]}} +\def\@symbols[#1]{\interzedlinepenalty=\interdisplaylinepenalty\z@env + \openup #1\jot + \halign\bgroup\zstrut\hbox to 3.8em{$##$\hss}\tabskip=0pt&##\hss\cr + \noalign{\vskip-#1\jot}}% equal vspace above and below argue display +\let\endsymbols=\endzed +\makeatother +% +\begin{document} +\begin{center} +{\Large\bf Printing Z and Object-Z \LaTeX\ documents}\\[2.5ex] +{\em Paul King}\\[1ex] +Department of Computer Science\\ +University of Queensland\\ +Australia, 4072\\ +king@batserver.cs.uq.oz.au\\[1ex] +May 29, 1990 +\end{center} + +\section{Introduction} +This note describes a package of \LaTeX\ macros for printing +Z and Object-Z specifications. The macros and this note are +based originally on Mike Spivey's \verb'zed.sty' macros and documentation. +The package does several related things for you: +\begin{itemize} +\item It loads extra fonts and defines mnemonics + for the Z symbols they contain. +\item It defines macros for some Z symbols (e.g. $\pinj$) which + don't appear in any of our fonts. +\item It fixes the way \TeX\ sets letters in mathematical formulas so + that multi-character identifiers look better. +\item It provides various brands of `boxed mathematics' + which appear in Z and Object-Z specifications. +\end{itemize} + +The package is kept in a file {\tt oz.sty} +in the directory \verb|/usr/local/lib/tex/localinputs|. +This directory should be mentioned in your \verb|TEXINPUTS| shell variable. +To use the macros you just begin your \LaTeX\ document with something like: +\begin{quote} +\begin{verbatim} +\documentstyle[11pt,oz]{article} +\end{verbatim} +\end{quote} +\vspace*{-1.5ex} + +\section{Schema Boxes} + +The example below shows a schema on the left and what you +need to say to get it on the right. + +\begin{example} +\begin{schema}{BirthdayBook} + known: \pset NAME \\ + birthday: NAME \pfun DATE +\ST + known = \dom birthday +\end{schema} +\end{example} + +The command \verb|\ST| (read `Such That') is the same as the previously used +command \verb|\where| which has been kept as an alias for upward compatibility. +If you want a schema with no name, just a horizontal rule at the top, +use the \verb|schema*| environment instead. +You can set various parameters (see Section 7) to change the box style, +for example: + +\begin{example} +$BirthdayBook \sdef \lsch ... \rsch$ +\end{example} + +A generic schema is produced as follows. + +\begin{example} +\begin{genschema}{Pool}{RESOURCE} +owner : RESOURCE \pfun USER \\ +free : \pset RESOURCE +\ST +(\dom owner) \uni free = RESOURCE \\ +(\dom owner) \int free = \emptyset +\end{genschema} +\end{example} + +\section{Axiomatic definitions} + +A `liberal' axiomatic definition is produced as follows. + +\begin{example} +\begin{axdef} +limit : \nat +\ST +limit \leq 65536 +\end{axdef} +\end{example} + +A `generic' axiomatic definition is produced as follows. + +\begin{example} +\begin{gendef}{X,Y} +first : X \prod Y \tfun X +\ST +\all x : X; y : Y \dot first(x,y) = x +\end{gendef} +\end{example} + +A `unique' axiomatic definition is produced as follows. + +\begin{example} +\begin{uniqdef} +\pi : \real +\ST +\pi = 3.14159265\ldots +\end{uniqdef} +\end{example} + +\section{Object-Z Class Boxes} + +Object-Z allows class types to be defined using a box very similar to +the schema box previously described. It allows the previously +described boxed environments (as well as nested sub-classes) to be +placed within a class box. In addition, special names can be used for +some of the boxed-environments when they appear within a class box. +The following example illustrates a class definition. + +\begin{example} +\begin{class}{Shape} +\also +colour : Colour \\ +\begin{axdef} +perim : \real +\ST +perim > 0 +\end{axdef} \\ +\begin{classcom} +This class has 2 constants +$colour$ and $perim$. +\end{classcom} \\ +\begin{state} +x, y : \real +\end{state} \\ +\begin{init} +x = y = 0 +\end{init} \\ +\begin{op}{Translate} +\Delta (x,y) \\ +dx?, dy? : \real +\ST +x' = x + dx? \\ +y' = y + dy? +\end{op} +\end{class} +\end{example} + +The \verb|classcom| environment hasn't been seen before. +It creates a paragraph of text with the same margins as used +for schemas and other Z environments. It uses a special font +intended for use when placing comments inside classes. +A similar environment, \verb|zpar|, uses the same margins +but with the normal roman font. + +The \verb|\begin{init}| command is an abbreviation for +\verb|\begin{schema}{\Init}|. Similarly \verb|\begin{state}| +is a more meaningful synonym for \verb|\begin{schema*}|. + +You will be given \LaTeX\ warning messages if you try to +use a \verb|state| environment outside of a class box +or if you try to place an environment such as \verb|syntax| +inside a class. You can ask for additional help in these +cases using the normal \LaTeX\ \verb|h| or \verb|H| help commands. +If you proceed with \LaTeX ing, the macros will attempt to +do the best they can to do what you probably intend, even though +you are violating the recommended nesting guidelines. + +\section{Controlling the Spacing within Equations and Boxes} + +Most of the special Z symbols are defined +in a way that allows \TeX\ to space them out correctly. +Sometimes, however, you'll need to give \TeX\ a helping hand if +you want it to get the spacing right. For example, to get $map\,f$ +you need to type \verb|map\,f|. The \verb|\,| gives you a thin space: +if this is omitted, the input \verb|map f| gives +$map f$, because \TeX\ ignores spaces in math mode. + +Sometimes it is useful to indent the left margin to emphasis +the logical structure of the predicate. +The command \verb|\t1| does this by making the corresponding +line in the output have one helping of indentation. +As things get more nested, you can say \verb|\t2|, \verb|\t3|, and so on. +But if you should ever get beyond \verb|t9|, you'll need to use braces +around the argument: \verb|\t{10}|, and you'd better look for some way +to simplify your specification! +These little tab marks might look different to normal tabs +but are never the less convenient. They're short, +and they don't get longer as the tabbing gets deeper, within reason, +so they can be tucked in neatly on the left, well away from the maths. +The size of `helping' you get with \verb|\t| is determined by +the \verb|\zedtab| parameter (see Section 7). + +If you want a more powerful aligning mechanism than tabbing +then you can use the margin stack as shown in the example below. +The command \verb|\M| sets the future left margin to the current +horizontal position and pushes the old value onto a margin stack. +The command \verb|\O| resets the left margin to its previous value +(which is popped off the stack). + +\begin{example} +\begin{schema}{Test} +x, y : \nat +\ST +x + 1/x = 0 \imp \M y + 1/y = 0 \\ +y = x \O \\ +\end{schema} +\end{example} + +If a schema or other box contains more than one predicate below the +line, it often looks better to add a tiny vertical space between +them, as in this example: + +\begin{example} +\begin{schema}{AddBirthday} + \Delta BirthdayBook \\ + n?: NAME \\ + d?: DATE +\ST + n? \nem known +\also + birthday'=birthday \uni \{n? \map d?\} +\end{schema} +\end{example} + +This is done with the command \verb|\also|, which behaves syntactically +like \verb|\ST|. +The command \verb|\also| is provided {\em instead\/} of the +optional argument to \verb|\\| +which \LaTeX\ provides in other environments. +If larger vertical spacing is required, the commands +\verb|\Also| and \verb|\ALSO| may be used (giving 2 and 4 times +as much space as \verb|\also| respectively). + +Normally, the contents of a schema box are kept on a single page. +For large schemas it may be necessary to split the box across pages. +You must specify which places are suitable for splitting using one of +\verb|\zbreak|, \verb|\Zbreak| or \verb|\ZBREAK|. If no split is +performed at this point, a vertical space will be added as if the +user had typed \verb|\also|, \verb|\Also|, or \verb|\ALSO| respectively. +You can also use the \verb|\znewpage| command to force a page break within +a box. (These breaking facilities will hopefully never be needed for schemas, +but may become necessary for class specifications.) + +\section{Other Display Environments} + +The \verb|zed| environment can be used to set multi-line formulas without +an enclosing box: it is useful for given-set declarations, theorems, and the +miscellaneous bits of mathematics that don't come in a box: + +\vspace{-1ex}\begin{example} +\begin{zed} + \all n: \nat \dot \\ +\t1 n+n \mem even. +\end{zed} +\end{example} + +The formula \verb|\begin{zed} ... \end{zed}| may be abbreviated to +\verb|\[ ... \]|; the \verb|zed| environment is a generalization of the +\verb|displaymath| environment of \LaTeX, so this redefinition of +commands is fairly benign. Notice that the maths is set flush left on the +same indentation as schemas and their friends. +Here too you can use \verb|\also| for a little extra space +between lines. + +For algebraic-style proofs, there is the \verb|argue| environment. +This is like the \verb|zed| environment, but the separation between +lines is increased a little, and page breaks may occur between lines. +When the left-hand side is long this style wastes less space +than the \LaTeX\ \verb|eqnarray| style. +The intended use is for arguments like this: +\begin{argue} + rev(append(cons(x,s),t)) \\ +\t1 = rev(cons(x,append(s,t))) \\ +\t1 = append(rev(append(s,t)),cons(x,nil)) \\ +\t1 = append(append(rev(t),rev(s)),cons(x,nil)) + \quad \hbox{by hypothesis} \\ +\t1 = append(rev(t),append(rev(s),cons(x,nil))) \\ +\t1 = append(rev(t),rev(cons(x,s))). +\end{argue} +Here is the input: +\begin{quote} +\begin{verbatim} +\begin{argue} + rev(append(cons(x,s),t)) \\ +\t1 = rev(cons(x,append(s,t))) \\ +\t1 = append(rev(append(s,t)),cons(x,nil)) \\ +\t1 = append(append(rev(t),rev(s)),cons(x,nil)) + \quad \hbox{by hypothesis} \\ +\t1 = append(rev(t),append(rev(s),cons(x,nil))) \\ +\t1 = append(rev(t),rev(cons(x,s))). +\end{argue} +\end{verbatim} +\end{quote} + +The example below shows an inference rule (the optional argument +to \verb|\derive| gives a side-condition of the rule): + +\vspace{-1ex}\begin{example} +\begin{infrule} + \Gamma \shows P +\derive[x \nem freevars(\Gamma)] + \Gamma \shows \all x \dot P +\end{infrule} +\end{example} + +The \verb|syntax| environment is used for making displays like this: + +\begin{syntax} + EXPR & \ddef & IDENT & identifier \\ + & \bbar & EXPR\;EXPR & application \\ + & \bbar & \lambda IDENT \dot EXPR & lambda-abstraction. +\end{syntax} +from input like this: +\begin{quote} +\begin{verbatim} +\begin{syntax} + EXPR & \ddef & IDENT & identifier \\ + & \bbar & EXPR\;EXPR & application \\ + & \bbar & \lambda IDENT \dot EXPR & lambda-abstraction. +\end{syntax} +\end{verbatim} +\end{quote} + +This kind of thing is useful when you're describing a language, +and it can also be used for data-type definitions as shown below. +The optional final column was omitted below by leaving out the third \verb|&|. + +\begin{example} +\begin{syntax} +TYPE & \ddef & givenT \lang NAME \rang \\ +& \bbar & powerT \lang TYPE \rang \\ +& \bbar & tupleT \lang \seq TYPE \rang \\ +& \bbar & schemaT \lang IDENT \ffun TYPE \rang \\ +& \bbar & classT \lang IDENT \ffun ClassAttr \rang +\end{syntax} +\end{example} + +This can be compared with the layout adopted by the UQ Z editor (version 1). + +\begin{example} +\begin{zed} +TYPE \ddef \M givenT \lang NAME \rang \\ +\bbar powerT \lang TYPE \rang \\ +\bbar tupleT \lang \seq TYPE \rang \\ +\bbar schemaT \lang IDENT \ffun TYPE \rang \\ +\bbar classT \lang IDENT \ffun ClassAttr \rang \O +\end{zed} +\end{example} + +The {\tt sidebyside} environment allows a display as shown in the +first two columns below to be produced from the text of the third column. +Note the use of the \verb|\comment| command. + +\begin{example} +\begin{sidebyside} +\begin{schema}{Schema} +\comment*{declarations} +\ST +a < b \comment{pred-1} \\ +aaaaa < bbbbb \comment{pred-2} +\end{schema} +\nextside +\begin{zpar} +This is a paragraph which has the same +margins as the standard schemas do. +\end{zpar} +\end{sidebyside} +\end{example} + +In fact, this environment was used throughout this note to +display the examples beside the required input text. +Incidentally, the above example shows that \verb|sidebyside| +environments can be nested; so what the author of this note typed +to get the above display was: + +\begin{quote} +\begin{verbatim} +\begin{sidebyside} + \begin{sidebyside} + ... + \nextside + ... + \end{sidebyside} +\nextside + ... +\end{sidebyside} +\end{verbatim} +\end{quote} + +This resulted in the first two columns being equally spaced and +together taking up as much space as the third column. +You can have more than 2 columns without nesting by specifying an optional +parameter to \verb|sidebyside|. For example, the display below has three +equally spaced columns obtained using \verb|\begin{sidebyside}[3]|. + + \begin{sidebyside}[3] + \begin{schema}{BirthdayBook} + known: \pset NAME \\ + birthday: NAME \pfun DATE + \ST + known = \dom birthday + \end{schema} + \nextside + \begin{schema}{BirthdayBook} + known: \pset NAME \\ + birthday: NAME \pfun DATE + \ST + known = \dom birthday + \end{schema} + \nextside + \begin{zpar} +Don't get carried away with \verb|sidebyside| + like this example does. + \end{zpar} + \end{sidebyside} + +\section{Style Parameters} + +\begin{description} +\item[\tt\string\zedindent] The (horizontal) indentation for mathematical text. + By default, this is the same as \verb|\leftmargini|, the indentation + used for list environments. +\item[\tt\string\zedleftsep] The (horizontal) space between the vertical line on the left + of schemas, etc., and the maths inside. The default is 1em. +\item[\tt\string\zedtab] The unit of indentation used by \verb|\t|. The default + is 2em. +\item[\tt\string\zedbar] The length of the horizontal bar in the middle of a + schema. The default is 8em. +\item[\tt\string\leftschemas] A declaration which makes schema names be + set flush left. Use it in the document preamble. +\item[\tt\string\zedlinethickness] The thickness of the lines that make up + schema and class boxes. You can change the thickness + with a command such as \verb|\zedlinethickness=0.1pt|. This may + be useful if you are creating overhead slides. + \begin{description} + \makeatletter + \item[0.1pt] \zedlinethickness=0.1pt + ~\hbox to 4cm{\z@hrulefill} + \item[0.4pt] \zedlinethickness=0.4pt + ~\hbox to 4cm{\z@hrulefill}~~~(The default) + \item[\hphantom{0.}1pt] \zedlinethickness=1pt + ~\hbox to 4cm{\z@hrulefill} + \end{description} +\item[\tt\string\baselinestretch] The spacing for the text part of your + document. It doesn't change the spacing within Z environments. It's + default value is 1. A command such as \verb|\def\baselinestretch{2}| + will make your text double spaced, but not your Z environments. +\item[\tt\string\zedbaselinestretch] The spacing for the Z environment + part of your document. It's default value is 1. +\item[\tt\string\zedsize] The size of the material within the Z + part of your document. It doesn't affect the remainder of your document. + For example, \verb|\zedsize{\large}| will give you large Z symbols + and equations but will not affect the size of the surrounding text. +\item[\tt\string\zedcornerheight] The height of `corners' that can be placed + on the right hand side of the top and bottom lines of schema and class + boxes. The default is 0em (i.e. no corners). +\end{description} + +\section{Symbols} + +Multi-letter identifiers have been changed to look +better than they do with vanilla \LaTeX: instead of +$\mathit{specifications}$, you get $specifications$. +The letters haven't been spread apart, and the +ligature $fi$ has been used. + +Almost all of the mathematical symbols of \LaTeX\ can be used; +some have been redefined---usually to fix the spacing so that it is +suitable for Z specifications. +The commands for obtaining additional symbols are listed below. +Sometimes more than one command may produce a symbol you +require. You should use the one that seems to be designed for the +context you have in mind. This is because the spacing around (and size of) +symbols has been chosen for their typical context. + +Throughout the lifetime of these macros a number of alternate control +sequences for any symbol may have existed. A list of aliases has been +set up so that old commands may still be used. It is +recommended however that you stick to the recommended command +names for symbols as these names may be supported by other tools. +Within the table below non-recommended aliases are surrounded by +brackets, e.g., \verb|(\power)|. +\begin{multicols}{2} +\setcounter{secnumdepth}{2} +\zedindent=0.2\zedindent +\subsection{Special Z Notation} +\vspace*{-0.5ex} +\subsubsection{Numbers} +\vspace*{-2.5ex} +\begin{symbols} +\nat & \verb' \nat' \\ +\natone & \verb' \natone (\nplus)' \\ +\integer & \verb' \integer (\num)' \\ +\real & \verb' \real' \\ +\div~\mod & \verb' \div \mod' \\ +i^n & \verb' i^n i\expon n' \\ +\succ & \verb' \succ' \\ +%\prec & \verb' \prec' \\ +=~\neq & \verb' = \neq' \\ +<~\leq~\leqslant & \verb' < \leq \leqslant' \\ +>~\geq~\geqslant & \verb' > \geq \geqslant' \\ +*\,/\,+ - & \verb' * / + -' \\ +\end{symbols} +\subsubsection{Logic} +\vspace*{-2.5ex} +\begin{symbols} +\lnot & \verb'\lnot' \\ +\land & \verb'\land (\wedge)' \\ +\lor & \verb'\lor (\vee)' \\ +\all & \verb'\all (\forall)' \\ +\exi & \verb'\exi (\exists)' \\ +\exi_1 & \verb'\exione' \\ +\nexi & \verb'\nexi (\nexists)' \\ +\dot & \verb'@ \dot (\spot)' \\ +%\cond & \verb'\cond' \\ +\imp & \verb'\imp (\implies)' \\ +\iff & \verb'\iff' \\ +\true & \verb'\true' \\ +\false & \verb'\false' \\ +\bool & \verb'\bool' \\ +\end{symbols} +\subsubsection{Sets} +\vspace*{-2.5ex} +\begin{symbols} +\{~~\cbar~~\} & \verb' \{ \cbar \}' \\ +\emptyset & \verb' \emptyset' \\ +\varemptyset & \verb' \varemptyset' \\ +\mem & \verb' \mem (\in)' \\ +\nmem & \verb' \nem (\nmem \notin)' \\ +\pset & \verb' \pset (\power)' \\ +\fset & \verb' \fset (\finset)' \\ +\psetone~~\fsetone & \verb' \fsetone \psetone' \\ +\uni & \verb' \uni (\union)' \\ +\int & \verb' \int (\inter)' \\ +\psubs & \verb' \psubs (\subset)' \\ +\subs & \verb' \subs (\subseteq)' \\ +\psups & \verb' \psups (\supset)' \\ +\sups & \verb' \sups (\supseteq)' \\ +\prod & \verb' \prod (\cross)' \\ +\min~\max & \verb' \min \max' \\ +\# & \verb' \#' \\ +\duni & \verb' \duni (\dunion)' \\ +\dint & \verb' \dint (\dinter)' \\ +\upto & \verb' \upto' \\ +\end{symbols} + +\subsubsection{Relations and Functions} +\vspace*{-2.5ex} +\begin{symbols}[0.1] +\lambda~~~\mu & \verb'\lambda \mu' \\ +\dom & \verb'\dom' \\ +\ran & \verb'\ran' \\ +\dres & \verb'\dres' \\ +\dsub & \verb'\dsub (\ndres)' \\ +\rres & \verb'\rres' \\ +\rsub & \verb'\rsub (\nrres)' \\ +\fovr & \verb'\fovr' \\ +\cmp & \verb'\cmp' \\ +\fcmp & \verb'\fcmp (\comp)' \\ +(\!|~~~|\!) & \verb'\limg \rimg' \\ +\id & \verb'\id' \\ +R\inv & \verb'R^{-1} R\inv' \\ +R^+ & \verb'R^+ R\tcl' \\ +R^* & \verb'R^* R\rtcl' \\ +R^k & \verb'R^k R\iter k' \\ +iter\,0\,R & \verb'iter \, 0 \, R' \\ +\map & \verb'\map' \\ +\rel & \verb'\rel' \\ +\tfun & \verb'\tfun (\fun)' \\ +\tinj & \verb'\tinj (\inj)' \\ +\tsur & \verb'\tsur (\surj)' \\ +\pfun & \verb'\pfun' \\ +\pinj & \verb'\pinj' \\ +\psur & \verb'\psur (\psurj)' \\ +\ffun & \verb'\ffun' \\ +\finj & \verb'\finj' \\ +\bij & \verb'\bij' \\ +\end{symbols} +\subsubsection{Sequences} +\vspace*{-2.5ex} +\begin{symbols} +\seq & \verb' \seq' \\ +\seqone & \verb' \seqone' \\ +\emptyseq & \verb' \emptyseq' \\ +\lseq~~~\rseq & \verb' \lseq \rseq' \\ +\head~~\tail & \verb' \head \tail' \\ +\front~~\last & \verb' \front \last' \\ +\rev & \verb' \rev' \\ +\next & \verb' \next' \\ +\inseq & \verb' \inseq' \\ +\prefix & \verb' \prefix' \\ +\suffix & \verb' \suffix' \\ +\squash & \verb' \squash' \\ +\cat & \verb' \cat' \\ +\dcat & \verb' \dcat' \\ +\dcmp & \verb' \dcmp' \\ +\dovr & \verb' \dovr' \\ +\ires & \verb' \ires' \\ +\sres & \verb' \sres \filter' \\ +\partitions & \verb' \partitions' \\ +\disjoint & \verb' \disjoint' \\ +\end{symbols} + +\subsubsection{Schemas} +\vspace*{-2.5ex} +\begin{symbols} +\Delta & \verb'\Delta' \\ +\equiv~~\Xi & \verb'\equiv \Xi' \\ +\pred & \verb'\pred' \\ +\pre & \verb'\pre' \\ +\post & \verb'\post' \\ +\project & \verb'\zproject \project' \\ +\zand & \verb'\zand' \\ +\zor & \verb'\zor' \\ +\zcmp & \verb'\zcmp (\semi)' \\ +\zexi & \verb'\zexi' \\ +\zall & \verb'\zall' \\ +\znot & \verb'\znot' \\ +\zhide & \verb'\zhide (\hide)' \\ +\zfor & \verb'\zfor' \\ +\zimp & \verb'\zimp' \\ +\zeq & \verb'\zeq' \\ +\zovr & \verb'\zovr' \\ +\zpipe & \verb'\zpipe' \\ +\theta & \verb'\theta' \\ +\lsch~~\zbar~~\rsch & \verb'\lsch \zbar \rsch' \\ +.. & \verb'.' \\ +\end{symbols} +\subsubsection{Bags} +\vspace*{-2.5ex} +\begin{symbols} +\lbag~~~\rbag & \verb'\lbag \rbag' \\ +\bag & \verb'\bag' \\ +\emptybag & \verb'\emptybag' \\ +\items & \verb'\items' \\ +\bagcount & \verb'\bagcount' \\ +\buni & \verb'\buni' \\ +\inbag & \verb'\inbag' \\ +\end{symbols} +\subsubsection{Definitions and Declarations} +\vspace*{-2.5ex} +\begin{symbols} +::= & \verb'\ddef' \\ +\bbar & \verb'\bbar' \\ +== & \verb'\defs' \also +\widehat= & \verb'\sdef' \also +\triangleq & \verb'\varsdef' \\ +,~~\semicolon~~: & \verb', ; :' \\ +\lang~~~\rang & \verb'\lang \rang' \\ +\end{symbols} +\subsubsection{Miscellaneous} +\vspace*{-2.5ex} +\begin{symbols}[0] +[~~~] & \verb'[ ]' \\ +(~~~) & \verb'( )' \\ +!~~~? & \verb'! ?' \\ +\zlet & \verb'\zlet' \\ +\zwhere & \verb'\zwhere' \\ +\zin & \verb'\zin' \\ +\langle\!|~~~|\!\rangle & \verb'\lblot \rblot' \\ +\intern Bump & \verb'\intern Bump' \\ +\Init & \verb'\Init'\\ +\Exit & \verb'\Exit' +\end{symbols} + +\subsection{Other Special Notation} +\vspace*{-1ex} +\subsubsection{Temporal Logic} +\vspace*{-2.5ex} +\begin{symbols} +\always~\uptilnow & \verb'\always \uptilnow' \\ +~&\verb'(\henceforth)'\\ +\atnext~\atlast & \verb'\atnext \atlast' \\ +\eventually~\previously & \verb'\eventually \previously' \\ +\end{symbols} +\subsubsection{Proofs} +\vspace*{-2.5ex} +\begin{symbols}[0.1] +\TH & \verb' \TH' \\ +\PR & \verb' \PR' \\ +\LE & \verb' \LE' \\ +\ETH~\Qed & \verb' \qed (\ETH) \Qed' \\ +\QED~\BLACKQED & \verb' \QED \BLACKQED' \\ +\vdash & \verb' \shows (\thrm)' \\ +\vDash & \verb' \vDash' \\ +\refines & \verb' \refines' \\ +\weakrefine & \verb' \weakrefine' \\ +\end{symbols} +\subsubsection{Object Theory} +\vspace*{-2.5ex} +\begin{symbols} +\subclass & \verb'\subclass \isa' \\ +\weaksubclass & \verb'\weaksubclass \islikea' \\ +\supclass & \verb'\supclass' \\ +\weaksupclass & \verb'\weaksupclass' \\ +\hasa & \verb'\hasa \instantiates' \\ +\instancein & \verb'\instancein' \\ +\subtype~~\subtypeeq & \verb'\subtype \subtypeeq' \\ +\suptype~~\suptypeeq & \verb'\suptype \suptypeeq' \\ +\end{symbols} +\subsubsection{Orders} +\vspace*{-2.5ex} +\begin{symbols} +\mono & \verb' \mono' \\ % these lines fudged to give more spacing +\torder & \verb' \torder' \\ +\porder & \verb' \porder' \\ +\end{symbols} +\subsubsection{Word Styles} +\vspace*{-2.5ex} +\begin{symbols}[0.4] +\word{word} & \verb'\word{word}' \\ +\keyword{word} & \verb'\keyword{word}' \\ +\boldword{word} & \verb'\boldword{word}' \\ +\underword{word} & \verb'\underword{word}' \\ +\underkeyword{word} & \verb'\underkeyword{word}' \\ +\underboldword{word} & \verb'\underboldword{word}' \\ +\String{word} & \verb'\String{word}' \\ +\STRING{word} & \verb'\STRING{word}' \\ +a \infix{rel} b & \verb'a \infix{rel} b' \\ +\end{symbols} + +\subsection{Special Letter Fonts} +\vspace*{-1ex} +\subsubsection{Greek} +\vspace*{-2.5ex} +\begin{symbols} +\alpha & \verb'\alpha' \\ +\beta & \verb'\beta' \\ +\gamma~\Gamma & \verb'\gamma \Gamma' \\ +\delta~\Delta & \verb'\delta \Delta' \\ +\epsilon~\varepsilon & \verb'\epsilon \varepsilon' \\ +\zeta & \verb'\zeta' \\ +\eta & \verb'\eta' \\ +\theta~\vartheta~\Theta & \verb'\theta \vartheta \Theta' \\ +\iota & \verb'\iota' \\ +\kappa~\varkappa & \verb'\kappa \varkappa' \\ +\lambda~\Lambda & \verb'\lambda \Lambda' \\ +\mu & \verb'\mu' \\ +\nu & \verb'\nu' \\ +\xi~\Xi & \verb'\xi \Xi' \\ +\pi~\varpi~\Pi & \verb'\pi \varpi \Pi' \\ +\rho~\varrho & \verb'\rho \varrho' \\ +\sigma~\varsigma~\Sigma & \verb'\sigma \varsigma \Sigma' \\ +\tau & \verb'\tau' \\ +\upsilon~\Upsilon & \verb'\upsilon \Upsilon' \\ +\phi~\varphi~\Phi & \verb'\phi \varphi \Phi' \\ +\chi & \verb'\chi' \\ +\psi~\Psi & \verb'\psi \Psi' \\ +\omega~\Omega & \verb'\omega \Omega' \\ +\end{symbols} +\subsubsection{Caligraphic} +\vspace*{-2.5ex} +\begin{symbols} +\mathcal{A} & \verb'\mathcal{A}' \\ +\mathcal{B} & \verb'\mathcal{B}' \\ +\mathcal{C} & \verb'\mathcal{C}' \\ +\mathcal{D} & \verb'\mathcal{D}' \\ +\mathcal{E} & \verb'\mathcal{E}' \\ +\mathcal{F} & \verb'\mathcal{F}' \\ +\mathcal{G} & \verb'\mathcal{G}' \\ +\mathcal{H} & \verb'\mathcal{H}' \\ +\mathcal{I} & \verb'\mathcal{I}' \\ +\mathcal{J} & \verb'\mathcal{J}' \\ +\mathcal{K} & \verb'\mathcal{K}' \\ +\mathcal{L} & \verb'\mathcal{L}' \\ +\mathcal{M} & \verb'\mathcal{M}' \\ +\mathcal{N} & \verb'\mathcal{N}' \\ +\mathcal{O} & \verb'\mathcal{O}' \\ +\mathcal{P} & \verb'\mathcal{P}' \\ +\mathcal{Q} & \verb'\mathcal{Q}' \\ +\mathcal{R} & \verb'\mathcal{R}' \\ +\mathcal{S} & \verb'\mathcal{S}' \\ +\mathcal{T} & \verb'\mathcal{T}' \\ +\mathcal{U} & \verb'\mathcal{U}' \\ +\mathcal{V} & \verb'\mathcal{V}' \\ +\mathcal{W} & \verb'\mathcal{W}' \\ +\mathcal{X} & \verb'\mathcal{X}' \\ +\mathcal{Y} & \verb'\mathcal{Y}' \\ +\mathcal{Z} & \verb'\mathcal{Z}' \\ +\end{symbols} +\subsubsection{BlackBoard Bold} +\vspace*{-2.5ex} +\begin{symbols} +\mathbb A & \verb'\mathbb A' \\ +\mathbb B & \verb'\mathbb B' \\ +\mathbb C & \verb'\mathbb C' \\ +\mathbb D & \verb'\mathbb D' \\ +\mathbb E & \verb'\mathbb E' \\ +\mathbb F & \verb'\mathbb F' \\ +\mathbb G & \verb'\mathbb G' \\ +\mathbb H & \verb'\mathbb H' \\ +\mathbb I & \verb'\mathbb I' \\ +\mathbb J & \verb'\mathbb J' \\ +\mathbb K & \verb'\mathbb K' \\ +\mathbb L & \verb'\mathbb L' \\ +\mathbb M & \verb'\mathbb M' \\ +\mathbb N & \verb'\mathbb N' \\ +\mathbb O & \verb'\mathbb O' \\ +\mathbb P & \verb'\mathbb P' \\ +\mathbb Q & \verb'\mathbb Q' \\ +\mathbb R & \verb'\mathbb R' \\ +\mathbb S & \verb'\mathbb S' \\ +\mathbb T & \verb'\mathbb T' \\ +\mathbb U & \verb'\mathbb U' \\ +\mathbb V & \verb'\mathbb V' \\ +\mathbb W & \verb'\mathbb W' \\ +\mathbb X & \verb'\mathbb X' \\ +\mathbb Y & \verb'\mathbb Y' \\ +\mathbb Z & \verb'\mathbb Z' \\ +\end{symbols} +\subsubsection{Miscellaneous} +\vspace*{-2.5ex} +\begin{symbols} +\hslash & \verb'\hslash' \\ +\hbar & \verb'\hbar' \\ +\backepsilon & \verb'\backepsilon' \\ +\eth & \verb'\eth' \\ +\beth & \verb'\beth' \\ +\gimel & \verb'\gimel' \\ +\daleth & \verb'\daleth' \\ +\complement & \verb'\complement' \\ +\intercal & \verb'\intercal' \\ +\aleph & \verb'\aleph' \\ +\nabla & \verb'\nabla' \\ +\hbar & \verb'\hbar' \\ +\imath & \verb'\imath' \\ +\jmath & \verb'\jmath' \\ +\ell & \verb'\ell' \\ +\wp & \verb'\wp' \\ +\Re & \verb'\Re' \\ +\Im & \verb'\Im' \\ +\mho & \verb'\mho' \\ +\digamma & \verb'\digamma' \\ +\end{symbols} + +\subsection{Shapes} +\vspace*{-2ex} +\begin{symbols} +\Box & \verb'\Box' \\ +\square & \verb'\square' \\ +\blacksquare & \verb'\blacksquare' \\ +\diamond & \verb'\diamond' \\ +\Diamond & \verb'\Diamond' \\ +\lozenge & \verb'\lozenge' \\ +\blacklozenge & \verb'\blacklozenge' \\ +\vartriangleright & \verb'\vartriangleright' \\ +\vartriangleleft & \verb'\vartriangleleft' \\ +\blacktriangledown & \verb'\blacktriangledown' \\ +\blacktriangleright & \verb'\blacktriangleright' \\ +\blacktriangleleft & \verb'\blacktriangleleft' \\ +\vartriangle & \verb'\vartriangle' \\ +\blacktriangle & \verb'\blacktriangle' \\ +\triangledown & \verb'\triangledown' \\ +\triangle & \verb'\triangle' \\ +\triangleleft & \verb'\triangleleft' \\ +\triangleright & \verb'\triangleright' \\ +\bigtriangleup & \verb'\bigtriangleup' \\ +\bigtriangledown & \verb'\bigtriangledown' \\ +\clubsuit & \verb'\clubsuit' \\ +\diamondsuit & \verb'\diamondsuit' \\ +\heartsuit & \verb'\heartsuit' \\ +\spadesuit & \verb'\spadesuit' \\ +\ast & \verb'\ast' \\ +\star & \verb'\star' \\ +\maltese & \verb'\maltese' \\ +\bigstar & \verb'\bigstar' \\ +\bigcirc & \verb'\bigcirc' \\ +\circ & \verb'\circ' \\ +\bullet & \verb'\bullet' \\ +\centerdot & \verb'\centerdot' \\ +\cdot & \verb'\cdot' \\ +\cdots & \verb'\cdots' \\ +\ldots & \verb'\ldots' \\ +\vdots & \verb'\vdots' \\ +\ddots & \verb'\ddots' \\ +\end{symbols} +\subsubsection{Circled Operations} +\vspace*{-2.5ex} +\begin{symbols} +\circledS & \verb'\circledS' \\ +\circledcirc & \verb'\circledcirc' \\ +\circledast & \verb'\circledast' \\ +\circleddash & \verb'\circleddash' \\ +\circledR & \verb'\circledR' \\ +\copyright & \verb'\copyright' \\ +\fovr & \verb'\fovr' \\ +\ominus & \verb'\ominus' \\ +\otimes & \verb'\otimes' \\ +\oslash & \verb'\oslash' \\ +\odot & \verb'\odot' \\ +\end{symbols} + +\subsubsection{Boxed operators} +\vspace*{-2.5ex} +\begin{symbols}[0.2] +\boxdot & \verb'\boxdot' \\ +\boxplus & \verb'\boxplus' \\ +\boxtimes & \verb'\boxtimes' \\ +\boxminus & \verb'\boxminus' \\ +\end{symbols} +\subsection{Arrow Symbols} +\vspace*{-1ex} +\subsubsection{Left Arrows} +\vspace*{-2.5ex} +\begin{symbols}[0.7] +\leftarrow & \verb'\leftarrow \gets' \\ +\Leftarrow & \verb'\Leftarrow' \\ +\hookleftarrow & \verb'\hookleftarrow' \\ +\leftharpoonup & \verb'\leftharpoonup' \\ +\leftharpoondown & \verb'\leftharpoondown' \\ +\longleftarrow & \verb'\longleftarrow' \\ +\Longleftarrow & \verb'\Longleftarrow' \\ +\twoheadleftarrow & \verb'\twoheadleftarrow' \\ +\leftleftarrows & \verb'\leftleftarrows' \\ +\leftarrowtail & \verb'\leftarrowtail' \\ +\Lleftarrow & \verb'\Lleftarrow' \\ +\nleftarrow & \verb'\nleftarrow' \\ +\nLeftarrow & \verb'\nLeftarrow' \\ +\end{symbols} + +\subsubsection{Right Arrows} +\begin{symbols}[0.7] +\rightarrow & \verb'\rightarrow \to' \\ +\Rightarrow & \verb'\Rightarrow' \\ +\map & \verb'\map' \\ +\longmapsto & \verb'\longmapsto' \\ +\hookrightarrow & \verb'\hookrightarrow' \\ +\rightharpoonup & \verb'\rightharpoonup' \\ +\rightharpoondown & \verb'\rightharpoondown' \\ +\leadsto & \verb'\leadsto' \\ +\longrightarrow & \verb'\longrightarrow' \\ +\Longrightarrow & \verb'\Longrightarrow' \\ +\twoheadrightarrow & \verb'\twoheadrightarrow' \\ +\rightrightarrows & \verb'\rightrightarrows' \\ +\rightarrowtail & \verb'\rightarrowtail' \\ +\rightsquigarrow & \verb'\rightsquigarrow' \\ +\Rrightarrow & \verb'\Rrightarrow' \\ +\nrightarrow & \verb'\nrightarrow' \\ +\nRightarrow & \verb'\nRightarrow' \\ +\end{symbols} + +\subsubsection{Left Right Arrows} +\begin{symbols}[0.6] +\leftrightarrow & \verb'\leftrightarrow' \\ +\Leftrightarrow & \verb'\Leftrightarrow' \\ +\rightleftharpoons & \verb'\rightleftharpoons' \\ +\longleftrightarrow & \verb'\longleftrightarrow' \\ +\Longleftrightarrow & \verb'\Longleftrightarrow' \\ +\rightleftharpoons & \verb'\rightleftharpoons' \\ +\leftrightharpoons & \verb'\leftrightharpoons' \\ +\leftrightarrows & \verb'\leftrightarrows' \\ +\rightleftarrows & \verb'\rightleftarrows' \\ +\leftrightsquigarrow & \verb'\leftrightsquigarrow' \\ +\nLeftrightarrow & \verb'\nLeftrightarrow' \\ +\nleftrightarrow & \verb'\nleftrightarrow' \\ +\end{symbols} + +\subsubsection{Up Down Arrows} +\begin{symbols}[1] +\uparrow & \verb'\uparrow' \\ +\Uparrow & \verb'\Uparrow' \\ +\downarrow & \verb'\downarrow' \\ +\Downarrow & \verb'\Downarrow' \\ +\updownarrow & \verb'\updownarrow' \\ +\Updownarrow & \verb'\Updownarrow' \\ +\upuparrows & \verb'\upuparrows' \\ +\downdownarrows & \verb'\downdownarrows' \\ +\upharpoonright & \verb'\upharpoonright' \\ +\downharpoonright & \verb'\downharpoonright' \\ +\upharpoonleft & \verb'\upharpoonleft' \\ +\downharpoonleft & \verb'\downharpoonleft' \\ +\end{symbols} + +\subsubsection{Miscellaneous} +\begin{symbols}[0.9] +\nearrow & \verb'\nearrow' \\ +\searrow & \verb'\searrow' \\ +\swarrow & \verb'\swarrow' \\ +\nwarrow & \verb'\nwarrow' \\ +\circlearrowright & \verb'\circlearrowright' \\ +\circlearrowleft & \verb'\circlearrowleft' \\ +\Lsh & \verb'\Lsh' \\ +\Rsh & \verb'\Rsh' \\ +\looparrowleft & \verb'\looparrowleft' \\ +\looparrowright & \verb'\looparrowright' \\ +\curvearrowleft & \verb'\curvearrowleft' \\ +\curvearrowright & \verb'\curvearrowright' \\ +\end{symbols} +\pagebreak[4] + +\subsection{Relations} +\begin{symbols}[0.8] +\ll & \verb'\ll' \\ +\gg & \verb'\gg' \\ +\llless & \verb'\lll \llless' \\ +\gggtr & \verb'\ggg \gggtr' \\ +\sqsubset & \verb'\sqsubset' \\ +\sqsupset & \verb'\sqsupset' \\ +\sqsubseteq & \verb'\sqsubseteq' \\ +\sqsupseteq & \verb'\sqsupseteq' \\ +\owns & \verb'\owns' \\ +\vdash & \verb'\vdash' \\ +\Vdash & \verb'\Vdash' \\ +\vDash & \verb'\vDash' \\ +\dashv & \verb'\dashv' \\ +\Vvdash & \verb'\Vvdash' \\ +\models & \verb'\models' \\ +\nvdash & \verb'\nvdash' \\ +\nVdash & \verb'\nVdash' \\ +\nvDash & \verb'\nvDash' \\ +\nVDash & \verb'\nVDash' \\ +\perp & \verb'\perp' \\ +\sim & \verb'\sim' \\ +\simeq & \verb'\simeq' \\ +\eqsim & \verb'\eqsim' \\ +\backsim & \verb'\backsim' \\ +\backsimeq & \verb'\backsimeq' \\ +\thicksim & \verb'\thicksim' \\ +\nsim & \verb'\nsim' \\ +\approx & \verb'\approx' \\ +\napprox & \verb'\napprox' \\ +\thickapprox & \verb'\thickapprox' \\ +\approxeq & \verb'\approxeq' \\ +\asymp & \verb'\asymp' \\ +\cong & \verb'\cong' \\ +\ncong & \verb'\ncong' \\ +\doteq & \verb'\doteq' \\ +\doteqdot & \verb'\Doteq \doteqdot' \\ +\risingdotseq & \verb'\risingdotseq' \\ +\fallingdotseq & \verb'\fallingdotseq' \\ +\lessdot & \verb'\lessdot' \\ +\gtrdot & \verb'\gtrdot' \\ +\eqcirc & \verb'\eqcirc' \\ +\circeq & \verb'\circeq' \\ +\bumpeq & \verb'\bumpeq' \\ +\Bumpeq & \verb'\Bumpeq' \\ +\triangleq & \verb'\triangleq' \\ +\multimap & \verb'\multimap' \\ +\propto & \verb'\propto' \\ +\varpropto & \verb'\varpropto' \\ +\lesssim & \verb'\lesssim' \\ +\gtrsim & \verb'\gtrsim' \\ +\lessapprox & \verb'\lessapprox' \\ +\gtrapprox & \verb'\gtrapprox' \\ +\xprec & \verb'\xprec' \\ +\xsucc & \verb'\xsucc' \\ +\preceq & \verb'\preceq' \\ +\succeq & \verb'\succeq' \\ +\precsim & \verb'\precsim' \\ +\succsim & \verb'\succsim' \\ +\precapprox & \verb'\precapprox' \\ +\succapprox & \verb'\succapprox' \\ +\eqslantless & \verb'\eqslantless' \\ +\eqslantgtr & \verb'\eqslantgtr' \\ +\curlyeqprec & \verb'\curlyeqprec' \\ +\curlyeqsucc & \verb'\curlyeqsucc' \\ +\preccurlyeq & \verb'\preccurlyeq' \\ +\succcurlyeq & \verb'\succcurlyeq' \\ +\leqq & \verb'\leqq' \\ +\geqq & \verb'\geqq' \\ +\leqslant & \verb'\leqslant' \\ +\geqslant & \verb'\geqslant' \\ +\lessgtr & \verb'\lessgtr' \\ +\gtrless & \verb'\gtrless' \\ +\lesseqgtr & \verb'\lesseqgtr' \\ +\Also +\gtreqless & \verb'\gtreqless' \\ +\Also +\lesseqqgtr & \verb'\lesseqqgtr' \\ +\Also +\gtreqqless & \verb'\gtreqqless' \\ +\also +\lvertneqq & \verb'\lvertneqq' \\ +\gvertneqq & \verb'\gvertneqq' \\ +\nleq & \verb'\nleq' \\ +\ngeq & \verb'\ngeq' \\ +\nless & \verb'\nless' \\ +\ngtr & \verb'\ngtr' \\ +\nprec & \verb'\nprec' \\ +\nsucc & \verb'\nsucc' \\ +\lneqq & \verb'\lneqq' \\ +\gneqq & \verb'\gneqq' \\ +\nleqslant & \verb'\nleqslant' \\ +\ngeqslant & \verb'\ngeqslant' \\ +\lneq & \verb'\lneq' \\ +\gneq & \verb'\gneq' \\ +\npreceq & \verb'\npreceq' \\ +\nsucceq & \verb'\nsucceq' \\ +\precnsim & \verb'\precnsim' \\ +\succnsim & \verb'\succnsim' \\ +\lnsim & \verb'\lnsim' \\ +\gnsim & \verb'\gnsim' \\ +\nleqq & \verb'\nleqq' \\ +\ngeqq & \verb'\ngeqq' \\ +\precneqq & \verb'\precneqq' \\ +\succneqq & \verb'\succneqq' \\ +\precnapprox & \verb'\precnapprox' \\ +\succnapprox & \verb'\succnapprox' \\ +\lnapprox & \verb'\lnapprox' \\ +\gnapprox & \verb'\gnapprox' \\ +\Subset & \verb'\Subset' \\ +\Supset & \verb'\Supset' \\ +\subseteqq & \verb'\subseteqq' \\ +\supseteqq & \verb'\supseteqq' \\ +%\varsubsetneq & \verb'\varsubsetneq' \\ +%\varsupsetneq & \verb'\varsupsetneq' \\ +\nsubseteqq & \verb'\nsubseteqq' \\ +\also +\nsupseteqq & \verb'\nsupseteqq' \\ +\also +\subsetneqq & \verb'\subsetneqq' \\ +\also +\supsetneqq & \verb'\supsetneqq' \\ +%\varsubsetneqq & \verb'\varsubsetneqq' \\ +%\varsupsetneqq & \verb'\varsupsetneqq' \\ +\subsetneq & \verb'\subsetneq' \\ +\supsetneq & \verb'\supsetneq' \\ +\nsubseteq & \verb'\nsubseteq' \\ +\nsupseteq & \verb'\nsupseteq' \\ +\trianglerighteq & \verb'\trianglerighteq' \\ +\trianglelefteq & \verb'\trianglelefteq' \\ +\ntrianglerighteq & \verb'\ntrianglerighteq' \\ +\ntrianglelefteq & \verb'\ntrianglelefteq' \\ +\ntriangleleft & \verb'\ntriangleleft' \\ +\ntriangleright & \verb'\ntriangleright' \\ +\between & \verb'\between' \\ +| & \verb'| \vert \mid' \\ +\| & \verb'\| \Vert \parallel' \\ +\interleave & \verb'\interleave' \\ +\shortmid & \verb'\shortmid' \\ +\shortparallel & \verb'\shortparallel' \\ +\shortinterleave & \verb'\shortinterleave' \\ +\nparallel & \verb'\nparallel' \\ +\nmid & \verb'\nmid' \\ +\nshortmid & \verb'\nshortmid' \\ +\nshortparallel & \verb'\nshortparallel' \\ +\end{symbols} + +\subsection{Binary Operations} +\begin{symbols}[1.4] +\curlywedge & \verb'\curlywedge' \\ +\curlyvee & \verb'\curlyvee' \\ +\veebar & \verb'\veebar' \\ +\barwedge & \verb'\barwedge' \\ +\doublebarwedge & \verb'\doublebarwedge' \\ +\pm & \verb'\pm' \\ +\mp & \verb'\mp' \\ +\times & \verb'\times' \\ +\ltimes & \verb'\ltimes' \\ +\rtimes & \verb'\rtimes' \\ +\leftthreetimes & \verb'\leftthreetimes' \\ +\rightthreetimes & \verb'\rightthreetimes' \\ +\divideontimes & \verb'\divideontimes' \\ +\divides & \verb'\divides' \\ +\uplus & \verb'\uplus' \\ +\sqcap & \verb'\sqcap' \\ +\sqcup & \verb'\sqcup' \\ +\Cup & \verb'\Cup \doublecup' \\ +\Cap & \verb'\Cap \doublecap' \\ +\backslash & \verb'\backslash' \\ +\setminus & \verb'\setminus' \\ +\smallsetminus & \verb'\smallsetminus' \\ +\wr & \verb'\wr' \\ +\lhd & \verb'\lhd' \\ +\rhd & \verb'\rhd' \\ +\unlhd & \verb'\unlhd' \\ +\unrhd & \verb'\unrhd' \\ +\restriction & \verb'\restriction' \\ +\amalg & \verb'\amalg' \\ +\top & \verb'\top' \\ +\bot & \verb'\bot' \\ +\smallsmile & \verb'\smallsmile' \\ +\smallfrown & \verb'\smallfrown' \\ +\smile & \verb'\smile' \\ +\frown & \verb'\frown' \\ +\pitchfork & \verb'\pitchfork' \\ +\dotplus & \verb'\dotplus' \\ +\Join & \verb'\Join' \\ +\bowtie & \verb'\bowtie' \\ +\end{symbols} + +\subsection{Miscellaneous Symbols} +\begin{symbols} +\dagger & \verb'\dagger' \\ +\ddagger & \verb'\ddagger' \\ +\sectionsymbol & \verb'\sectionsymbol' \\ +\P & \verb'\P' \\ +\angle & \verb'\angle' \\ +\measuredangle & \verb'\measuredangle' \\ +\sphericalangle & \verb'\sphericalangle' \\ +\prime & \verb'\prime' \\ +\backprime & \verb'\backprime' \\ +\surd & \verb'\surd' \\ +\smallint & \verb'\smallint' \\ +\flat & \verb'\flat' \\ +\natural & \verb'\natural' \\ +\sharp & \verb'\sharp' \\ +\partial & \verb'\partial' \\ +\infty & \verb'\infty' \\ +\yen & \verb'\yen' \\ +\therefore & \verb'\therefore' \\ +\because & \verb'\because' \\ +\checkmark & \verb'\checkmark' \\ +\end{symbols} + +\subsection{Variable-sized Symbols} +These symbols come in two sizes which +do not vary with the point size of your +font. The big size can be obtained +by preceding the symbol command with +the command \verb'\displaystyle'. +\begin{symbols}[1.3] +\sum \displaystyle \sum & \verb'\sum' \\ +\product \displaystyle \product & \verb'\product' \\ +\coprod \displaystyle \coprod & \verb'\coprod' \\ +\integral \displaystyle \integral & \verb'\integral' \\ +\oint \displaystyle \oint & \verb'\oint' \\ +\bigcap \displaystyle \bigcap & \verb'\bigcap' \\ +\bigcup \displaystyle \bigcup & \verb'\bigcup' \\ +\bigsqcup \displaystyle \bigsqcup & \verb'\bigsqcup' \\ +\bigvee \displaystyle \bigvee & \verb'\bigvee' \\ +\bigwedge \displaystyle \bigwedge & \verb'\bigwedge' \\ +\bigodot \displaystyle \bigodot & \verb'\bigodot' \\ +\bigotimes \displaystyle \bigotimes & \verb'\bigotimes' \\ +\bigoplus \displaystyle \bigoplus & \verb'\bigoplus' \\ +\biguplus \displaystyle \biguplus & \verb'\biguplus' \\ +\end{symbols} + +\subsection{Delimiters} +\vspace*{-1ex} +These symbols can be made large to surround large formula. +E.g., $$\left\lfloor\displaystyle\sum_{i=1}^n x^i\right\rfloor$$ +was generated using + +\begin{verbatim} +\left\lfloor...\right\rfloor +\end{verbatim} +\vspace*{-2ex} +\begin{symbols}[0.8] +(~~~) & \verb'( )' \\ +\{~~~\} & \verb'\{ \}' \\ +\lfloor~~~\rfloor & \verb'\lfloor \rfloor' \\ +\lceil~~~\rceil & \verb'\lceil \rceil' \\ +\langle~~~\rangle & \verb'\langle \rangle' \\ +\ulcorner~~~\urcorner & \verb'\ulcorner \urcorner' \\ +\llcorner~~~\lrcorner & \verb'\llcorner \lrcorner' \\ +\uparrow & \verb'\uparrow' \\ +\downarrow & \verb'\downarrow' \\ +\updownarrow & \verb'\updownarrow' \\ +\Uparrow & \verb'\Uparrow' \\ +\Downarrow & \verb'\Downarrow' \\ +\Updownarrow & \verb'\Updownarrow' \\ +\end{symbols} + +\subsection{Math Accents} +\vspace*{-1ex} +\begin{symbols}[0.2] +\hat{a} & \verb'\hat{a}' \\ +\widehat{a} & \verb'\widehat{a}' \\ +\widehat{aa} & \verb'\widehat{aa}' \\ +\widehat{aaa} & \verb'\widehat{aaa}' \\ +\tilde{a} & \verb'\tilde{a}' \\ +\widetilde{a} & \verb'\widetilde{a}' \\ +\widetilde{aa} & \verb'\widetilde{aa}' \\ +\widetilde{aaa} & \verb'\widetilde{aaa}' \\ +\check{a} & \verb'\check{a}' \\ +\breve{a} & \verb'\breve{a}' \\ +\acute{a} & \verb'\acute{a}' \\ +\grave{a} & \verb'\grave{a}' \\ +\bar{a} & \verb'\bar{a}' \\ +\vec{a} & \verb'\vec{a}' \\ +\dotaccent{a} & \verb'\dotaccent{a}' \\ +\ddot{a} & \verb'\ddot{a}' \\ +\end{symbols} + +\subsection{Size Commands} +\vspace*{-1ex} +\begin{symbols} +\mu~\zsmall\mu~\zSmall\mu &\verb'\mu \zsmall\mu \zSmall\mu'\\ +\zbig\mu~\zBig\mu~\zBIG\mu &\verb'\zbig\mu \zBig\mu \zBIG\mu'\\ +\end{symbols} +\end{multicols} +\end{document} diff --git a/macros/latex/contrib/objectz/oztest.tex b/macros/latex/contrib/objectz/oztest.tex new file mode 100644 index 0000000000..fc8ea11c93 --- /dev/null +++ b/macros/latex/contrib/objectz/oztest.tex @@ -0,0 +1,206 @@ +\documentclass[11pt]{article} +\usepackage{oz} +\def\Out#1{#1 \!\!\rightarrow} +\def\In#1{\rightarrow\!\! #1} +\begin{document} + +Multi-letter identifiers have been changed to look +better than they do with vanilla \LaTeX: instead of +$\mathit{specifications}$, you get $specifications$. +The letters haven't been spread apart, and the +ligature $fi$ has been used. + +{\tt This is in typewriter font} + + +\begin{schema}{BirthdayBook} + known: \pset NAME \\ + birthday: NAME \pfun DATE +\ST + known = \dom birthday +\end{schema} + +\begin{axdef} +limit : \nat +\ST +limit \leq 65536 +\end{axdef} + +\begin{class}{Shape} +\also +colour : Colour \\ +\end{class} + +\begin{axdef} +perim : \real +\ST +perim > 0 +\end{axdef} + +\begin{axdef} +ini:State \cross Occ \cross T \fun Bool +\where +\forall S:State, i: Occ, t:T \dot ini(S,i,t) \iff \\ +\t1 \theta(\Out{S}, 1,0)\land\\ +\t2 \exi t_{1}:T \dot \theta(\In{S},i,t_{1}) \land +t_{1}\leq t \land \forall t_{2}:T \dot t_{2} < t \imp \neg \theta(\Out{S},i+1,t_{2} +)\\ +\t1 \lor \theta(\In{S}, 1,0)\land\\ +\t2 \exi t_{1}:T \dot \theta(\In{S},i,t_{1}) \land +t_{1}\leq t \land \forall t_{2}:T \dot t_{2} < t \imp \neg +\theta(\Out{S},i,t_{2}) +\end{axdef} + +Let us see if \verb|zbreak| works: +\typeout{*************************************} +\typeout{If you get large overfull vboxes now, Oz is not working} +\typeout{*************************************} + +\def \comm{\comment} + +\begin{schema}{MakePlan} + c? : Company \comm{The company that is making the plan}\\ + t? : Month \comm{Time period} \\ + \Xi NFMM \\ + \Xi AttrOfMarkets \comm{OpenMarkets} \\ + \Xi Cost \\ + \Xi AttrOfEconomy \comm{Buying and selling price of quota }\\ + \Xi AttrOfQuota \\ + \Xi AttrOfProduction \\ + \Xi FishingLimitations \\ + Plans! : Company \fun Plan \comm{The output is the plan for + the company} \\ +\zbreak +\where + \forall v: Vessel; f: Fishery; s: QuotaStock; p: Product; \\ +\t0 l: Landing; t: Month; i: Input @ \\ +\t0 \exists plan: Plan; Months: \power Month; \\ +\t0 vs : \power Vessel; fs: \power Fishery ; qs: \power QuotaStock; ls: \power Landing; \\ +\t0 ps : \power Product; \\ +\t0 catch: Vessel \cross Fishery \cross QuotaStock \pfun Tons; \\ +\t0 MAXnet\_profit:Kronur; fishing\_cost:Kronur; \\ + \t1 production\_earnings:Kronur; \\ + \t1 production\_cost:Kronur; quota\_trading\_profit:Kronur; \\ +\t0 fishing\_days: Vessel \cross Fishery \cross Month \pfun \nat; \\ +\t0 value\_landing: Vessel \fun Kronur; \\ +\t0 export: Vessel \cross Landing \cross Month \pfun Tons; \\ + \t1 trade\_in, trade\_out: Landing \cross Month \pfun Tons; \\ + \t1 prod: Product \cross Month \fun Tons; \\ +\t0 quota\_rent\_in, quota\_rent\_out, quota\_next\_to, \\ + \t1 quota\_next\_from, quota\_exch\_to, quota\_exch\_from,\\ + \t1 quota\_trans\_from, quota\_trans\_to: Vessel \cross QuotaStock \pfun Tons; \\ +\t0 ExchangeCharge: \num; \comm{charge for changing one species into another} \\ +\t0 quota\_used: Vessel \cross QuotaStock \pfun Tons @ \\ +\zbreak + \t0 Plans! = Plans! \oplus \{c? \mapsto plan \} \land \\ + \t0 Months = t? \upto 12 \land \\ + \t0 i \in Inputs \land \\ + \t0 vs = Vessels ~ c? \land v \in vs \land\\ + \t0 fs = \{f: Fishery | f \in \\ + \t1 (\bigcup \{ v: Vessel | v \in vs @ Fisheries(v) \}) @ f \} \land f \in fs \land \\ + \t0 qs = \{s: QuotaStock; f: Fishery | \\ + \t1 f \in fs \land s \in QuotaStocks (f) @ s \} \land s \in qs \land \\ + \t0 ls = \{s: QuotaStock; f: Fishery | f \in fs \land s \in qs @ \\ + \t1 Landings~(f,s) \} \land l \in ls \land \\ + \t0 ps = \{p: Product | \\ + \t1 p \in \bigcup \{ fa: Factory | fa \in Factories~c? @ Products(fa) \} @ p \} \land \\ + \t0 p \in ps \land \\ +\comm{The overall goal is to maximize net profits} \\ + \t0 MAXnet\_profit = -fishing\_cost+production\_earnings + \\ + \t1 -production\_cost + quota\_trading\_profit \land \comm{A.1}\\ + \t0 catch ~(v,f,s) = ExpCatch~(v,f,s)* \comm{A.4}\\ + \t1 \sum_{t: Month | t \in Months} fishing\_days~(v,f,t) \land \\ +\comm{One of the prices LandingPrice or ExportPrice is always zero for any l} \\ + \t0 (\forall l | l \in ls @ LandingPrice (l) = 0 \lor ExportPrice(l) = 0 \land \\ + \t1 LandingPrice(l) \neq ExportPrice(l) ) \land \\ + \t0 value\_landing= \comm{A.3} \\ + \t1 \{v: Vessel | v \in vs @ v \mapsto \\ + \t1 \sum_{ l: Landing | l \in ls} LandingPrice (l)* ExportPriceConst(l) * \\ + \t1 \sum_{f: Fishery | f \in fs} \sum_{s: QuotaStock | s \in qs} (SpeciesToLandings~(s,f,l) *(catch~(v,f,s)) \}\land \\ + \t0 fishing\_cost = \sum_{v: Vessel | v \in vs} Share (v)*value\_landing(v) + \comm{A.2}\\ + \t1 \sum_{ f: Fishery | f \in fs} CostFishDay ~ (v, f) * \\ + \t1 \sum_{t: Month | t \in Months} fishing\_days~(v,f,t) \land \\ +\zbreak + \t0 production\_earnings = \comm{A.5}\\ + \t1 \sum_{l: Landing | l \in ls} \sum_{ t: Month | t \in Months} \\ + \t3 (ExportPrice~(l,t))*(1-0.002)*t)* \\ + \t3 \sum_{v: Vessel | v \in vs} export~(v,l,t) \\ + \t1 -WetfishBuyingPrice(l) * (1-0.002)*t)*trade\_in~(l,t) \\ + \t1 +WetfishSellingPrice(l) * (1-0.002)*t)*trade\_out~(l,t) \\ + \t1 +\sum_{p: Product | p \in ps} ProductPrice~(p,t) *(1-0.002)*t)* \\ + \t1 \sum_{t:Month | t \in Months} prod~ (p,t) \land \\ + \t0 production\_cost = \sum_{i: Input | i \in Inputs} InputCost(i)* \comm{A.6}\\ + \t1 \sum_{p: Product | p \in ps} InputForProduct(p,i) * \\ + \t1 \sum_{ t: Month | t \in Months} prod(p,t) \land \\ + \t0 ExchangeCharge = 0.005*NextPrice(s) \land \\ + \t0 quota\_trading\_profit = -(\sum_{s: QuotaStock | s \in qs } QuotaRentInPrice(s) * \\ + \t1 \sum_{v: Vessel | v \in vs } quota\_rent\_in~(v,s) ) \comm{A.7}\\ + \t1 + \sum_{s: QuotaStock | s \in qs } QuotaRentOutPrice(s)* \\ + \t1 \sum_{v: Vessel | v \in vs } quota\_rent\_out~(v,s) \\ + \t1 + \sum_{s: QuotaStock | s \in qs } NextCharge *NextPrice(s)*(1-InterestRate)* \\ + \t1 \sum_{v: Vessel | v \in vs } quota\_next\_to~(v,s) \\ + \t1 + \sum_{s: QuotaStock | s \in qs } NextPrice(s)*(1-InterestRate) * \\ + \t1 \sum_{v: Vessel | v \in vs } quota\_next\_from~(v,s) \\ + \t1 -ExchangeCharge*\sum_{v: Vessel | v \in vs }\sum_{s: QuotaStock | s \in qs } quota\_exch\_to(v,s) \\ + \t1 -TransferCharge*\sum_{v: Vessel | v \in vs }\sum_{s: QuotaStock | s \in qs } quota\_trans\_to~(v,s) \land \\ + \t0 \sum_{ f: Fishery | f \in fs } fishing\_days~(v,f,t) \leq MaxTotFishingDays ~(v,t) \land \comm{A.9}\\ +\comm{A.6.1 Constraints on fishing time } \\ + \t0 l \in ExportLandings \implies \\ + \t1 \sum_{f: Fishery | f \in fs } \sum_{s: QuotaStock | s \in qs } \comm{A.10} \\ + \t2 SpeciesToLandings~(s,f,l) * ExpCatch (v,f,s)*fishing\_days(v,f,t) = \\ + \t3 export~(v,l,t) \land \\ +\comm{A.6.2 Processing and selling the catch } \\ + \t0 l \notin ExportLandings \implies \\ + \t1 \sum_{v: Vessel | v \in vs } \sum_{f: Fishery | f \in fs } \sum_{s: QuotaStock | s \in qs } \\ + \t2 SpeciesToLandings~(s,f,l)*ExpCatch~(v,f,s)*fishing\_days~(v,f,t) \\ + \t1 = (1 / LandingsToProducts~(p,l)) * prod~(p,t) - trade\_in~(l,t) + trade\_out(l,t) \land \comm{A.11}\\ +\zbreak + \t0 \sum_{t: Month | t \in Months } \sum_{p:Product | p \in ps }InputForProduct(p,i)*prod(p,t) \\ + \t1 \leq \sum_{i : Input | i \in Inputs } MaxInput~(i,t) \land \comm{A.13}\\ + \t0 \sum_{t: Month | t \in Months } \sum_{p: Product | p \in ps } InputForProduct(p,i)*prod~(p,t) \\ + \t1 \geq \sum_{i: Input | i \in Inputs } MinInput~(i,t) \land \comm{A.14}\\ + \t0 \sum_{t: Month | t \in Months } export~(v,l,t) \leq MaxExport~(v,l) \land \comm{A.15}\\ +\comm{A.6.3 Constraints because of quota restrictions } \\ + \t0 quota\_used = \comm{A.17} \\ + \t1 \{ v:Vessel; s: QuotaStock | v \in vs \land s \in qs @ \\ + \t2 (v,s) \mapsto \sum_{f: Fishery | f \in fs } (1+QuotaSurcharge~(s,f))* \\ + \t2 catch~(v,f,s) \} \land \\ + \t0 \sum_{v: Vessel | v \in vs } quota\_trans\_to(v,s)- quota\_trans\_from(v,s) =0 \land \comm{A.18} \\ + \t0 quota\_used(v,s) - quota\_rent\_in(v,s) + quota\_rent\_out(v,s) - \comm{A.16} \\ + \t1 quota\_exch\_to(v,s) + quota\_exch\_from(v,s) - \\ + \t1 quota\_trans\_to(v,s) + quota\_trans\_from(v,s) - \\ + \t1 quota\_next\_to~(v,s) + quota\_next\_from~(v,s) \leq QuotaLeft~(v,s) \land \\ + \t0 s = Cod \implies MaxQuotaInto(v,s) = 0 \land \comm{A.19}\\ + \t0 s \neq Cod \implies MaxQuotaInto(v,s) = 0.05*QuotaAllocated(v,s) \land \\ + \t1 QuotaValueInto(s)*quota\_exch\_to(v,s) \leq \\ + \t2 \sum_{s: QuotaStock | s \in qs } MaxQuotaInto~(v,s) \land \\ + \t0 \sum_{s: QuotaStock | s \in qs } QuotaValueInto (s)*quota\_exch\_to~(v,s) - \comm{A.20}\\ + \t1 \sum_{s: QuotaStock | s \in qs } QuotaValueFrom(s)* quota\_exch\_from~(v,s) = 0 \land \\ + \t0 quota\_next\_from(v,s) \leq (QuotaOver(v,s) / 100)*QuotaAllocated(v,s) \land \comm{A.21}\\ + \t0 quota\_next\_to~(v,s) \leq (QuotaUnder(v,s) / 100)*QuotaAllocated(v,s) \land \comm{A.22} \\ +\zbreak +\comm{Bounds} \\ + \t0 fishing\_days~(v,f,t) \leq MaxFishingDays~(f,t) \land \comm{A.23}\\ + \t0 QuotaAllocated~(v,s) = 0 \implies \\ + \t1 (quota\_exch\_to~(v,s) = 0 \land \comm{A.24}\\ + \t1 quota\_rent\_in~(v,s) = 0 \land \comm{A.25}\\ + \t1 quota\_trans\_to~(v,s) = 0) \land \comm{A.26} \\ + \t0 QuotaValueInto~s = 0 \implies quota\_exch\_to~(v,s) = 0 \land \comm{A.27}\\ + \t0 QuotaValueFrom~s = 0 \implies quota\_exch\_from~(v,s) = 0 \comm{A.28}\\ +\zbreak + \t0 plan.c = c? \ + \t0 plan.fishing\_days = fishing\_days \land + \t0 plan.quota\_rent\_out = quota\_rent\_out \land \\ + \t0 plan.quota\_rent\_in = quota\_rent\_in \land \\ + \t0 plan.quota\_trans\_from = quota\_trans\_from \land \\ + \t0 plan.quota\_trans\_to = quota\_trans\_to \land \\ + \t0 plan.quota\_next\_from = quota\_next\_from \land \\ + \t0 plan.quota\_next\_to = quota\_next\_to \land \\ + \t0 plan.quota\_exch\_from = quota\_exch\_from \land \\ + \t0 plan.quota\_exch\_to = quota\_exch\_to \land \\ + \t0 plan.trade\_out = trade\_out \land \\ + \t0 plan.trade\_in = trade\_in \land \\ + \t0 plan.prod = prod \land \\ + \t0 plan.export = export \\ +\end{schema} +\end{document} diff --git a/macros/latex/contrib/objectz/readme b/macros/latex/contrib/objectz/readme new file mode 100644 index 0000000000..c3ee8cd92f --- /dev/null +++ b/macros/latex/contrib/objectz/readme @@ -0,0 +1,45 @@ +This is a revision of Paul King's oz.sty macros for typesetting Object Z, +updated for LaTeX2e. Users should run ozguide.tex through \LaTeX\ (after +installation!) for details of usage. + +Install by running \TeX\ on oz.ins and install oz.sty where \LaTeX\ +can find it. + +UPDATE NOVEMBER 1996 +******************** + +The Formal Methods Group in the Computer Science Department at the +University of Queensland recently released 'wizard', a type checker +for Object-Z specifications. Included in the wizard release was an +updated version of the oz.sty file for LaTeX 2.09. + +I have implemented all changes made in the oz.sty for LaTeX 2.09, +since it's last official release in late 1990, into the oz.dtx file +which you maintain for LaTeX 2e. I have attached my updated version +of oz.dtx to this message so that you may check these modifications +and officially release the updated version. + +The changes were made to the oz.dtx file with last changes logged +on 22 Feb 95 (this is the version currently available from CTAN). +All modifications and additions I have made are clearly indicated in +the updated file for your convenience. + +Should you need to compare my changes with the updated oz.sty file for +LaTeX 2.09, you can download the wizard archive from the following url: + + ftp://ftp.cs.uq.edu.au/pub/SVRC/software/wizard.tar.gz + +The new oz.sty file and oz.tex file are located in the wizard/tex +subdirectory when the archive is extracted. + +Please contact me if you need to. + +Thanks. + +Dave. +-- +David Leadbetter Email: davidl@cs.uq.edu.au +PhD Student Phone: + 61 7 3365 1204 +Department of Computer Science FAX: + 61 7 3365 1999 +The University Of Queensland 4072 AUSTRALIA + -- cgit v1.2.3