\chapter{Case study}
\label{case-chap}

A suitable case study must be of a reasonable size so that
\begin{itemize}
\item The data can be prepared (to take account of issues we will
describe below)
\item The results can be comprehended
\end{itemize}

The development of a symbol table (given in \cite{San90}) is of a
suitable size. Here, we will present the results generated by the
obligation tool when analysing the first of the two developments
offered in \cite{San90}. The full development code is given in
Section~\ref{develop-code}.

We will present the results of the analysis below. First, however, it
is important to describe the ways in which the input files have to
differ from the code in \cite{San90}.

\section{Preparation}

\begin{enumerate}

\item All uses of {\tt implies} (in fact in \cite{San90} the relation
$\implies$) have had to be removed. This is because the EML front-end cannot
parse the keyword correctly. Thus A {\tt implies} B is re-written as (A
{\tt andalso} B) {\tt orelse} ({\tt not} A).

\item All structures must be annotated with their signature. e.g. 
\begin{quote}
\STRUCTURE\ X = X
\end{quote}
is corrected to
\begin{quote}
\STRUCTURE\ X:ID = X
\end{quote}

\item Some parameter identifiers require changing. In \cite{San90},
many of the functors use the same identifiers for their arguments.
This issue is only important because the functors are given in a
derived form. The derived form translation of

\begin{quote}
\funid(\spec):\sigexp = \strexp
\end{quote}
is
\begin{quote}
\funid(\strid:\SIG\ \spec\ \END):\sigexp$'$ =\\
\LET\ \OPEN\ \strid\ \IN\ \strexp\ \END
\end{quote}

where \strid\  is a unique structure identifier.

Thus, in the development, where we have

\begin{quote}
\begin{tabbing}
\FUNCTOR\ Symtab\\
\mv(\STRUCTURE\ X:ID\\
\mv \STRUCTURE\ Y:ATTRIB):\cdots\\
= ChangeAttrib(Symtab'(\=\STRUCTURE\ X:ID = X\\
\>\STRUCTURE\ Y:ATTRIB = Y))
\end{tabbing}
\end{quote}

the argument parameters X and Y are in scope when X:ID = X and
Y:ATTRIB = Y are analysed i.e. these bindings will be seen as
refinements.

We can ensure that this does not happen by choosing suitable
identifiers for the argument structures to functors.

\end{enumerate}

\section{Execution}

In the following execution, the code is read in from files and the
results written out to files. The {\tt results} variable is reset
prior to each file being read so that the obligations from each
development step can be identified.

It is important that each file may only contain a $\topdec$
declaration i.e. the same file cannot contain functor declarations and
signature declarations.

For the 5 development steps, each comprising functor and/or signature
declarations, we have files step1T.eml, step2F.eml etc.

The code for executing this case study from a session in New Jersey ML
is 

\begin{verbatim}
use "INSTALL";
 
results := empty_Os;
val synt_0T = deal_with_file("case/step0T.eml",init_A);
val results_file = open_out("case/res0T.brf");
val results_string = get_string_results(!results);
output(results_file,results_string);
close_out(results_file);

results := empty_Os;
val synt_0F = deal_with_file("case/step0F.eml",synt_0T);
val results_file = open_out("case/res0F.brf");
val results_string = get_string_results(!results);
output(results_file,results_string);
close_out(results_file);

etc.
\end{verbatim}

As we can see, the results will be produced into files called 

\begin{verbatim}
res0F.brf       res1F.brf       res2F.brf       res4F.brf
res0T.brf       res1T.brf       res3F.brf       res5F.brf
\end{verbatim}

\section{Results}

Below, we present each input file together with the obligations
generated by that step. 

Note that the obligations are not laid out in
full. In particular, the sub-structure environments are not laid out.
Also, due to a parser bug, it is unwise to lay out the bindings in
full. All identifiers are tagged with {\tt UNRES\_INFIX} constructors
and the layout function provided by the EML front end displays all of
these. The output becomes unreadable. Instead then, just enough
information is shown so that the structure might be determined.

29 obligations are yielded by the 6 real steps.
\begin{itemize}
\item step0F - no obligations
\item step1F - 7 obligations
\item step2F - 3 obligations
\item step3F - 4 obligations
\item step4F - 5 obligations
\item step5F - 10 obligations
\end{itemize}

