#! /bin/sh
# This is a shell archive.  Remove anything before this line, then unpack
# it by saving it into a file and typing "sh file".  To overwrite existing
# files, type "sh file -c".  You can also feed this as standard input via
# unshar, or by typing "sh <file", e.g..  If this archive is complete, you
# will see the following message at the end:
#		"End of shell archive."
# Contents:  adt.ops.tex
# Wrapped by pepe@cain on Sat Jun 24 10:43:32 1989
PATH=/bin:/usr/bin:/usr/ucb ; export PATH
if test -f adt.ops.tex -a "${1}" != "-c" ; then 
  echo shar: Will not over-write existing file \"adt.ops.tex\"
else
echo shar: Extracting \"adt.ops.tex\" \(43240 characters\)
sed "s/^X//" >adt.ops.tex <<'END_OF_adt.ops.tex'
X%> do TEX -latex -x %F
X
X%  ADT fundamentals
X%  Jose A. Manas
X%  dpt. ingenieria telematica
X%  etsi telecomunicacion
X
X%  jmanas@dit.upm.es
X
X\documentstyle[12pt]{article}
X
X\textwidth=16cm
X\oddsidemargin=1cm
X\evensidemargin=1cm
X\textheight=22cm
X\topmargin=0cm
X
X\parindent=0cm
X\parskip=3mm
X
X\unitlength=1mm
X
X\title  {
X        A Tutorial on ADT semantics for LOTOS users     \\
X        Part II: Operations on Types
X        }
X
X\author {
X        Jos\'e A. Ma\~nas       \\
X                                \\
X        Dept. Ingenier\'{\i}a Telem\'atica      \\
X        E.T.S.I. Telecomunicaci\'on             \\
X        Ciudad Universitaria                    \\
X        E-28040  MADRID                         \\
X        SPAIN                                   \\
X                                                \\
X        {\tt jmanas@dit.upm.es}
X        }
X
X\date {14 November, 1988}
X
X\begin{document}
X
X\maketitle
X
X\begin{flushright}
X\em
XQuis Custodiet Ipsos Custodes?          \\
XDecimus Junius Juvenalis
X\end{flushright}
X
X\begin{abstract}
XIn a LOTOS specification
Xthere are many types
Xthat are build from more basic ones.
XThe operations allowed for types are presented
Xwith plenty of examples.
X\end{abstract}
X
X\section{Introduction}
XThis tutorial intends to cover the gap between normal specifiers and
Xalgebricians.
XThe question to answer is
X
X\begin{center}
Xwhat are the abstract data types of LOTOS?
X\end{center}
X
XLOTOS syntax is used,
Xbut not introduced in detail.
XReaders are referred to the standard
X\cite{kn:is8807-88}.
XThis tutorial is dealing with semantics.
X
XThe author is not a mathematician,
Xnor an algebrician,
Xbut a plain computer scientist,
Xwith a very pragmatic interest on abstract data types.
X
XThe presentation will be straightforward,
Xintroducing only those theoretical concepts that are strictly
Xrequired.
XMany examples will be presented,
Xnot big ones,
Xbut meaningful ones.
X
XThe theory of abstract data types is not a single theory,
Xbut there are as many as ADT languages.
XWe shall concentrate on ACT ONE,
Xthe language used in LOTOS.
XWhen there are several choices,
Xthey will be briefly presented,
Xbut only the one followed by ACT ONE is carried on.
X
X\begin{center}
X\rule{10cm}{.4mm}
X\end{center}
X
XIn real specifications there will be many types.
XThese types can be combined in different forms.
XNamely,
Xrenamed,
Xcomposed,
Xextended and
Xactualized.
X
X\section{Renaming}
XIn LOTOS there is syntactic support to define morphisms.
XA new type NT may be derived from and old one OT
Xby means of a morphism
X
X\[m: OT \rightarrow NT\]
X
Xthat is written as
X
X\begin{verbatim}
X        type NT is OT renamedby
X          sortnames
X            ns  for  os
X            . . . .
X          opnnames
X            no  for  oo
X            . . . .
X          endtype
X\end{verbatim}
X
Xwhere $m$ is defined as
X
X\begin{center}
X  \begin{tabular}{ll}
X    $m (os) = ns$  &  for sorts         \\
X    $m (oo) = no$  &  for operations
X  \end{tabular}
X\end{center}
X
XThe syntax forces to preserve the functionality of the operations:
Xnumber of arguments and format (prefix, infix) is not modified;
Xjust the names are consistently changed all over the signature.
X
XLOTOS puts a requirement on these morphisms:
Xthey must be
X{\bf injective}.
XThis requirement is not very theoretical,
Xbut practical.
XLOTOS designers think that
Xit is not very sensible to write morphisms that confuse things.
XBut it may be very restrictive in certain cases\footnote{
X    For instance,
X    users cannot specify the mapping of Mod4 into Mod2,
X    (see Part I).
X    }.
XHowever,
Xthere is not much more fun with renaming.
X
X\section{Composition}
XIt is much more challenging to compose types.
XLOTOS supports two forms of composition,
Xnamely
X{\bf union} and
X{\bf ``enrichment''}\footnote{
X        We shall briefly define a propriety called enrichment,
X        so let us write the LOTOS construction within quotes.
X        }.
XUnion appears as multiple import of types,
Xas in
X
X\begin{verbatim}
X    type ... is A, B, ..., Z with ...
X\end{verbatim}
X
Xwhere types $A, B, ... Z$ are composed,
Xthat is
X
X\[A + B + ... + Z\]
X
X{\em Enrichment} appears when sorts and/or operations are introduced,
Xas in
X
X\begin{verbatim}
X    type ... is ... with
X        sorts ... opns ... eqns ...
X        endtype
X\end{verbatim}
X
XLet's start with some theoretical background.
X
X\medskip
X
XLet
X
X\[A = < S, F, E >\]
X
Xbe an algebra with sorts $S$,
Xoperations $F$ and
Xsemantics defined by (positive conditional) equations $E$.
XWe extend this algebra by adding more of everything,
X
X\[A + A' = < S + S', F + F', E + E' >\]
X
Xwhere $+$ stands for disjunctive set union
X(i.e. standard {\em or}).
XThe use of set union is interesting in actual practice.
XSuppose two types include booleans.
XIn the composition of them there will be only a single boolean,
Xas usually expected.
X
X\subsection{Consistency}
XIf in (the initial model of) algebra $A$
Xthere exist two terms $t_{1}$ and $t_{2}$
Xthat are not equal,
Xbut they become equal in (the initial model of) algebra $A+A'$,
Xthen we say the extension is {\bf inconsistent}.
X
XIn positive terms,
Xan extension is {\bf consistent} iff
X$\forall t_{1}, t_{2} \in |A|$
X
X\[E+E' \vdash t_{1} = t_{2}  \Rightarrow  E \vdash t_{1} = t_{2}\]
X
XTo be read:
Xif in $A+A'$ we can prove two terms are equal,
Xit must be provable too in the original algebra.
XConsistency means equivalence classes are not collapsed.
X
XFor instance,
Xwhen you write down types involving booleans,
Xyou must be careful that things are either true or false,
Xbut never
X
X\begin{center}
Xtrue = false
X\end{center}
X
X\subsubsection{Example}
XLet's consider natural numbers
X
X\begin{verbatim}
X        type Naturals
X          sorts  nat
X          opns   0 :     -> nat
X                 s : nat -> nat
X          endtype
X\end{verbatim}
X
Xthat we extend to have stacks of natural numbers\footnote{
X     We do not claim it is a useful stack at all.
X     But be aware that the strange equation [3]
X     is too closed to what normal specifiers write when they want a finite
X     stack:
X     something where nothing else can be added.
X     }
X
X\begin{verbatim}
X        type Inconsistent.Stack is Naturals with
X          sorts  stack
X          opns   empty :            -> stack
X                 push  : nat, stack -> stack
X                 top   :      stack -> nat
X          eqns
X[1]         top (empty) = 0 ;
X[2]         top (push (n, s)) = n ;
X[3]         push (n, s) = s;
X          endtype
X\end{verbatim}
X
XIt can be easily shown this type is an inconsistent extension of
Xnaturals:
X
X\begin{center}
X  \begin{tabular}{llr}
X    \hline
X    $[4]$  &  top (push (s (0), empty)) = s (0)  &  $[2]$   \\
X    $[5]$  &  top (empty) = s (0)                &  $[4]\leftarrow[3]$      \\
X    $[6]$  &  0 = s (0)                          &  $[5]\leftarrow[1]$      \\
X    \hline
X  \end{tabular}
X\end{center}
X
XWe can easily demonstrate that
X
X\[\forall x: nat, s(x) = 0\]
X
XALL the naturals are equal to zero.
XWe have just ONE equivalence class.
X
XHowever,
Xdon't be distressed by this terrible example.
XThere are many practical cases where it is possible to live with
Xinconsistencies.
XA bit more later on.
X
X\subsection{[Sufficient] Completeness}
XIf for some sort $s \in A$,
Xthere exist terms in $|A+A'|s$
Xfor which there is no equal term in $|A|s$,
Xthen we say the extension is {\bf incomplete}.
X
XIn positive terms,
Xan extension is {\bf complete}\footnote{
X   Some authors call it sufficiently complete.
X   We shall not make any difference.
X   }
Xiff
X
X\[\begin{array}{l}
X\forall s \in A,
X\forall t \in |A+A'|s,
X\exists t_{1} \in |A|s,
XE+E' \vdash t = t_{1}
X\end{array}\]
X
XCompleteness means that we are not inventing new equivalence classes.
X
XFor instance,
Xwhen you write down types involving booleans,
Xit is important that for every {\em t: bool}
Xyou can prove
X
X\begin{center}
X{\em t = true}    or    {\em t = false}
X\end{center}
X
X\subsubsection{Example}
XLet's now try another definition of stacks of natural numbers\footnote{
X      We do not claim it is a useful stack at all.
X      But be aware that lack of previous equation [1]
X      is too close to what normal specifiers write when ignoring errors.
X      }.
X
X\begin{verbatim}
X        type Incomplete.Stack is Naturals with
X          sorts  stack
X          opns   empty :            -> stack
X                 push  : nat, stack -> stack
X                 top   :      stack -> nat
X          eqns
X            top (push (n, s)) = n;
X          endtype
X\end{verbatim}
X
XIt can be easily shown this type is an incomplete extension of
XNaturals.
XHere you have a few new equivalence classes for sort nat
X
X\begin{center}
Xtop (empty)     \\
Xs (top (empty)) \\
Xs (s (top (empty))) \\
X\ldots
X\end{center}
X
X\subsection{Enrichment}
XWe say an extension is an {\bf enrichment}
Xiff it is consistent and complete.
X
XEnrichment means there are the same equivalence classes before and
Xafter the extension.
XNeither less, nor more.
X
X\subsubsection{Example}
XLastly, let's define a good stack of nats.
X
X\begin{verbatim}
X        type Good.Stack is Naturals with
X          sorts  stack
X          opns   empty :            -> stack
X                 push  : nat, stack -> stack
X                 top   :      stack -> nat
X          eqns
X[1]         top (empty) = 0 ;
X[2]         top (push (n, s)) = n ;
X          endtype
X\end{verbatim}
X
XIt can be shown this type is an enrichment of Naturals:
X
X\begin{enumerate}
X  \item
X    Consistency
X    \begin{enumerate}
X      \item
X        it is enough to consider sort {\em nat},
X	just because there is no other sort in Naturals.
X      \item
X        there is only one operation producing {\em nat}: {\em top}
X      \item
X        we have to prove that
X
X        $\not\exists s: stack$, $top (s) = s_{1}$ and $top (s) = s_{2}$
X
X        and  Naturals $\vdash s_{1} \not\in s_{2}$
X        \begin{enumerate}
X          \item
X            for $s = empty$,
X            $top (empty) = 0$ is unique.
X          \item
X            for $s = push (n, s)$,
X            $top (push (n, s)) = n$ is unique too.
X        \end{enumerate}
X    \end{enumerate}
X  \item
X    Completeness
X    \begin{enumerate}
X      \item
X        we have to prove that
X        $\forall t = top (s) \in nat$,
X        $\exists n: nat$ such that
X        $top (s) = n$
X        \begin{enumerate}
X          \item
X            $top (empty) = 0  \in |Naturals|nat$
X          \item
X            $top (push (n, s)) = n  \in |Naturals|nat$
X        \end{enumerate}
X    \end{enumerate}
X\end{enumerate}
X
X\subsection{Do we need enrichments?}
XLOTOS does not restrict extensions.
XSpecifiers may write inconsistent and incomplete types freely.
XIt's their full responsibility\footnote{
X     For readers surprised by such a permissiveness,
X     we must recognize that,
X     in general,
X     these proprieties are indecidable.
X     That's the true reason to allow them:
X     who sorts them out?
X     }.
XInconsistent specifications may save paper.
XFor example,
Xlet us suppose we have a very nice theory of groups.
XWe can easily go into abelian groups
X
X\begin{verbatim}
X        type Abelian.Group is Group with
X          eqns
X            x . y = y . x
X          endtype
X\end{verbatim}
X
Xwhich is clearly inconsistent,
Xbecause $a.b \not= b.a$ in group theory.
X
XIncompleteness is very often used in relation with partial algebras.
XComing back to that example of type {\em Incomplete.Stack},
Xthe peculiar equation for {\em top(empty)}
Xreflects that it is an exception.
XWe can comfortably live with incomplete types,
Xso far as we can prove (somehow)
Xthat the undesirable terms will be never produced.
XThe issue is not trivial,
Xand here we just have the room to mention it.
XWhen ADT languages are more oriented to produce working products
X(lotos is mostly devoted to algebra)
Xit is usual to introduce ``application conditions''
Xor predicates that are tested on produced terms,
Xand mut be fulfilled in order to the term to be accepted.
XIt is closely related to exception mechanisms that raise a signal
X(in Ada terms)
Xwhen the operands fail to comply with some requirement,
Xas is the case for operation $top$ on operand $empty$.
X
XTo put another example,
Xthe definition of a partial ordering relation
Xwill yield {\em TRUE}, {\em FALSE} or {\em UNKNOWN}
X(for unrelated pairs).
XIt's clearly an incomplete extension of Booleans.
X
XTo summarize,
XLOTOS allows for inconsistent and incomplete types.
XSuch types may be harmless,
Xor cause troubles.
XThat's up to the specifier.
XNevertheless,
Xit would be great having a tool to check it.
XSuch a tools,
Xare currently under study,
Xbut their applicability is quite restricted.
X
X\section{Parameterized Types: Introduction}
XReusability is a major goal of modern software engineering.
XIn order to achieve this goal,
Xit is necessary that software be broken into components
Xthat are as resuable as possible;
Xparameterization is a technique that can greatly enhance
Xthe reusability of components.
XFor example,
X{\em lists of X},
X{\em sets of X},
Xetc.
XGeneric modules also greatly ameliorate the otherwise odious need for
Xdefining abstractions whenever they are used.
XWithout some such facility,
Xstrong typing would not be tolerable in practice.
X
XBefore giving details,
Xwe shall informally introduce the concepts
Xwe are going to deal with.
XA free use of Pascal will help in fixing the wishes.
X
X\section{Parameterization: Informal Presentation}
X 
X\subsection{Just Abstraction}
XIt is typical of Pascal programmers to define LISP lists as
X
X\begin{verbatim}
X    TYPE list= record  item: integer; next: ^list  end;
X\end{verbatim}
X
XAnd then code some functions and procedures to handle these lists,
Xnamely header, tail, concatenation, etc.
X
XLOTOS uses normal ADTs for this business:
X
X\begin{verbatim}
X        type Lists is Naturals with
X          sorts  list
X          opns   nil    :            -> list
X                 _ .. _ : nat,  list -> list    (* cons   *)
X                 hd     :       list -> nat     (* car    *)
X                 tl     :       list -> list    (* cdr    *)
X                 _ ++ _ : list, list -> list    (* append *)
X          eqns
X            hd (nil) = 0 ;                      (* exception *)
X            tl (nil) = nil ;                    (* exception *)
X            hd (n .. L) = n ;
X            tl (n .. L) = L ;
X            nil ++ L = L ;
X            L ++ nil = L ;
X            (n .. L1) ++ L2 = n .. (L1 ++ L2) ;
X          endtype
X\end{verbatim}
X
XNow, the Pascal programmer wants a sorting function:
X
X\begin{verbatim}
X        function sort (L: list): list;
X          begin
X            (*  some wonderful algorithm  *)
X          end
X\end{verbatim}
X
XThe LOTOS specifier just extends the previous type:
X
X\begin{verbatim}
X        type Sorts.Nats is Lists with
X          opns
X            sort   :       list -> list
X            sorted :       list -> bool
X            in     : X,    list -> bool
X            hase   : list, list -> bool
X              (* HAs Same Elements *)
X          eqns
X[1]         hase (L, L) = true ;
X[2]         hase (L1 ++ (x .. L2),
X                  M1 ++ (x .. M2)) = hase (L1 ++ L2, M1 ++ M2) ;
X[3]         x in L1 = true,
X            x in L2 = false =>
X                hase (L1, L2) = false ;
X[4]         hase (L1, L2) = hase (L2, L1) ;
X
X[5]         x in nil = false ;
X[6]         x in (y .. L) = (x eq y) or (x in L) ;
X
X[7]         sorted (nil) = true ;
X[8]         sorted (x .. nil) = true ;
X[9]         sorted (x .. (y .. L)) = (x <= y) and sorted (y .. L) ;
X
X[10]        hase (L1, L2) = true,
X            sorted (L2)   = true =>
X                sort (L1) = L2 ;
X
X          endtype
X\end{verbatim}
X
XWhile the Pascal programmer needed a parameterized function,
Xthe LOTOS specifier uses just an extended ADT.
X
XSorting may be specified in many ways.
XWhile the Pascal programmer has to go directly for a sorting
Xalgorithm,the LOTOS specifier doen't need any:
Xhe just states the properties of sorting,
Xnamely getting something sorted.
XThe previous presentation is particularly independent of any sorting
Xalgorithm.
XThe key ideas come from prof.dr. Manfred Broy,
Xat Passau.
X
X\subsection{Parameterization}
XNow,
Xour Pascal programmer wants something better,
Xa list of anything,
Xsomething he tries to write as
X
X\begin{verbatim}
X    TYPE list (X) = record item: X; next: ^list (X) end;
X\end{verbatim}
X
Xbut the Pascal compiler shouts.
X
XNo problem for the LOTOS specifier:
X
X\begin{verbatim}
X        type Lists.of.X is
X          formalsorts  X
X          formalopns   E :  -> X        (* for error *)
X
X          sorts  list
X          opns   nil    :            -> list
X                 _ .. _ : X,    list -> list    (* cons   *)
X                 hd     :       list -> X       (* car    *)
X                 tl     :       list -> list    (* cdr    *)
X                 _ ++ _ : list, list -> list    (* append *)
X          eqns
X            hd (nil) = E ;                      (* the error *)
X            tl (nil) = nil ;
X            hd (n .. L) = n ;
X            tl (n .. L) = n ;
X            nil ++ L = L ;
X            (n .. L1) ++ L2 = n .. (L1 ++ L2) ;
X          endtype
X\end{verbatim}
X
XNow, for lists of naturals,
X
X\begin{verbatim}
X        type Lists.of.Nats is Lists.of.X
X          actualizedby Naturals using
X
X          sortnames   nat for X
X          opnnames      0 for E
X          endtype
X\end{verbatim}
X
XThe poor Pascal programmer is still alive\footnote{
X    Incredible!
X    Why didn't he yet learn LOTOS?
X    }
Xto try
X
X\begin{verbatim}
X        function sort (L: list (X),
X                       <=: function (X, X): boolean): list (X) ;
X\end{verbatim}
X
Xwhere he is trying to pass both a list of anything and a boolean
Xfunction to compare those anythings.
XOf course,
Xthe Pascal compiler shouts more and more \ldots
X
XIn the meanwhile,
Xour LOTOS specifier goes on without trouble \ldots\footnote{
X    He sings in the rain, you know.
X    }
X
X\begin{verbatim}
X        type Sorts.Lists.of.X is Lists.of.X with
X          formalsorts
X            bool
X          formalopns
X            _ <= _ : X,    X    -> bool
X            _ eq _ : X,    X    -> bool
X            true,
X            false  :            -> bool
X            _ and _,
X            _ or _ : bool, bool -> bool
X          opns
X                (* same as above in type Sorts.Nats *)
X          eqns
X                (* same as above in type Sorts.Nats *)
X          endtype
X\end{verbatim}
X
XIf you want to sort natural numbers,
Xjust instantiate it ...
X
X\begin{verbatim}
X        type Sorts.Lists.of.Nats is Sorts.Lists.of.X
X          actualizedby  Naturals using
X
X          sortnames  nat for X
X          opnnames     0 for E
X          endtype
X\end{verbatim}
X
XAgain,
Xnotice that those sorts and operations with the same names
Xdo not need to be explicitly stated.
XE.g. {\em bool for bool}.
X(We suppose Naturals include Booleans, as usual).
X
X\subsection{Interface Requirements}
XReaders may be shivering by the power of these constructions.
XWhile in poor Pascal strong type checking is good enough,
Xhere we are going far further.
XIs strong sort checking enough?
XShouldn't we ask for more security?
X
XYes, we can go further.
XNotice you can build lists of anything,
Xbut you can only sort lists of things on which a total ordering is
Xdefined.
XLOTOS permits to impose conditions on actual parameters.
XFor our case, we would like the following
X{\bf formal semantics}\footnote{
X     Semantics for the formal algebra,
X     that is,
X     restrictions to put on any potential actual algebra.
X     }
X
X\begin{verbatim}
X(*  eq must be an equality relation  *)
X[1]   a eq a = true ;      (* reflexive *)
X[2]   a eq b = b eq a ;    (* symmetric *)
X[3]   a eq b = true ,
X      b eq c = true =>
X        a eq c = true ;    (* transitive *)
X
X(*  <= must be a total ordering  *)
X[4]   a <= a = true ;      (* reflexive *)
X[5]   a <= b = true ,
X      b <= a = true =>
X        b eq a = true ;    (* antisymmetric *)
X[6]   a <= b = true ,
X      b <= c = true =>
X        a <= c = true ;    (* transitive *)
X[7]   (a <= b) or (b <= a) = true ;  (* total *)
X
X(*  true and false must be different  *)
X[8]   true <> false ;
X
X(*  and must be as expected  *)
X[9]   true and a = a ;
X[10]  false and a = false ;
X[11]  a and b = b and a ;
X
X(*  or must be as expected  *)
X[12]  true or a = true ;
X[13]  false or a = a ;
X[14]  a or b = b or a ;
X\end{verbatim}
X
XLOTOS permits to state all these conditions under the section
X\verb/formaleqns/.
XBut there is an exception:
Xonly (positive conditional) equalities are allowed.
XThus,
X[8] is not accepted.
X
XIn general ADT theory,
Xthe formal equations are needed only to {\em certify} an actual candidate
Xis acceptable.
XOnce accepted, they may be dropped.
XBut in LOTOS,
Xthese formal equations are retained as part of the result type.
XThen the discussion above about existence of an initial model for
Xalgebras specified using unequalities comes back.
XLOTOS just request (positive conditional) equalities.
X
XAs perspicacious readers did already notice
Xthe difficulty arises  when one has to prove that the conditions hold for
Xsome particular module.
XOf course,
Xthe simpler the conditions
Xthe better the chance of actually getting the proof.
XBut be ready for hard work!
X
XAutomatic theorem provers are not very good in actual practice.
XBut,
Xit is usually the case that the formal equations are 
X{\bf syntactically equal}
Xto the equations of the actual parameter.
XIn these cases,
Xthe demonstration is trivial.
XFor instance,
Xthe formal equations imposed on operations {\em and} and {\em or}.
Xare very likely to be present in the actual type Booleans.
XThat greatly simplifies life.
X
X\subsection{General Instantiation}
XWe have already done some instantiations or actualizations of
Xparameterized ADTs.
XThey were rather conventional in the sense that the result is an
Xalgebra\footnote{
X        Better say a category of algebras out of which
X        we choose the initial model.
X        }.
XBut let's go a little bit further
Xand allow actual parameters to be parameterized ADTs as well.
XFor instance,
X{\em lists of lists \ldots}
X
X\begin{verbatim}
X        type Lists.of.Lists.of.X is Lists.of.X
X          actualizedby Lists.of.X using
X
X          sortnames  list for X
X          opnnames    nil for E
X          endtype
X\end{verbatim}
X
XWe get another parameterized ADT that can be instantiated.
XFor instance,
X{\em lists of lists of natural numbers \ldots}
X
X\begin{verbatim}
X        type Lists.of.Lists.of.Nats is Lists.of.Lists.of.X
X          actualizedby Naturals using
X
X          sortnames  nat for X
X          opnnames     0 for E
X          endtype
X\end{verbatim}
X
XWhen several actualization steps are involved,
Xthe order of actualization is not relevant.
XThat is,
Xwe can as well specify
X
X\begin{verbatim}
X        type Lists.of.Lists.of.Nats is Lists.of.X
X          actualizedby Lists.of.Nats using
X
X          sortnames  list for X
X          opnnames    nil for E
X          endtype
X\end{verbatim}
X
X\subsection{Higher Order Programming}
XThis last example will not introduce new concepts,
Xbut let's put it forward to show the power of LOTOS ADTs.
X
XLISP and functional languages in general
Xclaim that they provide higher order functions.
XIn simple terms,
Xthey treat functions as first class citizens
Xthat can be passed as arguments
Xand returned as results.
XLOTOS is not a higher order language
Xand arguments to operations cannot be operations.
XBut with parameterized specifications,
Xsomething can be done.
X
XThe next example shows a classical case of higher order programming.
XIn LISP style it is expressed as
X
X\begin{verbatim}
Xmkiter= function (star, one)
X        return iter
X        where
X          iter= function (L)
X                if (L = NIL)
X                  then
X                    return one
X                  else
X                    return star (car (L), iter (cdr (L)))
X\end{verbatim}
X
XBut we have something more than in LISP:
Xwe can impose conditions on the formals ...
X
X\begin{verbatim}
X        type On.Lists is Lists.of.X with
X          formalopns
X            1     :      -> X
X            _ * _ : X, X -> X
X            _ + _ : X, X -> X
X          
X          formaleqns
X            a * 1 = a ;         (* right neutral *)
X
X          opns
X            iter  :       list -> X
X            _ & _ : list, list -> list
X
X          eqns
X            iter (nil) = 1 ;
X            iter (x .. L) = x * iter (L) ;
X
X            L & nil = L ;
X            nil & L = nil ;
X            (x1 .. L1) & (x2 .. L2) = (x1 + x2) .. (L1 & L2) ;
X\end{verbatim}
X
XThis type may be instantiated with Naturals using
X
X\begin{verbatim}
X        +  for *
X        0  for 1
X        f  for +
X\end{verbatim}
X
XThen {\em iter} adds the elements of a list.
XAnd you can count the elements as
X
X\begin{verbatim}
X    iter (L & (1 .. 1 .. 1 .. ... ))
X\end{verbatim}
X
XOr you can use
X
X\begin{verbatim}
X        + for *
X        0 for 1
X        * for +
X\end{verbatim}
X
XThen $\&$ corresponds to the internal product.
X
XIt is left as an exercise to the reader instantiating it
Xto evaluate the Pythagoras' distance.
X
X\section{Parameterization: Formal Presentation}
XIn general,
Xa LOTOS ADT will include some formal sorts $FS$,
Xsome formal operations $FF$,
Xsome formal equations $FE$,
Xsome sorts $S$,
Xsome operations $F$
Xand some equations $E$.
X
XLet's introduce some notation,
X
X\begin{center}
X  \begin{tabular}{lll}
X    $PSPEC$  &  is the parameterized ADT                        \\
X    $FA$     &  is the formal parameter   &  $= <FSIG, FE>$     \\
X    $AA$     &  is the actual parameter   &  $= <ASIG, AE>$     \\
X    $RA$     &  is the result of instantiation & $= <RSIG, RE>$
X\end{tabular}
X\end{center}
X
X\subsection{Parameterized Specifications}
XA parameterized specification is defined as a pair of algebras
X
X\[PSPEC = < FA , A >\]
X
Xwhere there is a {\em formal} and a {\em target} algebras
X
X\[FA = < FS, FF, FE >\]
X\[A = < FS + S, FF + F, FE + E >\]
X
X$FA$ states properties that actual parameters must have.
X$A$ extends the result of importing an actual
Xwith more sorts, operations and equations.
X
X\subsection{Basic Actualization}
XActualization is a total {\em morphism}
X
X\[g : FSIG \rightarrow ASIG\]
X
XTotal {\em morphism} means that every formal sort and every formal
Xoperation must be instantiated.
XLOTOS does not support the so called partial actualizations
Xwhere some formals are instantiated while others remain formal.
X
XIf the actual is a simple algebra AA,
Xthe result is defined as
X
X\[RA = < AS + g (FS) + S,
X               AF + g (FF) + F,
X               AE + g (FE) + g(E)
X             >\]
X
XNotice we write $g(E)$ because formal operations may appear in the
Xtarget part,
Xand the actualization morphism have to be applied to them.
X
XThat expression may be simplified to
X
X\[RA = < AS + S, AF + F, AE + g (FE) + g(E)>\]
X
Xbecause $g(FS)$ must be a subset of $AS$,
Xand $g(FF)$, a subset of $AF$.
X
X\[g(FSIG) \subset ASIG\]
X
XWith respect to equations,
Xthey could be dropped,
Xbut LOTOS holds them.
X(See requirement 2 below).
X
X\subsection{General Actualization}
XIn general,
Xthe actual parameter may be another parameterized ADT
X
X\[APSPEC = < < AFS, AFF, AFE >
X           < AFS + AS, AFF + AF, AFE + AE > >\]
X
Xthen the instantiation is a nice game of unions
X
X\[\begin{array}{ll}
XPSPEC (APSPEC) =  & < < AFS, AFF, AFE >                 \\
X                  &   < AFS + AS + g (FS) + S,          \\
X                  &     AFF + AF + g (FF) + F,          \\
X                  &     AFE + AE + g (FE) + g(E) > >
X\end{array}\]
X
XWith respect to requirements, 
Xsee requirement 2 below.
X
X\subsection{Nonparameterized types}
XThe types studied up to this section were not parameterized.
XThey strictly correspond to parameterized specifications
Xwith an empty formal part
X
X\[< <> , < S, F, E > >\]
X
XThey play a similar role to nullary operations:
Xsomehow they are {\em constants}.
X
X\subsection{Operations on parameterized ADTs}
XParameterized ADTs may be renamed and composed.
XWhen renamed,
Xthe morphism applies both to the formal and target parts.
X
XWhen composed,
Xthey are {\em or'ed} componentwise.
XI.e.
X
X\[\begin{array}{ll}
XPSPEC1 + PSPEC2 = & < < FS1 + FS2, FF1 + FF2, FE1 + FE2 >,      \\
X                  & < FS1 + FS2 + S1 + S2,                      \\
X                  &  FF1 + FF2 + F1 + F2,                       \\
X                  &  FE1 + FE2 + E1 + E2 > >
X\end{array}\]
X
X\subsection{Requirement 1}
XThe formal part must be a self-contained ADT.
XThat means that sorts used in $FF$ and $FE$ must belong to $FS$,
Xand operations used in $FE$ must belong to $FF$.
X
XReferring back to the example of type {\em Sorts.Lists.of.X},
Xnotice {\em bool} appears as a formal sort
Xthat will be later actualized by actual booleans.
X
X\subsection{Requirement 2}
XThe formal equations must hold for the actual parameter.
XThat is,
X$FE$ must be a consequence of $AE$
X
X\[AE  \vdash  g(FE)\]
X
Xin terms of categories,
X
X\[Alg (ASIG, AE) \subseteq Alg (ASIG, g (FE))\]
X
Xin words,
Xthe actual parameter must be a subcategory of the formal algebra after
Xmapping it to the actual signature.
X
X\begin{center}
X  \begin{picture}(0, 60)
X    \put(0, 52){\makebox(0, 0)[b]{word algebra}}
X    \put(0, 50){\line(-1, -1){20}}
X    \put(0, 50){\line( 1, -1){20}}
X    \put(0, 50){\vector(0, -1){10}}
X    \put(2, 42){\makebox(0, 0)[l]{g(FE)}}
X    \put(0, 40){\line(-1, -1){15}}
X    \put(0, 40){\line( 1, -1){15}}
X    \put(0, 40){\vector(0, -1){10}}
X    \put(2, 32){\makebox(0, 0)[l]{AE}}
X    \put(0, 30){\line(-1, -1){10}}
X    \put(0, 30){\line( 1, -1){10}}
X    \put(-20, 30){\vector( 1, -1){20}}
X    \put( 20, 30){\vector(-1, -1){20}}
X    \put(0, 8){\makebox(0, 0)[t]{bottom algebra}}
X  \end{picture}
X\end{center}
X
XWhen the actual is a parameterized ADT,
Xthen the formal equations must be guaranteed
X
X\[AFE + AE  \vdash  g(FE)\]
X
X\subsection{Persistency}
XLet's consider every sort $s$ in $AS$.
XWhen the target is added,
Xwe are adding new terms to that sort.
XAfter considering the whole set of equations $AE + g(FE) + E$,
Xthe number of equivalence classes in the sort $s$ in the result algebra
Xmay be
X
X\begin{itemize}
X  \item
X    bigger than in $AA$
X    
X    that's similar to extending an ADT incompletely;
X    we say $AA$ does not {\bf persists}
X    through actualization;
X  \item
X    smaller than in $AA$
X    
X    that's similar to extending an ADT inconsistently;
X    we say $AA$ does not {\bf persists}
X    through actualization;
X  \item
X    equal
X
X    that's similar to enriching an ADT;
X    we say $AA$ {\bf persists}
X    through actualization;
X\end{itemize}
X
XA PSPEC is {\bf persistent}
Xif for every actual algebra $AA$
Xthat have the properties required by $FE$,
Xand for every sort in $AA$,
Xthe equivalence classes of s in $AA$
Xare the same as in $RA$.
X
XUsually,
X{\em pspecs} are not persistent for every valid actual algebra,
Xbut only for some of them.
XPersistency is similar to consistency and completeness
Xbetween the actual parameter and the resultant algebra.
XThe intuition is rather natural and not too complicated,
Xbut the mathematical treatment is too large to be covered in this
Xtutorial.
X
X\subsubsection{Examples}
XType Lists.of.X is persistent over any actual because
X
X\begin{enumerate}
X  \item
X    There is no formal condition $FE$,
X    thus any actual type may be used for instantiation.
X  \item
X    The equations do not make equal any term in $X$\footnote{
X        It is not true by definition;
X        you have to prove it,
X        but the proof is very easy.
X        }.
X  \item
X    No new equivalence class is introduced in sort $X$.
X\end{enumerate}
X
XPersistency in actualizations is very similar to consistency in
Xextensions.
XFor instance,
X
X\begin{verbatim}
X        type Stack.of.X is
X          formalsorts  X
X          formalopns   E  : -> X
X          sorts  stack
X          opns   empty :            -> stack
X                 push  : nat, stack -> stack
X                 top   :      stack -> nat
X          eqns
X[1]         top (empty) = E ;
X[2]         top (push (x, s)) = x ;
X[3]         push (x, s) = s;
X          endtype
X\end{verbatim}
X
X
Xis not persistent for any actual,
Xbecause it makes every term of sort X
Xequal to E.
X
X\subsection{Do we need persistent types?}
XAs with enrichments,
Xpersistency is a nice propriety,
Xbut very often it is too restrictive.
XSo, it's reasonable that LOTOS does not require parameterized ADTs to
Xbe persistent.
XNevertheless,
Xit would be great having a tool to check it.
XSuch a tools
Xare currently under study,
Xbut its applicability seems to be quite restricted.
X
XHowever,
Xpersistency is very important when libraries of ADTs are considered.
XParameterized ADTs in libraries should be carefully documented,
Xclearly specifying the interface requirements,
Xthe class of ADTs for which they are persistent,
Xand what happens with other ADTs
Xfor which they are not persistent,
Xbut may still be useful.
X
XNobody would accept type {\em Stack.of.X}
X(as presented in the last section)
Xin the standard library.
XBut specifiers may accept a version that introduces new equivalence
Xclasses
X(something similar to the type {\em Incomplete.Stack} presented before).
XOf course,
Xspecifiers must be warned.
X
XTo summarize.
XPersistency is a nice property,
XLOTOS does not enforce it,
Xit is not easily checkable,
Xyou can live without it,
Xbut it must be clearly documented,
Xmainly for types in the standard library.
X
X\subsection{Composability}
XPersistency of PSPECS guarantees composability of actualizations.
XAn example was already shown building
X
X\begin{verbatim}
XLists.of.Lists.of.Nats = Lists.of.Lists.of.X (Naturals)
X                       = (Lists.of.X (Lists.of.X)) (Naturals)
X
X                       = Lists.of.X (Lists.of.Nats)
X                       = Lists.of.X (Lists.of.X (Naturals))
X\end{verbatim}
X
Xand both routes yield the same result.
X
X\section{The Case for LOTOS}
XMost of the use of parameterized specifications in LOTOS has been
Xalready presented.
XLet's now introduce the last details with respect to scopes,
Xin order to unsderstand the use of signatures and algebras in actual
Xspecifications. 
X
X\subsection{Requirement}
XSurprisingly,
XLOTOS requires actualization morphisms to be injective for operations.
XSo, you cannot actualize type {\em On.Lists} using $+$ both for $*$ and $+$.
XI wonder why.
X
X\subsection{Scope signatures}
XLOTOS specifications are organized in scopes that can be nested as
Xusual in block structured languages as Pascal.
XThere is a global scope that encompasses
Xfrom the specification header
Xdown to the end of the specification.
XGloal data types have this scope:
X
X\begin{verbatim}
X        specification ...
X            global data type definitions
X          behaviour
X            . . . .
X          endspec
X\end{verbatim}
X
XThere are nested scopes called definition blocks.
XThey are introduced after the behaviour key word
X(as in the previous pattern),
Xand as the body of process definitions:
X
X\begin{verbatim}
X        behaviour expression
X        where
X          local data type definitions
X\end{verbatim}
X
XWhen we refer to a sort identifier to qualify a formal parameter
X(of specification or process),
Xor in a behaviour expression,
Xwe are referring to some signature that gives the syntax of the terms
Xof that sort,
Xand to some algebra that gives the semantics of values of that sort.
X
XBut,
Xwhen there are several types with the same scope,
Xones being extensions of others,
X
X\begin{center}
X        which signature are we referring to?
X\end{center}
X
XLet's put an example ...
X
X\begin{verbatim}
X        process P ...
X            ... g ?x: SA ; BE
X
X          where
X            type A is
X              sorts  SA
X              opns    a : -> SA
X              endtype
X
X            type B is A with
X              opns    b : -> SA
X              endtype
X          endproc
X\end{verbatim}
X
Xwhere type $B$ is an incomplete extension of type $A$.
X
X\begin{center}
Xwhich are the valid values for  $x: SA$ ?
X\end{center}
X
Xthe answer is:
Xyou build a signature per scope
Xthat is the union of all the types defined in that scope\footnote{
X     Standard rules for visibility and hiding of identifiers in nested
X     scopes,
X     as in Pascal,
X     are used.
X     }.
XThat signature is used to produce ground terms for $x$.
XIn the previous example,
X
X\begin{verbatim}
X        type this.scope is
X          sorts  SA
X          opns    a : -> SA
X                  b : -> SA
X          endtype
X\end{verbatim}
X
Xand
X
X\begin{center}
X\verb/g ?x: SA ; BE/
X\end{center}
X
Xis equivalent to
X
X\begin{verbatim}
X          g !a ; BE [a/x]
X        []
X          g !b ; BE [b/x]
X\end{verbatim}
X
XThe procedure is systematic,
Xbut usually there are infinite ground terms,
Xand you cannot expand ?-experiment offers
Xin a finite piece of paper.
XBut that's only a minor trouble.
XHowever,
Xa bigger trouble rises when considering the following section.
XIn-line expansion of ground terms is not always correct.
X
X\subsection{Canonical Data Type}
XPrevious section presented the case for signatures,
Xbut we are also interested on the algebra.
X{\em
X  Which algebra are we referring to
X  when there are several types involved?
X}
XSurprisingly,
Xwe are not referring to the algebra resulting of the union of local
Xalgebras.
XLet's put another example,
X
X\begin{verbatim}
X        hide g in
X            g ?x: SA ; ...
X          |[ g ]|
X            P [g]
X        
X        where
X          type A is
X            sorts  SA
X            opns     a : -> SA
X            endtype
X
X          process P [g] ... :=
X              g !b ; ...
X            
X            where
X              type B is A with
X                opns    b : -> SA
X                endtype
X            endproc
X\end{verbatim}
X
Xwill actions on $g$ synchronize?
X
XAccording to the scope signature procedure,
Xthey would not,
Xbecause term $b$ is ignored outside process $P$,
Xand thus \verb/g ?x: Sa/ would only expand into \verb/g !a/.
XBut that's an incomplete view of the story.
XIn fact they synchronize
Xbecause LOTOS uses ONLY ONE algebra 
Xfor the WHOLE specification.
XThis single algebra is called
X{\bf canonical}
Xand results of the union of ALL the types spread along the
Xspecification.
XOf course,
Xonly non parameterized types are considered.
XParameterized ADTs were already used to build nonparameterized types.
X
X\subsection{Last comment}
XThe procedures to build scope signatures
Xand the canonical algebra
Ximply that it is
X{\bf EXTREMELY DANGEROUS}
Xto extend types incompletely or inconsistently,
Xor deal with nonpersistent parameterized ADTs.
X
XFor instance,
Ximagine you extend some type including Booleans
Xand, inadvertently, you make
X
X\begin{center}
X{\em true = false}
X\end{center}
X
XYou have destroyed Booleans everywhere!
X
XBut,
Xas already mentioned,
Xthose {\em bad} types are useful.
XThere is a systematic trick to deal with this business.
XIf you want a new type $NT$
Xthat is based on an old one $OT$,
Xand $NT$ modifies the partition of $OT$ sorts into equivalence classes,
Xand you want $OT$ to be preserved as it is,
Xthen do the extension (actualization) in two steps:
X
X\begin{verbatim}
Xfirst rename OT:
X
X        type ROT is OT renamedby
X          sortnames
X            . . . .
X          opnnames
X            . . . .
X          endtype
X\end{verbatim}
X
X\begin{verbatim}
Xthen operate on ROT:
X
X        type NT is ROT with
X            ... your nasty business goes here
X          endtype
X\end{verbatim}
X
XWhen LOTOS joins $OT + ROT + NT$,
X$NT$ destroys $ROT$,
Xbut $OT$ is not disturbed.
X
X\section{Further Readings}
XThe {\em bible} is \cite{kn:ehrig-85},
Xbut it is unreadable for beginners
Xand covers too many topics and issues currently under research.
XLanguage ACT ONE,
Xthe ancestor of LOTOS for ADTs,
Xis presented in chapter 9,
Xwith examples.
X
XFor LOTOS,
Xthe standard reference is \cite{kn:is8807-88},
Xboth for syntax and precise semantics.
XThis tutorial has not been too precise with syntax.
XIf you really intend to write data types in LOTOS,
Xhave a look at the concrete syntax.
XFor the semantics,
XI think that the only way through is letting the semantics analyser
Xcomplain till it gets through.
XThen, use a simulator till you are confident with your types.
X
X\cite{kn:broy-81} introduces the proprieties of composition
Xfrom the point of view of category theory.
X
XParameterization is subject to very intensive research.
XA good introduction with reasonable examples can be found in
X\cite{kn:goguen-85a}.
XThere is some philosophy in \cite{kn:goguen-85b}.
XIt is interesting to read \cite{kn:goguen-79}
Xwhere a working language is presented with many examples.
X
X\cite{kn:wagner-81} is more formal, but still readable.
XThis last paper was presented to a congress in \cite{kn:tatcher-82}
Xin a more formal style.
XIf the reader wants brain food,
Xhe may try \cite{kn:ehrig-81}.
XAt least there are several interesting examples.
X
X\section{Acknowledgements}
XPresentations of ADTs use to be too trivial or too complicated for
Xlaymen.
XUnderstanding the theory and putting it in simple words with examples
Xhas been a time consuming task.
XMany people have helped in discussing issues,
Xexamples,
Xpapers
Xand books.
X
XI have to acknowledge the early help of Huub van Thienen in the Twente
XUniversity of Technology\footnote{
X	   Current affiliation:
X	   Dpt. of Informatics,
X	   Faculty of Science,
X	   University of Nijmegen,
X	   The Netherlands.
X	   },
Xas well as the other members of the SEDOS Project,
Xmainly those at the Technical University of Berlin.
X
XApart from SEDOS,
XI am very thankful to the Research Center of Standard Electrica at
XMadrid,
Xfor inviting to the highly illuminating lectures of prof.dr. Manfred
XBroy from Passau.
X
XAnd last,
Xbut not least,
XI have to remind the members of the Department of Ingenier\`{\i}a Telem\'atica,
Xand the students attending to the courses on LOTOS at the ETSITM,
Xwho have stoically attended the lectures
Xand provided fruitful feedback.
X
X\begin{thebibliography}{Bolognesi, 87}
X
X\bibitem[Broy, 81]{kn:broy-81}
XM. Broy,
XC. Pair and
XM. Wirsing.
XA Systematic Study of Models of Abstract Data Types.
X1981.
X
X\bibitem[Ehrig, 81]{kn:ehrig-81}
XH. Ehrig,
XH.J. Kreowski,
XJ.W. Tatcher,
XE.G. Wagner and
XJ.B. Wright.
XParameter Passing in Algebraic Specification Languages.
XWorkshop on Program Specification,
XAarhus,
X1981.
XLNCS vol. 134,
Xpp. 322-369.
X
X\bibitem[Ehrig, 85]{kn:ehrig-85}
XH. Ehrig and
XB. Mahr.
XFundamentals of Algebraic Specification,
XPart 1.
XSpringer Verlag,
XBerlin,
X1985.
X
X\bibitem[Goguen, 85a]{kn:goguen-85a}
XJ. Goguen and
XJ. Meseguer.
XEQLOG: Equality, Types, and Generic Modules for Logic Programming.
XInt. Summer School on Advanced Prog. Technologies,
XM.F. Verdejo (ed.).
XFac. Informatica de San Sebastian, 1985.
Xpp. 1-69.
X
X\bibitem[Goguen, 85b]{kn:goguen-85b}
XJ. Goguen.
XParameterized Programming.
XInt. Summer School on Advanced Prog. Technologies,
XM.F. Verdejo (ed.).
XFac. Informatica de  San Sebastian, 1985.
Xpp. 70-121.
X
X\bibitem[Goguen, 79]{kn:goguen-79}
XJ.A. Goguen and
XJ.J. Tardo.
XAn Introduction to OBJ.
XIEEE Conf. Spec. for Reliable Software, M.I.T. April, 1979.
Xpp. 170-189.
X
X\bibitem[ISO, 88]{kn:is8807-88}
XISO - Information Processing Systems -
XOpen Systems Interconnection -
XLOTOS, A Formal Description Technique Based
Xon the Temporal Ordering of Observational Behaviour.
XIS 8807, 1988.
X
X\bibitem[Tatcher, 82]{kn:tatcher-82}
XJ. Tatcher,
XE. Wagner and
XJ.B. Wright.
XData Type Specification:
XParameterization and The Power of Specification Techniques.
XTrans. Prog. Lang. and Systems, 4(4), 1982.
Xpp. 711-732.
X
X\bibitem[Wagner, 81]{kn:wagner-81}
XE.G. Wagner.
XLecture Notes on the Algebraic Specification of Data Types.
XIBM, Thomas J. Watson Research Center,
XYorktown Heights, New York.
XRC 9203, Oct. 1981.
X\end{thebibliography}
X\end{document}
X
X%% Local Variables:
X%% mode:indented-text
X%% comment-column:60
X%% comment-start:"%"
X%% comment-end:""
X%% End:
END_OF_adt.ops.tex
if test 43240 -ne `wc -c <adt.ops.tex`; then
    echo shar: \"adt.ops.tex\" unpacked with wrong size!
fi
# end of overwriting check
fi
echo shar: End of shell archive.
exit 0
