% \documentstyle[12pt,fleqn,espcrc1,alltt]{article} % \documentstyle[fleqn,wicsbook,alltt,fuzz]{article} % \documentstyle[fleqn,wicsbook,alltt,zed]{article} \documentstyle[fleqn,wicsbook,zed]{article} % Last updated by Jonathan Bowen, 18 November 1993. %%% Mike: please check lines starting with "%%%" \title{\vspace{-3pc}\titlesize\bf Z and HOL} \author{\footnotesize % \hspace{-2mm} \begin{tabular}[t]{@{}l} {\large Jonathan Bowen} \\[1ex] Oxford University\\ Computing Laboratory \\ %Programming Research Group \\ Wolfson Building \\ Parks Road \\ Oxford OX1 3QD \\ UK \\[1ex] \footnotesize Email: \verb"Jonathan.Bowen@comlab.ox.ac.uk" \end{tabular} % \hspace{-2mm} \begin{tabular}[t]{l@{}} {\large Mike Gordon} \\[1ex] University of Cambridge \\ Computer Laboratory \\ New Museums Site \\ Pembroke Street \\ Cambridge CB2 3QG \\ UK \\[1ex] \footnotesize Email: \verb"Mike.Gordon@cl.cam.ac.uk" \end{tabular} \date{} } % Definitions \def\Z{{Z}} \def\W{${\cal W}$} \def\zedB{{\it zed}{\bf B}} \def\HOL{{\rm\small HOL}} \def\LCF{{\rm\small LCF}} \def\ML{{\rm\small ML}} \def\fuzz{{\large\it f\kern0.1em}{\normalsize\sc uzz}} % --------------------------------------------------------------------- % Macros for little HOL sessions displayed in boxes. % % Usage: (1) \setcounter{sessioncount}{1} resets the session counter % % (2) \begin{session}\begin{verbatim} % . % < lines from hol session > % . % \end{verbatim}\end{session} % % typesets the session in a numbered box. % --------------------------------------------------------------------- \newlength{\hsbw} \setlength{\hsbw}{\textwidth} \addtolength{\hsbw}{-\arrayrulewidth} \addtolength{\hsbw}{-\tabcolsep} \newcommand\HOLSpacing{9pt} \newcounter{sessioncount} \setcounter{sessioncount}{1} \newenvironment{session}{\begin{flushleft} \vskip-1.5mm \begin{tabular}{@{}|c@{}|@{}}\hline \begin{minipage}[b]{\hsbw} \vspace*{-.5pt} \begin{flushright} \rule{0.01in}{.15in}\rule{0.3in}{0.01in}\hspace{-0.35in} \raisebox{0.04in}{\makebox[0.3in][c]{\small \thesessioncount}} \end{flushright} \vspace*{-.55in} % Change the following from \small to make fit WICS style if necessary \begingroup\small\baselineskip\HOLSpacing}{\endgroup\end{minipage}\\ \hline \end{tabular} \vskip-1.5mm \end{flushleft} \stepcounter{sessioncount} } % ALLTT DOCUMENT-STYLE OPTION % ` changed to be non-active \makeatletter \def\docspecials{\do\ \do\$\do\&% \do\#\do\^\do\^^K\do\_\do\^^A\do\%\do\~} \def\alltt{\trivlist \item[]\if@minipage\else\vskip\parskip\fi \leftskip\@totalleftmargin\rightskip\z@ \parindent\z@\parfillskip\@flushglue\parskip\z@ \@tempswafalse \def\par{\if@tempswa\hbox{}\fi\@tempswatrue\@@par} \obeylines \tt % \catcode``=13 % \@noligs \let\do\@makeother \docspecials \frenchspacing\@vobeyspaces} \let\endalltt=\endtrivlist \makeatother \begin{document} \maketitle \thispagestyle{empty} % \tableofcontents %%% New abstract - check you are happy with it. %%% Tweaked by MJCG \begin{abstract} \noindent \noindent A simple `shallow' semantic embedding of the \Z\ notation into the \HOL\ logic is described. The \Z\ notation is based on set theory and first order predicate logic. The \HOL\ theorem proving system supports higher order logic. A well-known case study is used as a running example. The presentation is intended to show people with some knowledge of \Z\ how a tool such as \HOL\ can be used to provide mechanical support for the notation, including mechanization of proofs. No specialized knowledge of \HOL\ is assumed. \end{abstract} \section{Introduction} \HOL\ \cite{HOL} is an `\LCF-style' theorem proving environment \cite{EdinLCF,CamLCF} for classical higher order logic \cite{Andrews,Church}. Proof tools for the formal specification notation \Z\ \cite{Z:Brie92,Z:Spiv92} can be implemented by translating \Z\ schemas into higher order logic and then programming schema combining operations in \HOL's metalanguage \ML.\footnote{The ML language was originally developed as part of LCF, but is now an independent programming language in its own right \cite{StandardML}. It is an eager-evaluation impure functional language with a polymorphic type discipline.} This technique is known as {\it semantic embedding\/} (see section~\ref{embed}) and has been pioneered by ICL for many years. They have built their own `industrial strength' version of \HOL, called ProofPower \cite{ProofPower}, and implemented sophisticated proof tools for \Z\ on top of it (see section~\ref{other} for more on ProofPower and other proof tools for \Z). This paper is intended to be an accessible introduction to support for \Z\ by semantic embedding. It is intended for readers familiar with \Z, but not with \HOL. The techniques described here use ordinary \HOL\ and are simpler and less powerful than those found in ProofPower. In the next section a familiar Z specification example, Spivey's `birthday book', is used to illustrate how \HOL\ can support \Z. Subsequent sections discuss how this support is achieved. \section{The Birthday Book}\label{birthdaybook} It is assumed that readers are reasonably familiar with the birthday book example in Chapter~1 of Spivey's {\it The \Z\ Notation: A Reference Manual\/} \cite{Z:Spiv92} (also to be found in \cite{Z:Spiv89b}), henceforth called ZRM. The schemas from this specification are included here for comparison with their \HOL\ equivalents. The numbered boxes that follow show a \HOL\ session in which the birthday book is input and some simple facts are proved. The \HOL\ system prompts for input with {\verb"#"}, so all lines beginning with this symbol are supplied by the user. All other lines are generated by \HOL{}. The sessions have been edited to remove some output and to suppress details of some user-supplied theorem proving tactics, which will only be comprehensible to readers familiar with \HOL.\footnote{The complete input to HOL for the Birthday Book and other examples is available in the directory {\verb+contrib/Examples+} distributed with HOL88, Version 2.02. Details of HOL (including how to get it) are available from an on-line networked hypertext documentation service run by the Laboratory for Applied Logic at Brigham Young University. To browse this documentation, first obtain the XMosaic tool (connect to {\verb+ftp.ncsa.uiuc.edu+} by anonymous FTP, then the directory {\verb+/Mosaic/xmosaic-binaries+} contains compiled copies of the latest version of XMosaic for a variety of architectures). To connect to the HOL documentation server select {\tt OPEN} from the XMosaic menu and enter {\verb+http://lal.cs.byu.edu/lal/hol-documentation.html+}.} Before the session starts \HOL{} is run and the \Z{} support package loaded. This package is a collection of \ML{} declarations together with a theory {\verb+Z+} containing definitions to support \Z\ operators and its `Mathematical Tool-kit' (see section~\ref{zops}). Details of this loading are omitted here. The first interaction of the session is shown in box~1 below. A new theory called {\verb"BirthdayBook"} is started. Theories contain definitions and theorems that the user has proved. They are stored in a hierarchical database on disk. The \ML\ command {\verb"new_theory"} starts a new theory with a user-supplied name. \begin{session}\begin{verbatim} #new_theory `BirthdayBook`;; \end{verbatim}\end{session} This interaction initiates the specification of the Birthday Book by starting a new \HOL\ theory called {\verb"BirthdayBook"}. Note that in the version of \ML\ (Classic~\ML) provided by \HOL 88 (which is the version of \HOL{} used here) user input is terminated with {\verb+;;+} (in Standard \ML\ the terminator is a single semi-colon). The first definition in this theory introduces two sets: \begin{zed} [~ NAME, DATE ~] \end{zed} \noindent The corresponding declaration in \HOL\ uses an \ML\ function {\verb"sets"}. \begin{session}\begin{verbatim} #sets `NAME DATE`;; \end{verbatim}\end{session} With this second interaction the two sets {\tt NAME} and {\tt DATE} are declared. The first schema in the Birthday Book defines the abstract state and an `invariant' on that state: \begin{schema}{BirthdayBook} known : \power NAME \\ birthday : NAME \pfun DATE \where known = \dom birthday \end{schema} \noindent The declaration of schemas in \HOL\ uses a notation that is intended to make it clear what the corresponding \Z\ is. This is shown in box~3 below. \begin{session}\begin{verbatim} #declare # `BirthdayBook` # "SCHEMA # [known :: (P NAME); # birthday :: (NAME -+> DATE)] # %---------------------------% # [known = dom birthday]";; \end{verbatim}\end{session} This third interaction illustrates the format (shown on lines starting with {\verb"#"}) used to input \Z{} schemas to \HOL. A preprocessor converts the input format to a \HOL\ term that represents the semantics of the corresponding schema. This preprocessor could in principle be a complete parser for \Z\ notation,\footnote{HOL libraries provide syntax processing utilities that enable custom parsers and pretty-printers to be generated.} but in keeping with our `lightweight' approach this has not been done (ICL's ProofPower tool supports proper \Z\ syntax). The aim has been to have an input format that is readable as both \Z\ and \HOL. The powerset operator {\tt P} and infix partial function operator {\verb"-+>"} are defined in the theory {\tt Z}, which implements (part of) the \Z\ mathematical tool-kit; see section~\ref{zops} for more details. The \ML\ function {\verb"declare"} converts the term {\verb+"SCHEMA+}$~\cdots${\verb+"+} that follows it into the \HOL\ representation of the schema, remembers the declaration (and the types of declared variables) in a global data structure and returns the schema representation. The \HOL\ representation of a schema of the form: %%unchecked \begin{schema}{~\ldots~} x_1 \hspace{1mm} : S_1 \\ x_2 \hspace{1mm} : S_2 \\ \hspace{5.2mm}\vdots\\ x_m : S_m \where P_1\\ P_2\\ \hspace{1mm}\vdots\\ P_n \end{schema} \noindent is semantically equivalent to the formula: \[ x_1 \in S_1 \wedge x_2 \in S_2 \wedge \ldots \wedge x_m \in S_m \wedge P_1 \wedge P_2 \wedge \ldots \wedge P_n \] \noindent which in \HOL\ notation is written as: \begin{alltt} \(x\sb{1}\) IN \(S\sb{1}\) \verb"/\" \(x\sb{2}\) IN \(S\sb{2}\) \verb"/\" \(\ldots\) \verb"/\" \(x\sb{m}\) IN \(S\sb{m}\) \verb"/\" \(P\sb{1}\) \verb"/\" \(P\sb{2}\) \verb"/\" \(\ldots\) \verb"/\" \(P\sb{n}\) \end{alltt} \noindent where $S_i$ is a \HOL\ term denoting a set and $P_1, \ldots, P_n$ are Boolean terms constituting the schema's predicate. The infix operators {\verb"IN"} and {\verb"::"} both denote the set membership relation. The former is used for general set membership in predicates (e.g.~to represent $\in$), the latter for type membership assertions (e.g.~in the declaration part of schemas, where \Z\ would have a colon). Note that schema operations can move type membership assertions from the declaration part of schemas into the predicate part, thus automatically generated assertions of the form $x{\verb+::+}S$ may appear in the predicate parts of schemas. The actual semantic representation is not the conjunction shown above, but the logically equivalent term: \begin{alltt} SCHEMA [\(x\sb{1}\) :: \(S\sb{1}\); \(x\sb{2}\) :: \(S\sb{2}\); \(\ldots\) ;\(x\sb{m}\) :: \(S\sb{m}\)] [\(P\sb{1}\); \(P\sb{2}\); \(\ldots\) ; \(P\sb{n}\)] \end{alltt} \noindent where {\tt SCHEMA} is defined (in the theory {\tt Z}) by: \begin{alltt} SCHEMA [\(d\sb{1}\); \(\ldots\) ;\(d\sb{m}\)] [\(P\sb{1}\); \(\ldots\) ;\(P\sb{n}\)] = \(d\sb{1}\) \verb"/\" \(\ldots\) \verb"/\" \(d\sb{m}\) \verb"/\" \(P\sb{1}\) \verb"/\" \(\ldots\) \verb"/\" \(P\sb{n}\) \end{alltt} \noindent This representation is more convenient as the conjuncts corresponding to the declaration and predicate parts of the schema can be easily extracted. \HOL\ input will usually be laid out in the following `\Z-style' format: \begin{alltt} SCHEMA [\(x\sb{1}\) \hspace{1.3mm}:: \(S\sb{1}\); \(x\sb{2}\) \hspace{1.3mm}:: \(S\sb{2}\); \(\vdots\) \(x\sb{m}\) :: \(S\sb{m}\)] %---------% [\(P\sb{1}\); \(P\sb{2}\); \hspace{1mm} \(\vdots\) \(P\sb{n}\)] \end{alltt} \noindent where the line {\verb"%--"}$\cdots${\verb"--%"} is just a comment to aid the eye (comments in \ML\ are enclosed between percent symbols). The next schema illustrates schema inclusion and the $\Delta$ change of state schema convention. First the \Z: \begin{schema}{AddBirthday} \Delta BirthdayBook \\ name? : NAME \\ date? : DATE \where name? \notin known \also birthday' = birthday \cup \{name? \mapsto date?\} \end{schema} \noindent The corresponding \HOL\ is: \begin{session}\begin{verbatim} #declare # `AddBirthday` # "SCHEMA # [DELTA BirthdayBook; # name? :: NAME; # date? :: DATE] # %--------------------------------------------% # [~(name? IN known); # birthday' = birthday UNION {name? |-> date?}]";; \end{verbatim}\end{session} The symbol {\verb"~"} represents negation ($\neg$) in \HOL. Normally schemas are printed out as their name, but this default can be changed so that the semantic representations of schemas are printed in full. This mode is entered by evaluating the \ML\ expression {\verb"show_schemas true"}. \begin{session}\begin{verbatim} #"BirthdayBook";; "BirthdayBook" : term #show_schemas true;; #"BirthdayBook";; "SCHEMA [known :: (P NAME); birthday :: (NAME -+> DATE)] [known = dom birthday]" : term #"AddBirthday";; "SCHEMA [known :: (P NAME); birthday :: (NAME -+> DATE); known' :: (P NAME); birthday' :: (NAME -+> DATE); name? :: NAME;date? :: DATE] [known = dom birthday; known' = dom birthday'; ~name? IN known; birthday' = birthday UNION {name? |-> date?}]" \end{verbatim}\end{session} Note how the schema inclusion {\tt DELTA~BirthdayBook} (which represents \Z's $\Delta BirthdayBook$) results in extra primed variables being added to the declaration of {\tt AddBirthday}, and appropriate instances of the predicate part of {\tt BirthdayBook} being included in the predicate of {\tt AddBirthday}. More details of how {\tt DELTA}-expansion is implemented can be found in section~\ref{io}. As a check, the precondition of {\tt AddBirthday} can be computed and simplified using a theorem proving tool called {\tt simp}. The precondition of an operation schema is the condition on the state that must hold if the operation is to be applicable. See page 77 of \cite{Z:Spiv92}, page 151 of \cite{Z:Pott90} and page 141 of \cite{Z:Dill90} for further discussions of this. For example, here is the computation of the precondition of $AddBirthday$: \begin{session}\begin{verbatim} #show_schemas false;; #simp "pre AddBirthday";; known :: (P NAME), birthday :: (NAME -+> DATE), name? :: NAME, date? :: DATE, (dom(birthday UNION {name? |-> date?})) :: (P NAME), (birthday UNION {name? |-> date?}) :: (NAME -+> DATE) |- pre AddBirthday = (known = dom birthday) /\ ~name? IN (dom birthday) \end{verbatim}\end{session} \noindent The evaluation of {\verb+simp "pre AddBirthday"+} results in a theorem asserting that the precondition of $AddBirthday$ is $known = \dom birthday \land name? \notin \dom birthday$. Theorems are a special datatype in \ML, values of which can only be created by applying sequences of inference rules to axioms (or previously proved theorems) \cite{EdinLCF,HOL}. A theorem $t_1${\verb","}$\ldots${\verb","}$t_n${\verb" |- "}$t$ asserts that the term $t$ follows from the conjunction of the terms $t_1$, $\ldots$ , $t_n$. In the example above, the terms before the turnstile {\verb"|-"} are type inclusion assumptions used by {\verb"simp"} in simplifying {\verb"pre AddBirthday"}. The function {\tt simp} uses some simple heuristics (e.g.~the `One Point Rule' \cite{Z:Pott90}, which is implemented in the {\verb"unwind"} library), to simplify the supplied term. The heuristics are adequate here, but not for more complex examples (see {\tt RAddBirthday} below). Special purpose theorem proving tools like {\tt simp} are easy for users to implement for themselves in \ML. Sets are regarded as primitive in \Z, but in \HOL\ they must be defined. Fortunately, \HOL's {\tt sets} library defines a type of sets and the usual operations of set theory. It also defines the set comprehension notation: $${\verb"{"}~E[x_1,\cdots,x_n]~{\verb"|"}~P[x_1,\cdots,x_n]~{\verb"}"}$$ which is equivalent to: $${\verb"{"}~x~{\verb"|"}~\exists x_1\cdots x_n.~ x = E[x_1,\cdots,x_n] ~\wedge~ P[x_1,\cdots,x_n]~{\verb"}"}$$ Thus the \Z\ set comprehension notation $\{S\spot E\}$ is translated into $\{E\mid S\}$ in \HOL. It would be possible to support \Z's comprehension notation directly, but as the translation is so direct this has not been done. The theory {\tt Z} provides the definitions of some of the set theoretic operators in \Z\ and its mathematical toolkit. For example, \Z\ functions are a special case of relations: \[ \begin{array}{@{}lll} X \rel Y & = & \power(X \cross Y) \also X \pfun Y & = & \{f : X \rel Y \mid (\forall x : X; y_1,y_2:Y\spot\\ && \t2 (x\mapsto y_1)\in f \land (x\mapsto y_2)\in f \implies y_1 = y_2)\} \end{array} \] The corresponding \HOL\ definitions are: \begin{verbatim} X <-> Y = P(X >< Y) X -+> Y = {f | f IN (X <-> Y) /\ (!x y1 y2. (x|->y1) IN f /\ (x|->y2) IN f ==> (y1 = y2))} \end{verbatim} \noindent where {\verb"!"} is \HOL's notation for the universal quantifier $\forall$. These definitions are `generic': {\verb"X"} and {\verb"Y"} range over sets of arbitrary elements. In the \HOL\ logic functions are a primitive concept and unlike in \Z\ are not regarded as certain kinds of sets. The \HOL\ notation $f${\tt (}$x${\tt )}, which can also be written without brackets as just $f~x$, denotes the application of the logical function $f$ to argument $x$. If $f$ is a set of ordered pairs, then this is not a well-formed \HOL\ term -- only logical functions can be applied to arguments. To get around this problem occurrences of $f${\tt (}$x${\tt )}, where $f$ has been previously declared to be a function graph, are preprocessed to $f${\verb"^^"}$x$, where {\verb"^^"} is an infix operator for `applying' sets defined in the theory {\tt Z} (see section~\ref{zops}). The specification presented so far can be further tested by proving the property discussed on page 5 of ZRM. In \Z\ notation this is: \[ AddBirthday \vdash known' = known \cup \{name?\} \] \noindent In \HOL\ the proof proceeds as follows: \begin{session}\begin{alltt} #prove_theorem # (`known_UNION`, # "[AddBirthday] |-? (known' = known UNION {name?})", # REWRITE_ALL_TAC[SCHEMA;CONJL;dom_UNION;dom_SING]);; known_UNION = AddBirthday |- known' = known UNION {name?} \end{alltt}\end{session} The input has the form \verb"prove_theorem("$name$\verb","$goal$\verb","$tactic$\verb")". This instructs \HOL\ to try to prove $goal$ using $tactic$. A goal of the form {\verb"["}$t_1${\verb";"}$\ldots${\verb";"}$t_n${\verb"] |-? "}$t$ is solved if $tactic$ proves the theorem $t_1${\verb","}$\ldots${\verb","}$t_n${\verb" |- "}$t$. A goal just consisting of a term $t$ has no assumptions and is solved if $tactic$ proves the theorem {\verb" |- "}$t$ (see the example in box~18 below). The tactic used above rewrites the goal and assumptions with the definitions of {\tt SCHEMA} and {\tt CONJL} (see section~\ref{zops}) and also with the following two laws (which are pre-proved in the theory {\tt Z}, see section~\ref{zops}). \begin{verbatim} dom_UNION |- dom(X UNION Y) = (dom X) UNION (dom Y) dom_SING |- dom{x |-> y} = {x} \end{verbatim} \noindent If the proof succeeds, as it does here, then the resulting theorem value is bound to $name$ in the metalanguage \ML\ and may be used subsequently. \begin{session}\begin{verbatim} #known_UNION;; AddBirthday |- known' = known UNION {name?} #show_schemas true;; #known_UNION;; SCHEMA [known :: (P NAME);birthday :: (NAME -+> DATE);known' :: (P NAME); birthday' :: (NAME -+> DATE);name? :: NAME;date? :: DATE] [known = dom birthday; known' = dom birthday'; ~name? IN known; birthday' = birthday UNION {name? |-> date?}] |- known' = known UNION {name?} \end{verbatim}\end{session} The next operation schema in the birthday book specification is: \begin{schema}{FindBirthday} \Xi BirthdayBook \\ name? : NAME \\ date! : DATE \where name? \in known \also date! = birthday(name?) \end{schema} \noindent This uses the $\Xi$ (no change of state) convention in the declaration. \begin{session}\begin{verbatim} #declare # `FindBirthday` # "SCHEMA # [XI BirthdayBook; # name? :: NAME; # date! :: DATE] # %-----------------------% # [name? :: known; # date! = birthday(name?)]";; \end{verbatim}\end{session} \noindent The schema {\tt FindBirthday} is expanded out to a term logically equivalent to: \begin{verbatim} SCHEMA [known :: (P NAME); birthday :: (NAME -+> DATE); known' :: (P NAME); birthday' :: (NAME -+> DATE); name? :: NAME; date! :: DATE] [known = dom birthday; known' = known; birthday' = birthday; name? :: known; date! = birthday ^^ name?]" : term \end{verbatim} \noindent The actual expansion is described in section~\ref{io}. A second lemma to check the specification can now be proved. In \Z\ notation it is: \[ (AddBirthday \semi FindBirthday) \vdash (date! = date?) \] \noindent This checks that a subsequent $FindBirthday$ operation results in the same date for a given name as that provided by a previous $AddBirthday$ operation. The hypothesis is the sequential composition of two schemas. This illustrates the shallowness of the embedding of \Z. The composition of schemas is computed when they are input by the preprocessor: {\tt SEQ} acts like a macro. With a {\em deep embedding} (see section~\ref{embed}) the composition operator {\tt SEQ} would have to be defined in the object logic. \begin{session}\begin{alltt} #prove_theorem # (`SEQ_AddBirthday_FindBirthday`, # "[AddBirthday SEQ FindBirthday] |-? (date! = date?)", # REWRITE_ALL_TAC[SCHEMA;CONJL] # THEN POP_ASSUM STRIP_ASSUME_TAC # THEN SMART_ELIMINATE_TAC # THEN IMP_RES_TAC Ap_UNION2 # THEN ASM_REWRITE_TAC[]);; SEQ_AddBirthday_FindBirthday = SCHEMA [known :: (P NAME);birthday :: (NAME -+> DATE);known' :: (P NAME); birthday' :: (NAME -+> DATE);name? :: NAME; date? :: DATE;date! :: DATE] [?known'' birthday''. (known'' :: (P NAME) \verb"/\" birthday'' :: (NAME -+> DATE)) \verb"/\" (known = dom birthday) \verb"/\" (known'' = dom birthday'') \verb"/\" ~name? IN known \verb"/\" (birthday'' = birthday UNION {name? |-> date?}) \verb"/\" (known'' = dom birthday'') \verb"/\" (known' = dom birthday') \verb"/\" ((`birthday`,birthday'),`known`,known' = (`birthday`,birthday''),`known`,known'') \verb"/\" name? :: known'' \verb"/\" (date! = birthday'' ^^ name?)] |- date! = date? \end{alltt}\end{session} \noindent The symbol {\verb"?"} is \HOL's notation for the universal quantifier $\exists$. Iterated quantifications of the form $Q~x_1\cdots x_n${\verb"."}$t$ and $Q~x_1\cdots x_n${\verb"::"}$S${\verb"."}$t$ are allowed (where $Q$ is either {\verb"!"} or {\verb"?"}). The tactic above has the form $tac_1~{\tt THEN}~tac_2~{\tt THEN}~tac_3~{\tt THEN}~tac_5~{\tt THEN}~tac_5$, which instructs \HOL\ to apply $tac_1 \ldots tac_5$ in that order: \begin{itemize} \item$tac_1$ rewrites the goal with the definitions of {\tt SCHEMA} and {\tt CONJL}; \item $tac_2$ simplifies and `explodes' the assumption; \item $tac_3$ is {\verb"SMART_ELIMINATE_TAC"} which removes redundant assumptions (it was contributed \footnote{HOL is distributed with both a library and a {\tt contrib} directory. The former contains uniformly documented material; the latter contains less formal contributions including {\tt SMART\_ELIMINATE\_TAC}.} by Donald Syme of the Australian National University); \item $tac_4$ tries to combine the preproved law {\verb"Ap_UNION2"} with assumptions using Modus Ponens, where {\verb"Ap_UNION2"} is: \begin{verbatim} |- ~x IN (dom X) ==> ((X UNION {x |-> v}) ^^ x = v) \end{verbatim} \item $tac_5$ rewrites with all the current assumptions (including any extra ones generated by $tac_4$). \end{itemize} Switching off schema printing causes the input form to be reconstructed. (How this is done is explained in section~\ref{io}.) \begin{session}\begin{verbatim} #show_schemas false;; #SEQ_AddBirthday_FindBirthday;; AddBirthday SEQ FindBirthday |- date! = date? \end{verbatim}\end{session} The next two schemas given in ZRM ($Remind$ and $InitBirthdayBook$) do not add anything new and are omitted. The birthday book uses a `free set' called $REPORT$, defined in \Z\ by: \begin{zed} REPORT ::= ok \mid already\_known \mid not\_known \end{zed} \noindent Such definitions are supported in \HOL\ using a type definition facility written by Tom Melham \cite{Melham} (which is slightly repackaged for use with {\tt Z}). \begin{session}\begin{verbatim} #free_set `REPORT = ok | already_known | not_known`;; \end{verbatim}\end{session} \noindent Melham's package only supports a subset of \Z's free types. A wider class is definable in Isabelle's ZF application using a fixpoint method developed by Paulson \cite{paulson-fixedpt}. This approach suggests a way of handling more of \Z's free types in \HOL; see also \cite{Z:Smit92}. Next a couple of routine schema declarations to handle success and error conditions: \begin{schema}{Success} result!: REPORT \where result! = ok \end{schema} \begin{schema}{AlreadyKnown} \Xi BirthdayBook \\ name? : NAME \\ result! : REPORT \where name? \in known \also result! = already\_known \end{schema} \noindent These are input to \HOL\ by: \begin{session}\begin{verbatim} #declare # `Success` # "SCHEMA # [result! :: REPORT] # %-----------------% # [result! = ok]";; \end{verbatim}\end{session} \noindent and \begin{session}\begin{verbatim} #declare # `AlreadyKnown` # "SCHEMA # [XI BirthdayBook; # name? :: NAME; # result! :: REPORT] # %-----------------------% # [name? :: known; # result! = already_known]";; \end{verbatim}\end{session} The next schema in the birthday book uses schema conjunction and disjunction: \begin{zed} RAddBirthday \defs (AddBirthday \land Success) \lor AlreadyKnown \end{zed} The conjunction and disjunction of schemas is computed on input, just as for the sequential composition {\tt SEQ}. {\tt AND} and {\tt OR} can be regarded as macros. \begin{session}\begin{verbatim} #declare # `RAddBirthday` # "(AddBirthday AND Success) OR AlreadyKnown";; "RAddBirthday" : term #show_schemas true;; #"RAddBirthday";; "SCHEMA [known :: (P NAME); birthday :: (NAME -+> DATE); known' :: (P NAME); birthday' :: (NAME -+> DATE); name? :: NAME; date? :: DATE; result! :: REPORT] [(known = dom birthday) /\ (known' = dom birthday') /\ ~name? IN known /\ (birthday' = birthday UNION {name? |-> date?}) /\ (result! = ok) \/ (known = dom birthday) /\ (known' = known) /\ (birthday' = birthday) /\ name? :: known /\ (result! = already_known)]" : term \end{verbatim}\end{session} \noindent Note that in \HOL, {\verb"/\"} binds tighter than {\verb"\/"}, so the body of this schema is a disjunction of conjunctions. It is easy to prove it equivalent to: \def\RAddBirthday{RAddBirthday} \begin{schema}{\RAddBirthday} \Delta BirthdayBook \\ name? : NAME \\ date? : DATE \\ result! : REPORT \where (name? \notin known \land \\ \t1 birthday' = birthday \cup \{name? \mapsto date?\} \land \\ \t1 result! = ok) \lor\\ %\also (name? \in known \land \\ \t1 birthday' = birthday \land \\ \t1 result! = already\_known) \end{schema} \noindent From now on the tactics used to prove theorems will be omitted. %%% I've made the following into a figure to help avoid bad page breaks. %%% I think some tweaking may be necessary in the final version. %%% MJCG has undone this! %\begin{figure} \begin{session}\begin{alltt} #show_schemas false;; #prove_theorem # (`RAddBirthdayLemma`, # "(AddBirthday AND Success) OR AlreadyKnown = # SCHEMA # [DELTA BirthdayBook; # name? :: NAME; # date? :: DATE; # result! :: REPORT] # %-------------------------------------------------------% # [(~(name? IN known) \verb"/\" # (birthday' = birthday UNION {name? |-> date?}) \verb"/\" # (result! = ok)) \verb"\/" # (name? IN known \verb"/\" # (birthday' = birthday) \verb"/\" # (result! = already_known))]", # \(\) );; RAddBirthdayLemma = |- RAddBirthday = SCHEMA [known :: (P NAME);birthday :: (NAME -+> DATE);known' :: (P NAME); birthday' :: (NAME -+> DATE);name? :: NAME;date? :: DATE; result! :: REPORT] [known = dom birthday;known' = dom birthday'; ~name? IN known \verb"/\" (birthday' = birthday UNION {name? |-> date?}) \verb"/\" (result! = ok) \/ name? IN known \verb"/\" (birthday' = birthday) \verb"/\" (result! = already_known)] \end{alltt}\end{session} %\caption{Proof of logical equivalence in HOL.\label{lemma1}} %\end{figure} This proof confirms informal remarks made on page 9 of ZRM (page 10 in the first edition). Note that the left hand side of the equation proved is printed as {\tt RAddBirthday} rather than as {\tt (AddBirthday AND Success) OR AlreadyKnown}. This is because the former is recognized as being defined equal to the latter. The right hand side of the equation has not previously been given a name, so it is printed out in full. A further check on $RAddBirthday$ is to show that its precondition is true. Unfortunately, {\tt simp} is not powerful enough: \begin{session}\begin{verbatim} #simp "pre RAddBirthday";; known :: (P NAME), birthday :: (NAME -+> DATE), name? :: NAME, date? :: DATE |- pre RAddBirthday = (?known' birthday' result!. (known' :: (P NAME) /\ birthday' :: (NAME -+> DATE) /\ result! :: REPORT) /\ ((known = dom birthday) /\ (known' = dom birthday') /\ ~name? IN known /\ (birthday' = birthday UNION {name? |-> date?}) /\ (result! = ok) \/ (known = dom birthday) /\ (known' = dom birthday') /\ ((birthday' = birthday) /\ (known' = known)) /\ name? :: known /\ (result! = already_known))) \end{verbatim}\end{session} \noindent The heuristics employed by {\tt simp} cannot deal with the existentially quantified disjunction. They could be improved to work for this example, but sooner or later another example would crop up that is not handled. What is required is user guided simplification. This can be achieved in various ways, the approach illustrated here is to prove that the precondition is true with a user-supplied tactic. \begin{session}\begin{alltt} #prove_theorem # (`pre_RAddBirthday`, # "[BirthdayBook; sig RAddBirthday] |-? pre RAddBirthday", # \(\) );; pre_RAddBirthday = BirthdayBook, sig RAddBirthday |- pre RAddBirthday \end{alltt}\end{session} \noindent The {\tt sig} of a schema consists of the type membership statements of its variables. \[ \verb"sig (SCHEMA ["x_1\verb"::"S_1\verb";"\ldots\verb";"x_n\verb"::" S_n\verb"] ["\cdots\verb"]) = "x_1\in S_1\land\ldots\land x_n\in S_n \] The last three schema definitions in the abstract specification of the birthday book are $NotKnown$, $RFindBirthday$ and $RRemind$. These are straightforward and are omitted here. In section~1.5 of ZRM the operations and data structures of the birthday book are implemented. The concrete operation corresponding to $BirthdayBook$ is $BirthdayBook1$, where: \begin{schema}{BirthdayBook1} names : \nat_1 \fun NAME \\ dates : \nat_1 \fun DATE \\ hwm : \nat \where \forall i, j : 1 \upto hwm \spot i \neq j \implies names(i) \neq names(j) \end{schema} The \HOL\ version of this uses the terms {\tt NN} and {\verb"NN_1"} which denote the sets of natural numbers and strictly positive natural numbers, respectively. The notation $m${\verb".."}$n$ denotes the set of numbers in the closed interval $[m,n]$ (``{\verb".."}'' is a \HOL\ infix operator). \HOL{} allows restricted quantifications of the form {\verb"!"}$x${\verb"::"}$S${\verb"."}$t$ and {\verb"?"}$x${\verb"::"}$S${\verb"."}$t$ (where $S$ is a term denoting a set), which are equivalent to {\verb"!"}$x${\verb"."}$x~${\tt IN}$~S${\verb" ==> "}$t$ and {\verb"?"}$x${\verb"."}$x~${\tt IN}$~S${\verb" /\ "}$t$, respectively. The infix operator {\verb"-->"} is defined in the theory {\tt Z} and constructs the set of total functions. Using these notations, the \Z\ schema above is input into \HOL\ as: \begin{session}\begin{verbatim} #declare # `BirthdayBook1` # "SCHEMA # [names :: (NN_1-->NAME); # dates :: (NN_1-->DATE); # hwm :: NN] # %---------------------------------------------------% # [!i j::(1..hwm). ~(i = j) ==> ~(names(i) = names(j))]";; \end{verbatim}\end{session} The relation between $BirthdayBook$ and its implementation $BirthdayBook1$ is specified with the schema $Abs$: \begin{schema}{Abs} BirthdayBook \\ BirthdayBook1 \where known = \{~ i : 1 \upto hwm \spot names(i) ~\} \also \forall i : 1 \upto hwm \spot birthday(names(i)) = dates(i) \end{schema} \noindent The \HOL\ version is: \begin{session}\begin{verbatim} #declare # `Abs` # "SCHEMA # [BirthdayBook; # BirthdayBook1] # %-------------------------------------------% # [known = {names(i) | i::(1..hwm)}; # !i::(1..hwm). birthday(names(i)) = dates(i)]";; \end{verbatim}\end{session} The implementation of $AddBirthday$ is $AddBirthday1$, where: \begin{schema}{AddBirthday1} \Delta BirthdayBook1 \\ name? : NAME \\ date? : DATE \where \forall i: 1 \upto hwm \spot name? \neq names(i) \also hwm' = hwm + 1 \\ names' = names \oplus \{ hwm' \mapsto name? \} \\ dates' = dates \oplus \{ hwm' \mapsto date? \} \end{schema} \noindent The \HOL\ version of this is: \begin{session}\begin{verbatim} #declare # `AddBirthday1` # "SCHEMA # [DELTA BirthdayBook1; # name? :: NAME; # date? :: DATE] # %-----------------------------------% # [!i::(1..hwm). ~(name? = names(i)); # hwm' = hwm + 1; # names' = names (+) {hwm' |-> name?}; # dates' = dates (+) {hwm' |-> date?}]";; \end{verbatim}\end{session} The final three schemas in the implementation of the birthday book are $FindBirthday1$, $AbsCards$, $Remind1$ and $InitBirthdayBook1$. They introduce nothing new and are omitted. The specification of the implementation of the birthday book is now complete. The soundness of the implementation can be verified by proving that the rules for operation and data refinement are met. These rules are described in sections 5.5 and 5.6 of ZRM. When applied to the birthday book, they generate the following two conditions: %%% Old theorems: % \[ % 1.~ \pre AddBirthday \land Abs \implies \pre AddBirthday1 % \also % 2.~ \pre AddBirthday \land Abs \land AddBirthday1 \\ % \phantom{2.~} % \implies \\ % \phantom{2.~} % (\exists BirthdayBook' \spot Abs' \land AddBirthday) % \] %%% New theorems: (make HOL match) %%% Add \vdash in front? \begin{zed} \forall BirthdayBook; BirthdayBook1; name?:NAME; date?:DATE \spot \\ \t1 \pre AddBirthday \land Abs \implies \pre AddBirthday1 \also \forall BirthdayBook; BirthdayBook1; BirthdayBook1'; \\ \t1 name?:NAME; date?:DATE \spot \\ \t2 \pre AddBirthday \land Abs \land AddBirthday1 \\ \t2 \implies (\exists BirthdayBook' \spot Abs' \land AddBirthday) \end{zed} %%% A different paragraph should be sustituted for the following if %%% required. %%% \noindent The operator $\land$ here is schema conjunction, whereas %%% the operator $\implies$ is logical implication\footnote{Z experts %%% may like to ponder on why this is the case.}. The quantifier %%% $\exists$ is schema quantification. It is straightforward to verify these properties in \HOL. The proofs are quite a bit more complex than previous ones, involving various mathematical laws (see section~\ref{zops}) and extensive case analysis. The details will not be given here, but are available in the directory {\verb+contrib/Z/examples+} distributed with \HOL 88 Version 2.02. The first theorem establishes that the precondition of $AddBirthday1$ is liberal enough. %%% Update HOL to match theorems above. %%% Also add example on p140 of ZRM2 (functional data refinement) %%% if you have the time: (uncomment out and position the following %%% suitably if so) %%% \[ %%% \forall BirthdayBook; BirthdayBook'; %%% BirthdayBook1; BirthdayBook1'; \\ %%% \t1 name?:NAME; date?:DATE \spot \\ %%% \t2 \pre AddBirthday \land Abs \land AddBirthday1 \\ %%% \t2 \implies AddBirthday %%% \] \begin{session}\begin{alltt} #prove_theorem # (`AbsThm1`, # "FORALL [BirthdayBook; BirthdayBook1; (name?::NAME); (date?::DATE)] # ((pre AddBirthday \verb"/\" Abs) ==> (pre AddBirthday1))", # \(\) );; AbsThm1 = |- FORALL [BirthdayBook;BirthdayBook1;name? :: NAME;date? :: DATE] (pre AddBirthday \verb"/\" Abs ==> pre AddBirthday1) \end{alltt}\end{session} \noindent The schema operations {\tt pre} and {\tt FORALL} are expanded on input. Note that {\tt FORALL} is interpreted as yielding a predicate not a schema (the quantifier {\verb"SCHEMA_FORALL"} returns a schema). There is no standard way of formulating theorems about \Z\ schemas (though a start is made in Annexe F of the {\em \Z\ Base Standard\/} \cite{Z:Brie92}). For example, the two theorems in \Z\ notation above admit a variety of formal interpretations. `$\pre AddBirthday \land Abs$' could be interpreted as either a schema expression or as a predicate; in the former case $\land$ is a schema operation (represented by {\tt AND} in \HOL), in the latter case it is a logical operation (\verb"/\" in \HOL). In this particular case the two interpretations of conjunction result in logically equivalent terms in \HOL, but in general it is unclear if this will always be the case (particularly with implications and quantifications). The convention for theorems adopted here is, wherever possible, to interpret \Z's logical operators as operators that construct predicates rather than schemas. Other choices are possible, for example the following version of {\tt AbsThm1} is also provable: \begin{verbatim} FORALL [BirthdayBook; BirthdayBook1; (name?::NAME); (date?::DATE)] ((pre AddBirthday AND Abs) ==> (pre AddBirthday1)) \end{verbatim} The second theorem establishes that $AddBirthday1$ produces the right answer. \begin{session}\begin{alltt} #prove_theorem # (`AbsThm2`, # "FORALL [BirthdayBook; BirthdayBook1; BirthdayBook1'; # (name?::NAME); (date?::DATE)] # ((pre AddBirthday \verb"/\" Abs \verb"/\" AddBirthday1) # ==> # (EXISTS BirthdayBook' (Abs' \verb"/\" AddBirthday)))", # \(\) );; AbsThm2 = |- FORALL [BirthdayBook; BirthdayBook1; BirthdayBook1'; name? :: NAME; date? :: DATE] (pre AddBirthday \verb"/\" Abs \verb"/\" AddBirthday1 ==> EXISTS BirthdayBook'(Abs' \verb"/\" AddBirthday)) \end{alltt}\end{session} \noindent The schema operations {\tt pre}, {\tt FORALL} and {\tt EXISTS} are expanded on input. {\tt FORALL} and {\tt EXISTS} are interpreted as yielding predicates not schemas (the quantifier {\verb"SCHEMA_EXISTS"} returns a schema). The priming conventions for schemas are also handled on input. For example, \begin{session}\begin{verbatim} #show_schemas true;; #"BirthdayBook";; "SCHEMA [known :: (P NAME);birthday :: (NAME -+> DATE)] [known = dom birthday]" : term #"BirthdayBook'";; "SCHEMA [known' :: (P NAME);birthday' :: (NAME -+> DATE)] [known' = dom birthday']" : term \end{verbatim}\end{session} It is a tribute to \Z's notational power using the schema notation that complex theorems like $AbsThm1$ and $AbsThm2$ can be expressed concisely. This complexity is revealed if the \Z\ printing is switched off so that the semantic representations of schemas is output as illustrated in box~25. This graphically illustrates why the schema notation was invented to structure and hide the mass of detailed mathematics which can be held in a \Z\ specification. %%% I've made the following into a figure to help avoid bad page breaks. %%% I think some tweaking may be necessary in the final version. %%% Undone by MJCG! %\begin{figure} \begin{session}{\footnotesize\baselineskip=8pt\begin{verbatim} #AbsThm2;; |- !known birthday. known :: (P NAME) /\ birthday :: (NAME -+> DATE) ==> known :: (P NAME) /\ birthday :: (NAME -+> DATE) /\ (known = dom birthday) ==> (!names dates hwm. names :: (NN_1 --> NAME) /\ dates :: (NN_1 --> DATE) /\ hwm :: NN ==> names :: (NN_1 --> NAME) /\ dates :: (NN_1 --> DATE) /\ hwm :: NN /\ (!i j :: 1 .. hwm. ~(i = j) ==> ~(names ^^ i = names ^^ j)) ==> (!names' dates' hwm'. names' :: (NN_1 --> NAME) /\ dates' :: (NN_1 --> DATE) /\ hwm' :: NN ==> names' :: (NN_1 --> NAME) /\ dates' :: (NN_1 --> DATE) /\ hwm' :: NN /\ (!i j :: 1 .. hwm'. ~(i = j) ==> ~(names' ^^ i = names' ^^ j)) ==> (!name?. name? :: NAME ==> (!date?. date? :: DATE ==> SCHEMA [known :: (P NAME);birthday :: (NAME -+> DATE); name? :: NAME;date? :: DATE] [?known' birthday'. (known' :: (P NAME) /\ birthday' :: (NAME -+> DATE)) /\ (known = dom birthday) /\ (known' = dom birthday') /\ ~name? IN known /\ (birthday' = birthday UNION {name? |-> date?})] /\ SCHEMA [known :: (P NAME);birthday :: (NAME -+> DATE); names :: (NN_1 --> NAME);dates :: (NN_1 --> DATE); hwm :: NN] [known = dom birthday; !i j :: 1 .. hwm. ~(i = j) ==> ~(names ^^ i = names ^^ j); known = {names ^^ i | i :: (1 .. hwm)}; !i :: 1 .. hwm. birthday ^^ (names ^^ i) = dates ^^ i] /\ SCHEMA [names :: (NN_1 --> NAME);dates :: (NN_1 --> DATE); hwm :: NN;names' :: (NN_1 --> NAME); dates' :: (NN_1 --> DATE);hwm' :: NN;name? :: NAME; date? :: DATE] [!i j :: 1 .. hwm. ~(i = j) ==> ~(names ^^ i = names ^^ j); !i j :: 1 .. hwm'. ~(i = j) ==> ~(names' ^^ i = names' ^^ j); !i :: 1 .. hwm. ~(name? = names ^^ i);hwm' = hwm + 1; names' = names (+) {hwm' |-> name?}; dates' = dates (+) {hwm' |-> date?}] ==> (?known' birthday'. (known' :: (P NAME) /\ birthday' :: (NAME -+> DATE)) /\ known' :: (P NAME) /\ birthday' :: (NAME -+> DATE) /\ (known' = dom birthday') /\ SCHEMA [known' :: (P NAME);birthday' :: (NAME -+> DATE); names' :: (NN_1 --> NAME);dates' :: (NN_1 --> DATE); hwm' :: NN] [known' = dom birthday'; !i j :: 1 .. hwm'. ~(i = j) ==> ~(names' ^^ i = names' ^^ j); known' = {names' ^^ i | i :: (1 .. hwm')}; !i :: 1 .. hwm'. birthday' ^^ (names' ^^ i) = dates' ^^ i] /\ SCHEMA [known :: (P NAME);birthday :: (NAME -+> DATE); known' :: (P NAME);birthday' :: (NAME -+> DATE); name? :: NAME;date? :: DATE] [known = dom birthday;known' = dom birthday'; ~name? IN known; birthday' = birthday UNION {name? |-> date?}]))))) \end{verbatim}}\end{session} %\caption{An example of expanding a theorem.\label{AbsThm2}} %\end{figure} \bigskip As a final example, here is the ``sufficient condition'' for the correct implementation of the sequential composition of {\verb+AddBirthday+} and {\verb+FindBirthday+} that is described in general terms on page 134 of ZRM. This is much easier to prove than either {\verb"AbsThm1"} or {\verb"AbsThm2"}. The sufficient condition for the composition of {\verb+AddBirthday1+} and {\verb+FindBirthday1+} is also easy to prove. Note that {\verb"show_schema true"} is still in force. \begin{session}{\footnotesize\begin{alltt} #prove_theorem # (`AddFindSeq`, # "FORALL # [BirthdayBook''] # ((EXISTS[AddBirthday](theta BirthdayBook' = theta BirthdayBook'')) # ==> # (EXISTS[FindBirthday](theta BirthdayBook = theta BirthdayBook'')))", # \(\) );; AddFindSeq = |- !known'' birthday''. known'' :: (P NAME) \verb"/\" birthday'' :: (NAME -+> DATE) ==> known'' :: (P NAME) \verb"/\" birthday'' :: (NAME -+> DATE) \verb"/\" (known'' = dom birthday'') ==> (?known birthday known' birthday' name? date?. (known :: (P NAME) \verb"/\" birthday :: (NAME -+> DATE) \verb"/\" known' :: (P NAME) \verb"/\" birthday' :: (NAME -+> DATE) \verb"/\" name? :: NAME \verb"/\" date? :: DATE) \verb"/\" known :: (P NAME) \verb"/\" birthday :: (NAME -+> DATE) \verb"/\" known' :: (P NAME) \verb"/\" birthday' :: (NAME -+> DATE) \verb"/\" name? :: NAME \verb"/\" date? :: DATE \verb"/\" (known = dom birthday) \verb"/\" (known' = dom birthday') \verb"/\" ~name? IN known \verb"/\" (birthday' = birthday UNION {name? |-> date?}) \verb"/\" ((`birthday`,birthday'),`known`,known' = (`birthday`,birthday''),`known`,known'')) ==> (?known birthday known' birthday' name? date!. (known :: (P NAME) \verb"/\" birthday :: (NAME -+> DATE) \verb"/\" known' :: (P NAME) \verb"/\" birthday' :: (NAME -+> DATE) \verb"/\" name? :: NAME \verb"/\" date! :: DATE) \verb"/\" known :: (P NAME) \verb"/\" birthday :: (NAME -+> DATE) \verb"/\" known' :: (P NAME) \verb"/\" birthday' :: (NAME -+> DATE) \verb"/\" name? :: NAME \verb"/\" date! :: DATE \verb"/\" (known = dom birthday) \verb"/\" (known' = dom birthday') \verb"/\" ((`birthday`,birthday'),`known`,known' = (`birthday`,birthday),`known`,known) \verb"/\" name? :: known \verb"/\" (date! = birthday ^^ name?) \verb"/\" ((`birthday`,birthday),`known`,known = (`birthday`,birthday''),`known`,known'')) \end{alltt}}\end{session} The implementation of bindings and their extraction (i.e.~$\theta$ in \Z{} and {\verb"theta"} in \HOL) is discussed in section~\ref{io}. \section{How Z is supported in HOL}\label{support} The support for \Z\ illustrated in the previous section has two parts: (i) input and output procedures to handle the various schema operations and to manage schema and variable names, and (ii) the \HOL\ theory {\tt Z} that implements the \Z\ operators and mathematical toolkit. \subsection{Inputting and outputting schemas}\label{io} When a \HOL\ quotation of the form {\verb+"+}$\cdots${\verb+"+} is read a number of transformations are performed. The most important of these are listed below. \begin{enumerate} \item Variables that have previously been declared as schema names with the \ML\ function {\tt declare} are replaced by their semantic representation, which is a term of the form {\verb"SCHEMA ["}$\cdots${\verb"] ["}$\cdots${\verb"]"}. Decorated (e.g.~dashed) schema names are expanded to the appropriately decorated semantic representations (see box~24). \item Applications $s~x$, where $s$ has previously been declared in a schema as a set representing a \Z\ function, are expanded to $s${\verb"^^"}$x$. \item Terms of the form: \begin{enumerate} \item {\tt pre}~{\verb"(SCHEMA ["}$\cdots${\verb"] ["}$\cdots${\verb"])"} \item {\verb"(SCHEMA ["}$\cdots${\verb"] ["}% $\cdots${\verb"])"}~{\tt SEQ}~{\verb"(SCHEMA ["}$\cdots${\verb"] ["}% $\cdots${\verb"])"} \item {\verb"(SCHEMA ["}$\cdots${\verb"] ["}% $\cdots${\verb"])"}~{\tt AND}~{\verb"(SCHEMA ["}$\cdots${\verb"] ["}% $\cdots${\verb"])"} \item {\verb"(SCHEMA ["}$\cdots${\verb"] ["}% $\cdots${\verb"])"}~{\tt OR}~{\verb"(SCHEMA ["}$\cdots${\verb"] ["}% $\cdots${\verb"])"} \item {\verb"(SCHEMA ["}$\cdots${\verb"] ["}% $\cdots${\verb"])"}~{\tt IMPLIES}~{\verb"(SCHEMA ["}% $\cdots${\verb"] ["}$\cdots${\verb"])"} \item {\verb"(SCHEMA ["}$\cdots${\verb"] ["}% $\cdots${\verb"])"}~{\tt HIDE}~{\verb"("}$x_1,\cdots,x_n${\verb")"} \item {\verb"SCHEMA_FORALL "}{\verb"(SCHEMA ["}$\cdots${\verb"] ["}% $\cdots${\verb"])"}~{\verb"(SCHEMA ["}% $\cdots${\verb"] ["}$\cdots${\verb"])"} \item {\verb"SCHEMA_EXISTS "}{\verb"(SCHEMA ["}$\cdots${\verb"] ["}% $\cdots${\verb"])"}~{\verb"(SCHEMA ["}% $\cdots${\verb"] ["}$\cdots${\verb"])"} \end{enumerate} \noindent are expanded out to the appropriate semantic representation of the form {\verb"SCHEMA ["}$\cdots${\verb"] ["}$\cdots${\verb"]"}. The input and result of the expansion is saved in a global data structure, so that it can be inverted when schemas are printed. \item Terms of the form: \begin{enumerate} \item {\verb"FORALL "}{\verb"(SCHEMA ["}$\cdots${\verb"] ["}% $\cdots${\verb"])"}~$P$ \item {\verb"FORALL "}{\verb"("}$x${\verb"::"}$S${\verb")"}~$P$ \item {\verb"EXISTS "}{\verb"(SCHEMA ["}$\cdots${\verb"] ["}% $\cdots${\verb"])"}~$P$ \item {\verb"EXISTS "}{\verb"("}$x${\verb"::"}$S${\verb")"}~$P$ \end{enumerate} \noindent are expanded out to terms representing the appropriate quantifications of the predicate $P$. The input and result of the expansion is saved in a global data structure, so it that can be inverted when schemas are printed. Quantifications of the form {\tt Q}~{\verb"["}$v_1${\verb";"}$\cdots${\verb";"}$v_n${\verb"] "}$P$ are converted into iterated quantifications {\tt Q}~$v_1$~{\verb"("}{\tt Q}~$v_2$~{\verb"("}~$\cdots$~{\verb"("}{\tt Q}~% $v_n~P${\verb")"}~$\cdots$~{\verb")"}{\verb")"}. \item $ \verb"sig (SCHEMA ["x_1\verb":"S_1\verb";"\ldots\verb";"x_n\verb":" S_n\verb"] ["\cdots\verb"])" $ is expanded to the type membership statement: \begin{alltt} \(x\sb{1}\) IN \(S\sb{1}\) \verb"/\" \(x\sb{2}\) IN \(S\sb{2}\) \verb"/\" \(\ldots\) \verb"/\" \(x\sb{m}\) IN \(S\sb{m}\) \end{alltt} \item $ \verb"theta(SCHEMA ["x_1\verb":"S_1\verb";"\ldots\verb";"x_n\verb":" S_n\verb"] ["\cdots\verb"])" $ is expanded to $n$-tuples of pairs of the form: \begin{alltt} ((`\(x\sb{\sigma\sb{1}}\)`, \(x\sb{\sigma\sb{1}}\)), \(\ldots\) , (`\(x\sb{\sigma\sb{n}}\)`, \(x\sb{\sigma\sb{n}}\))) \end{alltt} which represent {\it bindings} in \Z. The sequence $x_{\sigma_1}\ldots x_{\sigma_n}$ is a canonical reordering of $x_1\ldots x_n$, which ensures that equivalent bindings (i.e. ones that are equal up to reordering of components) are translated to the same \HOL{} term. \item {\verb+DELTA+}$~{\cal S}$ is translated to ${\cal S}{\verb+ AND +}{\cal S}{\verb+'+}$. This implements the \Z{} definition: \[ \Delta {\cal S} ~\defs~ {\cal S} \land {\cal S}' \] \item {\verb+XI+}$~{\cal S}$ is translated to {\verb+SCHEMA[DELTA +}${\cal S}${\verb+][theta+}${\cal S}{\verb+'+}${\verb+ = theta+}${\cal S}${\verb+]+}. This implements the \Z{} definition: \[ \Xi {\cal S} ~\defs~ [ \Delta {\cal S} | \theta {\cal S}' = \theta {\cal S} ] \] \end{enumerate} When a term is output by \HOL, any schema representations that have previously been given a name are replaced by the name. In addition, any representation resulting from of one of the expansions in 3 -- 8 above is replaced by the input to the expansion. For example, if $S_1~{\tt SEQ}~S_2$ expands to $S_3$ (3b above), then $S_3$ will be output as $S_1~{\tt SEQ}~S_2$. This process is applied recursively. The method of fully expanding out schemas into their semantic representations works well for small examples like the birthday book. The interactions shown in the boxed sections mostly happen instantaneously (though the proofs of {\verb"AbsThm1"} and {\verb"AbsThm2"} take a few seconds to run). However, the underlying terms can get large and it is possible that `industrial scale' specifications might slow down \HOL\ unacceptably. If this were the case then abbreviatory definitions could be used to prevent terms getting too large. Such abbreviations could be introduced automatically (e.g.~by the \ML\ function {\verb"declare"}). Fortunately performance has been adequate so far and such measures have not been felt necessary. \subsection{Shallow versus deep embedding}\label{embed} Shallow embedding can be contrasted with {\it deep embedding\/} \cite{Embedding,Melham} in which both the syntax and semantics of the embedded language are formalized inside the host logic. With shallow embedding the mapping from language constructs to their semantic representations is part of the metalanguage; with deep embedding it is part of the object language theory. It is usually more work to support a language by deep embedding, but it is necessary if one wants to prove theorems about the language rather than just reason in it. Since the schema operations are `macro expanded' away, it is not possible to state general theorems about them. For example, it is impossible to express the fact that schema conjunction is commutative. For any particular schema one can prove the instance of the fact, but such proofs have to be repeated for each separate instance (though they can be performed automatically with a suitable derived rule). A weakness of shallow embedding is that the operations that are computed outside the logic are not subject to the same `quality control' as operations specified in the logic, because errors in the definition of operators reside in program code not in logical formulae. Generally the latter are easier to inspect for correctness than the former. For example, if the macro expansion of {\tt SEQ} contained a bug (e.g.~dashed variables were sometimes invalidly captured by quantifiers) then this might only manifest itself in the wrong schema expansion being computed. If in addition the output routines `inverted' the bug the user might be unaware that the wrong semantic representation was being manipulated. A deep embedding allows meta-theorems to be proved (e.g.~the associativity of schema sequencing) that can serve to partially validate the definitions of the operators. A deep embedding of \Z\ in \HOL\ is possible. It could, for example, be based on the metatheory presented in the \Z\ base standard \cite{Z:Brie92}. The resulting theory would be complex and probably hard to apply to particular examples like the birthday book. However, it would be suitable for testing out the meta-theory of \Z\ and verifying general properties of it (e.g.~see the work by Maharaj briefly discussed below). The distinction between ``shallow'' and ``deep'' is not always sharp. For example, ProofPower provides a much `deeper' embedding than the one described here (all the \Z\ operators are defined in \HOL) but there is no single semantic function defined in the the logic that maps \Z\ syntax into its meaning. ProofPower's embedding is not `deep enough' to allow facts like the commutativity of schema conjunction to be proved. The lightweight shallow embedding illustrated here puts relatively few obstacles in the way of using all the power of \HOL\ to reason about particular \Z\ specifications, but it is useless for verifying properties of \Z\ itself. \subsection{Z's operators in HOL}\label{zops} The operators used in the birthday book are included in those shown in the table below. The {\small\tt ASCII} versions of the \Z\ operators are based on those used by the \fuzz\ and ZTC type-checking tools \cite{Z:Spiv92b,Z:ZTC}. %\begin{table} \begin{center} \begin{tabular}{|l|l|l|} \hline \Z\ operator & \HOL\ notation & Meaning \\ \hline & & \\[-1ex] $:$ & {\verb"::"} & Membership declaration\\ $\dom$ & {\verb"dom"} & Domain\\ $\mapsto$ & {\verb"|->"} & Maplet\\ $\power$ & {\verb"P"} & Power set\\ $\cross$ & {\verb"><"} & Cartesian product\\ $\rel$ & {\verb"<->"} & Binary relations\\ $\pfun$ & {\verb"-+>"} & Partial functions\\ $\fun$ & {\verb"-->"} & Total functions\\ & {\verb"^^"} & Application of \Z\ functions\\ $\ndres$ & {\verb"<+"} & Domain anti-restriction\\ $\oplus$ & {\verb"(+)"} & Relational overriding\\ $\nat$ & {\verb"NN"} & Natural numbers\\ $\nat_1$ & {\verb"NN_1"} & Strictly positive integers\\ $\upto$ & {\verb".."} & Number range\\ \hline \end{tabular} \end{center} %\caption{Z and HOL operators.\label{notation}} %\end{table} The operators in this table are defined (in \HOL\ notation) by: \begin{verbatim} |- (CONJL[] = T) /\ (!b bl. CONJL(CONS b bl) = b /\ CONJL bl) |- SCHEMA decs body = CONJL decs /\ CONJL body |- x :: s = x IN s |- x |-> y = x,y |- dom R = {x | ?y. (x |-> y) IN R} |- P X = {Y | Y SUBSET X} |- X >< Y = {(x,y) | x IN X /\ y IN Y} |- X <-> Y = P(X >< Y) |- X -+> Y = {f | f IN (X <-> Y) /\ (!x y1 y2. (x |-> y1) IN f /\ (x |-> y2) IN f ==> (y1 = y2))} |- X --> Y = {f | f IN (X -+> Y) /\ (dom f = X)} |- f^^x = @y. (x,y) IN f |- S <+ R = {x |-> y | ~x IN S /\ (x |-> y) IN R} |- f (+) g = ((dom g) <+ f) UNION g |- NN = {n | n >= 0} |- NN_1 = {n | n > 0} |- m .. n = {i | m <= i /\ i <= n} \end{verbatim} \noindent The \HOL\ function \verb"CONJL" conjoins a list of predicates. The set application operator {\verb"^^"} is defined using the \HOL\ choice operator {\verb"@"}, which is Hilbert's $\varepsilon$-symbol. The term {\verb"@"}$x${\verb"."}$P[x]$ denotes some value, $a$ say, such that $P[a]$ is true. {\verb"@"} is related to the \Z\ $\mu$-operator, but unlike $\mu$ does not require $P[x]$ to be satisfied by a unique value. The conventional logical symbol corresponding to $\mu$ in \Z\ is the unique existence operator $\iota$. If no $a$ exists such that $P[a]$ is true, then {\verb"@"}$x${\verb"."}$P[x]$ denotes an arbitrary value. It would be possible to choose this arbitrary value in a canonical way, but its underlying \HOL\ type must be the same as that of $x$ in $P[x]$. The theory {\tt Z} also contains \HOL\ theorems about the \Z\ operators. The ones used in proving the theorems in section~\ref{birthdaybook} are listed below: \begin{verbatim} |- dom(X UNION Y) = (dom X) UNION (dom Y) |- dom{x |-> y} = {x} |- x IN (dom{x |-> y}) |- f IN (X -+> Y) /\ x IN (dom f) ==> x IN X |- f IN (X -+> Y) ==> (dom f) IN (P X) |- x IN X /\ y IN Y ==> {x |-> y} IN (X -+> Y) |- f IN (X -+> Y) /\ x IN X /\ y IN Y /\ ~x IN (dom f) ==> (f UNION {x |-> y}) IN (X -+> Y) |- f IN (X --> Y) ==> (dom f = X) |- f IN (X --> Y) ==> f IN (X -+> Y) |- ~(x1 = x2) ==> ((X UNION {x1 |-> v}) ^^ x2 = X ^^ x2) |- ~x IN (dom X) ==> ((X UNION {x |-> v}) ^^ x = v) |- {x |-> v} ^^ x = v |- f IN (X -+> Y) /\ x IN (dom f) ==> (!y. (f ^^ x = y) = (x,y) IN f) |- f IN (X -+> Y) ==> (!x. x IN (dom f) = (x,f ^^ x) IN f) |- f IN (X --> Y) /\ g IN (X --> Y) ==> (f (+) g) IN (X --> Y) |- f IN (X -+> Y) /\ g IN (X -+> Y) ==> (f (+) g) IN (X -+> Y) |- f IN (X -+> Y) /\ g IN (X -+> Y) ==> (dom(f (+) g) = (dom f) UNION (dom g)) |- f IN (X -+> Y) /\ g IN (X -+> Y) /\ x IN ((dom f) DIFF (dom g)) ==> ((f (+) g) ^^ x = f ^^ x) |- f IN (X -+> Y) /\ g IN (X -+> Y) /\ x IN (dom g) ==> ((f (+) g) ^^ x = g ^^ x) |- n IN NN |- (n + 1) IN NN_1 |- f IN (NN_1 --> X) /\ v IN X ==> ((f (+) {(n + 1) |-> v}) ^^ (n + 1) = v) |- 1 .. (n + 1) = (1 .. n) UNION ((n + 1) .. (n + 1)) |- x IN (n .. n) = (x = n) |- x IN (m .. n) = m <= x /\ x <= n |- f IN (NN_1 -+> X) /\ x IN X ==> (f (+) {(n + 1) |-> x}) IN (NN_1 -+> X) |- NN_1 UNION {n + 1} = NN_1 |- f IN (NN_1 --> X) /\ x IN X ==> (f (+) {(n + 1) |-> x}) IN (NN_1 --> X) \end{verbatim} \section{Other related work}\label{other} ICL's ProofPower \cite{ProofPower} is an `\LCF-like' system that supports the same version of higher order logic as \HOL, but provides different theorem proving infrastructure. ICL used the original \HOL\ for many years and have built on this experience in designing ProofPower. Although the theorem proving tools are not identical to \HOL's, they are similar in spirit but aim to be more powerful. Some of the features provided have been designed with the needs of \Z\ in mind. ProofPower supports \Z\ via a much `deeper' embedding than the one presented here. The main difference in their approach is that schemas are treated more like set abstractions (yielding a set of bindings), and schema operations are then operators over sets of bindings. Schema references as predicates are treated as abbreviations for membership statements, e.g.~a reference $S$ abbreviates $\theta S\in \hat{S}$, where $\hat{S}$ is the representation of schema $S$. ProofPower has been used for internal applications at ICL and is currently undergoing evaluation in a small group of companies and academic institutions. ProofPower proofs in \Z\ are intended to be conducted with all visible subgoals in \Z\ notation. The language supported is intended to be compatible with the proposed `ISO standard \Z' \cite{Z:Brie92} rather than the \Z\ described in ZRM. ProofPower has a polished interface that understands \Z's special symbols. It has more \Z-specific proof infrastructure and better coverage of the \Z\ notation than the implementation described here. More information is obtainable from the ProofPower server by sending an email message to: {\verb"ProofPower-server@win.icl.co.uk"}. A relatively deep embedding of \Z\ in the type theory UTT (Unifying Theory of dependent Types) has been undertaken by Savi Maharaj \cite{Maharaj}. A method of representing \Z\ schemas in UTT (independently of the \Z\ core language) was developed. The LEGO proof-checker has been used to prove several theorems that are intended to support reasoning about \Z-like specifications at the schema level. For example, introduction and elimination rules for schema conjunction have been verified. Earlier work \cite{Mah90} considered ways of encoding the core language of \Z\ in type theory. The \Z/EVES project at Odyssey Research Associates (ORA) \cite{EVES:Report,EVES:Paper} investigated the feasibility of using EVES, a theorem prover for ZF set theory, as a proof tool for \Z. A standard example from the security community (``The Low Water Mark'') was used as a case study. This was specified in \Z\ and a proof of a non-interference security property performed. Most of the Mathematical Toolkit in ZRM was expressed in EVES and the laws proved and installed as rewrites. EVES is much more automatic than \HOL\ and thus an embedding of Z into EVES might provide proof support with less user interaction. However, the feasibility study was not followed by any tool development. The Balzac project at Imperial Software Technology (IST) is building editing, typesetting, type-checking and proof support for \Z\ \cite{Balzac}; it is funded by contracts from CESG (a UK Government organization). Balzac is a tactic based system in which tactics rather than rules are primitive; the tactic writing language is a secure form of Lisp. The user interface is powerful and sophisticated. The version of \Z{} supported is non-standard (e.g.~basic types are assumed non-empty). Balzac has been used to produce specifications consisting of 500--1000 pages (about two and a half schemas a page) and has been used to carry out proofs about these which involve a significant proportion of the schemas. IST sell a commercial variant of Balzac called Zola. \footnote{The example from the report ``A Simple Demonstration of Balzac'' \cite{Collinson} has been done in HOL; see {\verb+contrib/Z/TelephoneBook.ml+} distributed with HOL88 Version 2.02.} Another approach to providing proof support for \Z\ is to encode a deductive system for it in a generic theorem prover. An example of this is the encoding of \W, a logic for \Z\ \cite{Z:Wood92}, in the 2OBJ metalogical theorem prover \cite{Z:Mart93}. This approach differs from semantic embedding in that the semantics of \Z\ is not represented in the host logic; instead proof rules are encoded directly. This has the advantage that complex rules can be immediately implemented as primitives. With semantic embedding such rules have to be embodied in procedures (e.g.~\ML\ functions) that perform inferences in an underlying logic. A single step in a logic designed specially for \Z\ (e.g.~\W) might correspond to many steps in a more primitive logic (e.g.~higher order logic). For example, the proof of {\verb"AbsThm2"} above consists of over five thousand primitive \HOL\ inferences. Currently the encoding of \W\ in 2OBJ is very inefficient and so it is not yet usable in practice. A more practical approach, not based on semantic embedding, was adopted by the \zedB\ tool \cite{Z:Neil91,Z:Neil92}. This was based on the B-Tool (which is a general-purpose symbolic manipulator not incorporating any particular logic) and enabled calculation and verification of properties of Z specifications. Facilities for schema viewing, expansions, precondition calculation, discharging of initialization and other syntactic and semantic operations were included. Unfortunately only a prototype tool which is not generally available has been produced. %%% Comment on level of embedding if you get the Neilson papers in the %%% post in time. I find it difficult to judge from the papers. %%% But Z and B are a pretty good match (both from the same %%% orginator, J-R Abrial). %%% Not based on semantic embedding [MJCG] Many \Z\ tools are under development; current information on the availability of \Z\ tools may be gleaned from the monthly message issued on the electronic newsgroup \verb"comp.specification.z" and the associated ZFORUM mailing list on \Z\ \cite{Z:Bowe93}. \section{Conclusions and future work} It turned out to be easier than expected to provide basic support for a significant subset of \Z\ in \HOL. At the time of writing only a few case studies have been conducted (the birthday book is the largest), so it is hard to evaluate the success or otherwise of the approach. Only a fragment of \Z\ is currently supported, but no major difficulties are anticipated in increasing the coverage to most of the rest of the Z toolkit. Other more complicated features of \Z\ such as schemas as types, true generic definitions and the complete facilities for free type definitions may require further thought and/or compromises. Our plan is to approach this via more case studies. Examples being considered include the simple checkpointing scheme in ZRM, the ``Word-For-Word'' example in the textbook {\it An Introduction to Formal Specification and \Z\/} \cite{Z:Pott90}, an \ML\ pattern matching refinement case study \cite{Zpatt} and the ``The Low Water Mark'' \cite{EVES:Report}. A disadvantage of our approach is that users need to be proficient with \HOL\ before they can attempt proofs in \Z. Learning \HOL\ is quite time consuming; at least one week of full-time training is needed to get started effectively. In particular, \HOL\ tactics must be mastered. However, extensive training materials for \HOL\ are available and there is a relatively large international user community. In the future it is hoped to provide support for interfacing with the widely available \LaTeX\ document preparation system for compatibility with other \Z-processing tools, such as \fuzz\ (whose \LaTeX\ style option was used to prepare this paper) and the public domain ZTC \cite{Z:ZTC}. \HOL's parser and pretty printer libraries should make this relatively straightforward. \section*{Acknowledgements} We are grateful to Jim Grundy, Terry Ireland, Roger Jones, Savitri Maharaj, Tom Melham and Mark Saaltink for reading a draft of this paper and making numerous suggestions for its improvement. Will Harwood provided information on Balzac and its use. Mike Spivey provided the Birthday Book example and the \fuzz\ tool. Jonathan Bowen is funded by the UK Science and Engineering Research Council (SERC) on grant no.\ GR/J15186. % Include all the bibliography if required: % \nocite{*} \bibliography{zhol} \bibliographystyle{wicsbook} \end{document}