These obligations are simplified so that all axioms appearing in the
conclusion that are syntactically identical to axioms in the premise
are removed. More consideration is required prior to removing value
and type declarations. It would seem that static analysis would have
checked that all the values and types in a specification have been
satisfied and therefore, they can be discarded. However, this is not
always the case. If a refined signature refers to a {\tt
datatype} while the original referred to a {\tt spantype}, then it is
not safe to ignore the {\tt datatype} in the conclusion. It must be
shown to satisfy the {\tt spantype}.

What we are interested in is the number of axioms that can be
discharged by syntactic matching. Of the 29 obligations generated,
just 6 have any axioms remaining in their conclusions.

\subsection{Step0T}
\subsubsection{Code}
\begin{verbatim}
signature ID =
    sig
        eqtype id
    end

signature ATTRIB =
    sig
        type attrib
        val null_attrib : attrib
    end

signature SYMTAB =
    sig
        structure Id : ID
        structure Attrib : ATTRIB
        type symtab
        val empty : symtab
        val add : Id.id * Attrib.attrib * symtab -> symtab
        val change_attrib : Id.id * Attrib.attrib * symtab -> symtab

        val present : Id.id * symtab -> bool
        axiom present(i,empty) = false
        axiom present(i,add(i',a',s)) = (i=i') orelse present(i,s)
        axiom present(i,change_attrib(i',a',s)) = present(i,s)

        val lookup : Id.id * symtab -> Attrib.attrib
        axiom lookup(i,empty) = Attrib.null_attrib
        axiom lookup(i,add(i,a,s)) = a
        axiom (i<>i' andalso (lookup(i,add(i',a',s)) = lookup(i,s)))
              orelse (not (i<>i'))
        axiom (present(i,s) andalso lookup(i,change_attrib(i,a,s)) =
              a) orelse (not present(i,s))
        axiom (i<>i' andalso lookup(i,change_attrib(i',a',s)) =
              lookup(i,s)) orelse (not (i<>i'))
    end
\end{verbatim}

This step yields no obligations but three entries into the signature environment

\subsection{step0F}
\subsubsection{Code}
\begin{verbatim}
functor Symtab
    (structure X : ID
     structure Y : ATTRIB
         ) : sig include SYMTAB
                 sharing Id = X and Attrib = Y
             end
    = ?
\end{verbatim}

This empty coding step yields no obligations but a single entry into
the functor environment

\subsection{step1T}
\subsubsection{Code}
\begin{verbatim}
signature SYMTAB' =
    sig
        structure Id : ID
        structure Attrib : ATTRIB
        type symtab
        val empty : symtab
        val add : Id.id * Attrib.attrib * symtab -> symtab

        val present : Id.id * symtab -> bool
        axiom present(i,empty) = false
        axiom present(i,add(i',a',s)) = (i=i') orelse present(i,s)

        val lookup : Id.id * symtab -> Attrib.attrib
        axiom lookup(i,empty) = Attrib.null_attrib
        axiom lookup(i,add(i,a,s)) = a
        axiom (i<>i' andalso (lookup(i,add(i',a',s)) = lookup(i,s)))
              orelse (not (i<>i'))
    end
\end{verbatim}

This step yields no obligations but an additional entry into the
signature environment.

\subsection{step1F}
\subsubsection{Code}
\begin{verbatim}
functor Symtab'
    (structure A : ID
     structure B : ATTRIB
         ) : sig include SYMTAB'
                 sharing Id = A and Attrib = B
             end
    = ?

functor ChangeAttrib
    (C : SYMTAB'
         ) : sig include SYMTAB
                 sharing Id = C.Id and Attrib = C.Attrib
             end
    = ?

functor Symtab
    (structure X : ID
     structure Y : ATTRIB
         ) : sig include SYMTAB
                 sharing Id = X and Attrib = Y
             end
    =  ChangeAttrib(Symtab'(structure A:ID = X
                            structure B:ATTRIB = Y))
\end{verbatim}

\subsubsection{Obligations}

This step, comprising two empty codings and a true coding, yields 7
obligations.

\begin{itemize}

\item Arises from fresh coding binding of A:ID = X
\begin{verbatim}
From depth : Symtab
  Premise
    struct
      eqtype
      StrEnv
    end
  Conclusion
    sig
      eqtype
      SubSigEnv
    end
\end{verbatim}

\item Arises from fresh coding binding of B:ATTRIB = Y
\begin{verbatim}
From depth : Symtab
  Premise
    struct
      type
      val
      StrEnv
    end
  Conclusion
    sig
      type
      val
      SubSigEnv
    end
\end{verbatim}

\item Arises from application of Symtab'
\begin{verbatim}
From depth : Symtab
  Premise
    struct

      StrEnv
    end
  Conclusion
    sig

      SubSigEnv
    end
\end{verbatim}

\item Arises from application of ChangeAttrib
\begin{verbatim}
From depth : Symtab
  Premise
    struct
      local
        struct

          StrEnv
        end
      in
        struct
          type
          val
          val
          val
          axiom
          axiom
          val
          axiom
          axiom
          axiom
          StrEnv
        end
      end
      StrEnv
    end
  Conclusion
    sig
      type
      val
      val
      val
      val
      SubSigEnv
    end
\end{verbatim}

\item Arises from binding of functor Symtab to ChangeAttrib(...)
\begin{verbatim}
From depth : 
  Premise
    struct
      type
      val
      val
      val
      val
      axiom
      axiom
      axiom
      val
      axiom
      axiom
      axiom
      axiom
      axiom
      StrEnv
    end
  Conclusion
    sig
      local
        sig

          SubSigEnv
        end
      in
        sig
          type
          val
          val
          val
          val
          val
          SubSigEnv
        end
      end
      SubSigEnv
    end
\end{verbatim}

\item Arises from refinement (in fact identity) of output signature of Symtab
\begin{verbatim}
From depth : 
  Premise
    sig
      local
        sig

          SubSigEnv
        end
      in
        sig
          type
          val
          val
          val
          val
          axiom
          axiom
          axiom
          val
          axiom
          axiom
          axiom
          axiom
          axiom
          SubSigEnv
        end
      end
      SubSigEnv
    end
  Conclusion
    sig
      local
        sig

          SubSigEnv
        end
      in
        sig

          SubSigEnv
        end
      end
      SubSigEnv
    end
\end{verbatim}

\item Arises from refinement (in fact identity) of input signature of Symtab
\begin{verbatim}
From depth : 
  Premise
    sig

      SubSigEnv
    end
  Conclusion
    sig

      SubSigEnv
    end
\end{verbatim}
\end{itemize}

\subsection{step2F}
\subsubsection{Code}
\begin{verbatim}
functor ChangeAttrib
    (C : SYMTAB'
         ) : sig include SYMTAB
                 sharing Id = C.Id and Attrib = C.Attrib
             end
    = struct
          open C
          fun change_attrib(i:Id.id,a:Attrib.attrib,s:symtab) = ? : symtab
          axiom (present(i,s) andalso change_attrib(i,a,s) =
                add(i,a,s)) orlese (not present(i,s))
          axiom ((not present(i,s)) andalso change_attrib(i,a,s) = s)
                orelse (present(i,s))
      end
\end{verbatim}

\subsubsection{Obligations}
This true coding step yields 3 obligations.

\begin{itemize}
\item Arises from binding of functor ChangeAttrib = struct ...
\begin{verbatim}
From depth : 
  Premise
    struct
      type
      val
      val
      val
      axiom
      axiom
      val
      axiom
      axiom
      axiom
      val
      axiom
      axiom
      StrEnv
    end
  Conclusion
    sig
      type
      val
      val
      val
      val
      axiom
      val
      axiom
      axiom
      SubSigEnv
    end
\end{verbatim}
\item Arises from refinement (in fact identity) of output signature of ChangeAttrib
\begin{verbatim}
From depth : 
  Premise
    sig
      type
      val
      val
      val
      val
      axiom
      axiom
      axiom
      val
      axiom
      axiom
      axiom
      axiom
      axiom
      SubSigEnv
    end
  Conclusion
    sig

      SubSigEnv
    end
\end{verbatim}
\item Arises from refinement (in fact identity) of input signature of ChangeAttrib
\begin{verbatim}
From depth : 
  Premise
    sig
      type
      val
      val
      val
      axiom
      axiom
      val
      axiom
      axiom
      axiom
      SubSigEnv
    end
  Conclusion
    sig

      SubSigEnv
    end
\end{verbatim}
\end{itemize}


\subsection{step3F}
\subsubsection{Code}
\begin{verbatim}
functor ChangeAttrib
    (C : SYMTAB'
         ) : sig include SYMTAB
                 sharing Id = C.Id and Attrib = C.Attrib
             end
    = struct
          open C
          fun change_attrib(i,a,s) = if present(i,s) then add(i,a,s) else s
      end
\end{verbatim}

\subsubsection{Obligations}
This refinement step yields 4 obligations.

\begin{itemize}
\item Arises from binding of functor ChangeAttrib = struct ...
\begin{verbatim}
From depth : 
  Premise
    struct
      type
      val
      val
      val
      axiom
      axiom
      val
      axiom
      axiom
      axiom
      val
      StrEnv
    end
  Conclusion
    sig
      type
      val
      val
      val
      val
      axiom
      val
      axiom
      axiom
      SubSigEnv
    end
\end{verbatim}
\item Arises from refinement (in fact identity) of output signature of ChangeAttrib
\begin{verbatim}
From depth : 
  Premise
    sig
      type
      val
      val
      val
      val
      axiom
      axiom
      axiom
      val
      axiom
      axiom
      axiom
      axiom
      axiom
      SubSigEnv
    end
  Conclusion
    sig

      SubSigEnv
    end
\end{verbatim}
\item Arises from refinement (in fact identity) of input signature of ChangeAttrib
\begin{verbatim}
From depth : 
  Premise
    sig
      type
      val
      val
      val
      axiom
      axiom
      val
      axiom
      axiom
      axiom
      SubSigEnv
    end
  Conclusion
    sig

      SubSigEnv
    end
\end{verbatim}
\item Arises from refinement of the body of ChangeAttrib
\begin{verbatim}
From depth : 
  Premise
    struct
      type
      val
      val
      val
      axiom
      axiom
      val
      axiom
      axiom
      axiom
      val
      StrEnv
    end
  Conclusion
    struct
      val
      axiom
      axiom
      StrEnv
    end
\end{verbatim}
\end{itemize}


\subsection{step4F}
\subsubsection{Code}
\begin{verbatim}
functor Symtab'
    (structure A : ID
     structure B : ATTRIB
         ) : sig include SYMTAB'
                 sharing Id = A and Attrib = B
             end
    = struct
          structure Id : ID = A
          structure Attrib : ATTRIB = B
          datatype symtab =
              empty
            | add of Id.id * Attrib.attrib * symtab

          fun present(i:Id.id,s:symtab) = ? : bool
          axiom present(i,empty) = false
          axiom present(i,add(i',a',s)) = (i=i') orelse present(i,s)

          fun lookup(i:Id.id,s:symtab) = ? : Attrib.attrib
          axiom lookup(i,empty) = Attrib.null_attrib
          axiom lookup(i,add(i,a,s)) = a
          axiom (i<>i' andalso lookup(i,add(i',a',s)) = lookup(i,s))
                orelse (not (i<>i'))
      end
\end{verbatim}

\subsubsection{Obligations}
This true coding step yields 5 obligations.

\begin{itemize}
\item Arises from fresh binding of Id:ID = A
\begin{verbatim}
From depth : Symtab'
  Premise
    struct
      eqtype
      StrEnv
    end
  Conclusion
    sig
      eqtype
      SubSigEnv
    end
\end{verbatim}
\item Arises from fresh binding of Attrib:ATTRIB = B
\begin{verbatim}
From depth : Symtab'
  Premise
    struct
      type
      val
      StrEnv
    end
  Conclusion
    sig
      type
      val
      SubSigEnv
    end
\end{verbatim}
\item Arises from binding of functor Symtab' = struct ...
\begin{verbatim}
From depth : 
  Premise
    struct
      datatype
      val
      axiom
      axiom
      val
      axiom
      axiom
      axiom
      StrEnv
    end
  Conclusion
    sig
      local
        sig

          SubSigEnv
        end
      in
        sig
          type
          val
          val
          val
          axiom
          axiom
          val
          axiom
          axiom
          axiom
          SubSigEnv
        end
      end
      SubSigEnv
    end
\end{verbatim}
\item Arises from refinement (in fact identity) of output signature of Symtab'
\begin{verbatim}
From depth : 
  Premise
    sig
      local
        sig

          SubSigEnv
        end
      in
        sig
          type
          val
          val
          val
          axiom
          axiom
          val
          axiom
          axiom
          axiom
          SubSigEnv
        end
      end
      SubSigEnv
    end
  Conclusion
    sig
      local
        sig

          SubSigEnv
        end
      in
        sig

          SubSigEnv
        end
      end
      SubSigEnv
    end
\end{verbatim}
\item Arises from refinement (in fact identity) of input signature of Symtab'
\begin{verbatim}
From depth : 
  Premise
    sig

      SubSigEnv
    end
  Conclusion
    sig

      SubSigEnv
    end
\end{verbatim}
\end{itemize}

\subsection{step5F}
\subsubsection{Code}
\begin{verbatim}

functor Symtab'
    (structure A : ID
     structure B : ATTRIB
         ) : sig include SYMTAB'
                 sharing Id = A and Attrib = B
             end
    = struct
          structure Id : ID = A
          structure Attrib : ATTRIB = B
          datatype symtab =
              empty
            | add of Id.id * Attrib.attrib * symtab

          fun present(i,empty) = false
            | present(i,add(i',a',s)) = (i=i') orelse present(i,s)

          fun lookup(i,empty) = Attrib.null_attrib
            | lookup(i,add(i',a,s)) = if i=i' then a else lookup(i,s)
      end
\end{verbatim}

\subsubsection{Obligations}
This refinement step yields 10 obligations.

\begin{itemize}
\item Arises from refinement of body of sub-structure Symtab'.Id
\begin{verbatim}
From depth : Symtab'
  Premise
    struct
      eqtype
      StrEnv
    end
  Conclusion
    struct

      StrEnv
    end
\end{verbatim}
\item Arises from refinement (in fact identity) of signature of
sub-structure Symtab'.Id
\begin{verbatim}
From depth : Symtab'
  Premise
    sig
      eqtype
      SubSigEnv
    end
  Conclusion
    sig

      SubSigEnv
    end
\end{verbatim}
\item Arises from binding of Id:ID = A
\begin{verbatim}
From depth : Symtab'
  Premise
    struct
      eqtype
      StrEnv
    end
  Conclusion
    sig
      eqtype
      SubSigEnv
    end
\end{verbatim}
\item Arises from refinement of body of sub-structure Symtab'.Attrib
\begin{verbatim}
From depth : Symtab'
  Premise
    struct
      type
      val
      StrEnv
    end
  Conclusion
    struct

      StrEnv
    end
\end{verbatim}
\item Arises from refinement (in fact identity) of signature of
sub-structure Symtab'.Attrib
\begin{verbatim}
From depth : Symtab'
  Premise
    sig
      type
      val
      SubSigEnv
    end
  Conclusion
    sig

      SubSigEnv
    end
\end{verbatim}
\item Arises from binding of Attrib:ATTRIB = B
\begin{verbatim}
From depth : Symtab'
  Premise
    struct
      type
      val
      StrEnv
    end
  Conclusion
    sig
      type
      val
      SubSigEnv
    end
\end{verbatim}
\item Arises from binding of functor Symtab' = struct ...
\begin{verbatim}
From depth : 
  Premise
    struct
      datatype
      val
      val
      StrEnv
    end
  Conclusion
    sig
      local
        sig

          SubSigEnv
        end
      in
        sig
          type
          val
          val
          val
          axiom
          axiom
          val
          axiom
          axiom
          axiom
          SubSigEnv
        end
      end
      SubSigEnv
    end
\end{verbatim}
\item Arises from refinement (in fact identity) of output signature of Symtab'
\begin{verbatim}
From depth : 
  Premise
    sig
      local
        sig

          SubSigEnv
        end
      in
        sig
          type
          val
          val
          val
          axiom
          axiom
          val
          axiom
          axiom
          axiom
          SubSigEnv
        end
      end
      SubSigEnv
    end
  Conclusion
    sig
      local
        sig

          SubSigEnv
        end
      in
        sig

          SubSigEnv
        end
      end
      SubSigEnv
    end
\end{verbatim}
\item Arises from refinement (in fact identity) of input signature of Symtab'
\begin{verbatim}
From depth : 
  Premise
    sig

      SubSigEnv
    end
  Conclusion
    sig

      SubSigEnv
    end
\end{verbatim}
\item Arises from refinement of body of Symtab'
\begin{verbatim}
From depth : 
  Premise
    struct
      datatype
      val
      val
      StrEnv
    end
  Conclusion
    struct
      val
      axiom
      axiom
      val
      axiom
      axiom
      axiom
      StrEnv
    end
\end{verbatim}
\end{itemize}



\section{Full case study code}
\label{develop-code}

\begin{verbatim}
signature ID =
    sig
        eqtype id
    end

signature ATTRIB =
    sig
        type attrib
        val null_attrib : attrib
    end

signature SYMTAB =
    sig
        structure Id : ID
        structure Attrib : ATTRIB
        type symtab
        val empty : symtab
        val add : Id.id * Attrib.attrib * symtab -> symtab
        val change_attrib : Id.id * Attrib.attrib * symtab -> symtab

        val present : Id.id * symtab -> bool
        axiom present(i,empty) = false
        axiom present(i,add(i',a',s)) = (i=i') orelse present(i,s)
        axiom present(i,change_attrib(i',a',s)) = present(i,s)

        val lookup : Id.id * symtab -> Attrib.attrib
        axiom lookup(i,empty) = Attrib.null_attrib
        axiom lookup(i,add(i,a,s)) = a
        axiom (i<>i' andalso (lookup(i,add(i',a',s)) = lookup(i,s)))
              orelse (not (i<>i'))
        axiom (present(i,s) andalso lookup(i,change_attrib(i,a,s)) =
              a) orelse (not present(i,s))
        axiom (i<>i' andalso lookup(i,change_attrib(i',a',s)) =
              lookup(i,s)) orelse (not (i<>i'))
    end

functor Symtab
    (structure X : ID
     structure Y : ATTRIB
         ) : sig include SYMTAB
                 sharing Id = X and Attrib = Y
             end
    = ?

signature SYMTAB' =
    sig
        structure Id : ID
        structure Attrib : ATTRIB
        type symtab
        val empty : symtab
        val add : Id.id * Attrib.attrib * symtab -> symtab

        val present : Id.id * symtab -> bool
        axiom present(i,empty) = false
        axiom present(i,add(i',a',s)) = (i=i') orelse present(i,s)

        val lookup : Id.id * symtab -> Attrib.attrib
        axiom lookup(i,empty) = Attrib.null_attrib
        axiom lookup(i,add(i,a,s)) = a
        axiom (i<>i' andalso (lookup(i,add(i',a',s)) = lookup(i,s)))
              orelse (not (i<>i'))
    end

functor Symtab'
    (structure A : ID
     structure B : ATTRIB
         ) : sig include SYMTAB'
                 sharing Id = A and Attrib = B
             end
    = ?

functor ChangeAttrib
    (C : SYMTAB'
         ) : sig include SYMTAB
                 sharing Id = C.Id and Attrib = C.Attrib
             end
    = ?

functor Symtab
    (structure X : ID
     structure Y : ATTRIB
         ) : sig include SYMTAB
                 sharing Id = X and Attrib = Y
             end
    =  ChangeAttrib(Symtab'(structure A:ID = X
                            structure B:ATTRIB = Y))

functor ChangeAttrib
    (C : SYMTAB'
         ) : sig include SYMTAB
                 sharing Id = C.Id and Attrib = C.Attrib
             end
    = struct
          open C
          fun change_attrib(i:Id.id,a:Attrib.attrib,s:symtab) = ? : symtab
          axiom (present(i,s) andalso change_attrib(i,a,s) =
                add(i,a,s)) orlese (not present(i,s))
          axiom ((not present(i,s)) andalso change_attrib(i,a,s) = s)
                orelse (present(i,s))
      end

functor ChangeAttrib
    (C : SYMTAB'
         ) : sig include SYMTAB
                 sharing Id = C.Id and Attrib = C.Attrib
             end
    = struct
          open C
          fun change_attrib(i,a,s) = if present(i,s) then add(i,a,s) else s
      end

functor Symtab'
    (structure A : ID
     structure B : ATTRIB
         ) : sig include SYMTAB'
                 sharing Id = A and Attrib = B
             end
    = struct
          structure Id : ID = A
          structure Attrib : ATTRIB = B
          datatype symtab =
              empty
            | add of Id.id * Attrib.attrib * symtab

          fun present(i:Id.id,s:symtab) = ? : bool
          axiom present(i,empty) = false
          axiom present(i,add(i',a',s)) = (i=i') orelse present(i,s)

          fun lookup(i:Id.id,s:symtab) = ? : Attrib.attrib
          axiom lookup(i,empty) = Attrib.null_attrib
          axiom lookup(i,add(i,a,s)) = a
          axiom (i<>i' andalso lookup(i,add(i',a',s)) = lookup(i,s))
                orelse (not (i<>i'))
      end

functor Symtab'
    (structure A : ID
     structure B : ATTRIB
         ) : sig include SYMTAB'
                 sharing Id = A and Attrib = B
             end
    = struct
          structure Id : ID = A
          structure Attrib : ATTRIB = B
          datatype symtab =
              empty
            | add of Id.id * Attrib.attrib * symtab

          fun present(i,empty) = false
            | present(i,add(i',a',s)) = (i=i') orelse present(i,s)

          fun lookup(i,empty) = Attrib.null_attrib
            | lookup(i,add(i',a,s)) = if i=i' then a else lookup(i,s)
      end
\end{verbatim}

