#! /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:  intro.tex sld.tex dit-.ps
# Wrapped by pepe@cain on Mon Feb  4 16:13:55 1991
PATH=/bin:/usr/bin:/usr/ucb ; export PATH
if test -f intro.tex -a "${1}" != "-c" ; then 
  echo shar: Will not over-write existing file \"intro.tex\"
else
echo shar: Extracting \"intro.tex\" \(43895 characters\)
sed "s/^X//" >intro.tex <<'END_OF_intro.tex'
X%> do TEX -d -latex -Pil2p %F
X
X%       @(#)ADT introduction
X%       @(#)Curso de Maestria, 18 de abril de 1989
X
X%       Jose A. Manas
X%	Tomas Robles
X%       Dpt. Ingenieria Telematica
X%       ETSIT Telecomunicacion
X%       Ciudad Universitaria
X%       E-28040  Madrid
X
X%       jmanas@dit.upm.es
X%       trobles@dit.upm.es
X
X\documentstyle{article}
X\input{sld}
X
X\def\today{18 April, 1989}
X\def\package{ADT Introduction}
X
X\begin{document}
X\begin{sld}
X
X  \vspace{8cm}
X
X  \head{Informal Introduction	\\
X	to Lotos ADTs
X        }
X
X  \vfill
X
X  \begin{flushright}
X    Jos\'e A. Ma\~nas                    \\
X    Tom\'as Robles			 \\
X    Dpt. Ingenier\'{\i}a Telem\'atica    \\
X    E.T.S.I. Telecomunicaci\'on          \\
X
X    \bigskip
X
X    jmanas@dit.upm.es			\\
X    trobles@dit.upm.es
X  \end{flushright}
X
X  \bigskip
X\end{sld}
X
X\begin{text}
X\head{Informal Introduction}
X
XLotos models data by means of Abstract Data Types.
XThe language is based on Ehrig's ACT ONE system.
XThe underlying theory is that of equational models.
XThat theory implies complex semantics,
Xand complex reasoning on data terms,
Xsince the conventional methods of equational reasoning have to be
Xapplied,
Xand we run into the nuisance of theorem proving.
X
XBut usually,
Xmost data types showing up in real specifications
Xmay be accurately regarded as conventional data structures
X(as in Pascal or other programming languages)
Xwith functions and procedures to manipulate them.
XThe aim of this paper is to be present such an informal and intuitive
Xvision of data types.
X
XOther papers will present the real semantics of data types,
Xas well as the accuracy and the limits of the informal view presented
Xin the following pages.
X\end{text}
X
X\begin{sld}
X\head{The Pieces of the Game}
X
X\begin{itemize}
X\item
X  TYPES
X
X  Worlds with terms and rules.  
X\item
X  SORTS
X
X  Classes of terms.
X\item
X  OPERATIONS
X
X  Elements (constants)		\\
X  and functions to manipulate.
X\item
X  EQUATIONS
X
X  \begin{itemize}
X  \item
X    Theoretically:
X    properties to be satisfied.
X  \item
X    Practically:
X    transformation rules:	\\
X    rewrite LHS $\rightarrow$ RHS
X  \end{itemize}
X\end{itemize}
X\end{sld}
X
X\begin{text}
X\head{The Pieces of the Game}
X
XThere is NO predefined data type.
XThe universe of a Lotos specification starts completely empty.
XEven booleans,
Xthat are explicitly referred to by the language
X(e.g. guards and predicates)
Xmust be specified in each Lotos text.
XUsually,
Xusers start by bringing a few types from 
X{\sc the standard library} to save time and paper
X\begin{verbatim}
X    library
X      Boolean, Set, NaturalNumber
X    endlib
X\end{verbatim}
X\ldots but users are completely free to specify whichever data model
Xthey wish,
Xeven affecting the ``usual'' understanding of what Booleans are.
X
XData specifications are collected into \verb/type/ constructions.
XLotos types are not Pascal types,
Xbut rather a world of things and properties.
XWhile in Pascal a Boolean is a data object with some predefined
Xoperators and properties,
Xin Lotos a Boolean is a collection of objects and operations that are
Xto be defined.
XWhile in Pascal the concept of type applies just to the kind of
Xvariable we have,
Xin Lotos a type encompasses both the shape of variables and the
Xoperations and properties that apply to variables of such a shape.
X
XThere are \verb/sorts/
Xthat are classes of objects.
XThe concept of sort in Lotos corresponds to the concept of type in
XPascal. 
XExpressions are of a certain sort;
Xthere are variables of this and that sort;
Xvariables can only hold expressions of the correct sort,
Xand so on.
X
XThere are \verb/operations/.
XThese correponds to functions and procedures written in Pascal to
Xmanipulate objects.
XBy means of operations it is possible to combine objects of the same
Xor different sorts into bigger objects,
Xor establish relations between them.
X
XLastly,
Xthere are \verb/equations/ that are written as equalities on
Xexpressions of the type,
Xpossibly using variables that are universally quantified.
XEquations state that two expressions are equal.
XE.g.:
X\[
X  \forall x: nat, x + 0 = 0
X\]
X\end{text}
X
X\begin{text}
X\head{The Pieces of the Game}
X
XTheoretically,
Xequations state properties that must be satisfied by
X$[$any implementation of$]$ the objects of the type.
XThat implies applying equational reasoning to the expressions of the
Xlanguage to find out whether they are equal or not.
XUsers may run into the complexities of theorem proving,
Xwhen showing two things equal or not becomes contrived.
XEven, it may not be provable.
X
XIn actual practice,
Xusers write equations with the mental model of being writing rewrite
Xrules.
XA rewrite rule is a way of programming transformations.
XA rewrite rule consists of a Left Hand Side (LHS)
Xand a Right Hand Side (RHS).
XLotos equations are thought of as
X\[
X  LHS = RHS ;
X\]
Xand interpreted as:	\\
X{\em every expression that matches the LHS pattern,
Xshall be rewritten into the corresponding RHS scheme}.
X\[
X  LHS \Rightarrow RHS ;
X\]
X
XThe intention of rewriting is to get some kind of {\em canonical
Xform}.
XIf we succeed, then speaking about equality/unequality becomes
Xtrivial:
Xjust rewrite every term into its canonical form and see whether they
Xare identical or not.
X
X``The canonical form'' is sometimes called ``the normal form''.
XThe determinate article is meaningful:
Xthere is {\sc one} canonical form.
XIt must be such that
X\begin{enumerate}
X\item
X  it cannot be further rewritten
X\item
X  two expressions that can be proved to be equal must render the same
X  canonical form after applying as many rewrites as possible
X\end{enumerate}
X
XCanonical forms are, informally, the forms used in computer
Xprogramming to hold data.
XData are hold as arrays, records, graphs, \ldots
XAll those are (usually) direct storing of canonical forms.
XFor instance, it is unusual to keep the plus operation on integers:
Xusually we shall evaluate into an integer and just keep the result.
X
XWell, canonical forms are nice,
Xand rewriting is a simple procedure to understand.
XBut,
XMay we run into rewriting loops?
Xshall we get the canonical form after applying every possible
Xrewriting?
XIf there are several possible LHS that match,
Xis it irrelevant to apply one or other?
X
XFor a large range of practical cases the answers to these questions
Xare positive, and we may be confident with the informal
Xinterpretation of the equations.
XThere are some limits that will be analysed in a different document.
X
XAlong this document we will just see equations as rewrite rules,
Xand we will {\em believe} that this vision is correct.
X\end{text}
X
X\begin{sld}
X\head{Basic Types}
X
X\begin{verbatim}
Xtype Booleans is
X  sorts
X    bool
X  opns
X    T, F: -> bool
X    not: bool -> bool
X  eqns
X    ofsort bool
X    not (T) = F;
X    not (F) = T;
X  endtype
X
Xtype Naturals is
X  sorts
X    nat
X  opns
X    0:     -> nat
X    s: nat -> nat
X  endtype
X\end{verbatim}
X
XThe terms are
X
X$0, s(0), s(s(0)), s(s(s(0))), \ldots$
X\end{sld}
X
X\begin{text}
X\head{Basic Types}
X
XHere are a couple of basic types to show the basic syntax of Lotos to
Xdescribe types.
X
XWe have specified a type Booleans that has terms of sort bool.
XThere are a couple of well-known constants T (for true) and F (for
Xfalse),
Xand one operation on bool's that provide new bool's.
XHope the equations do not require many explanations,
Xsince Booleans use to be well known by most users.
X
XThe second type is also well known: natural numbers.
XWe are using Peano's trick to avoid specifying the nice look of arabic
Xnumerals.
XThe idea is to have a single constant for zero,
Xand all the other naturals are expressed relative to zero
Xby means of finding enough {\em successors}.
XThere are no operations on nat's (till next slide).
X
XAfter these specifications,
Xwe may have variables and expressions of sort bool and nat.
XWe may have bool expressions involving T, F and not.
XWe may have nat expressions involving 0 and s.
XThat's all we have.
X\end{text}
X
X\begin{sld}
X\head{Extension}
X
X\begin{verbatim}
Xtype Extended_Naturals is Naturals
X  opns
X    _ + _: nat, nat -> nat
X  eqns
X    forall x, y: nat
X    ofsort nat
X      x + 0 = x;
X      x + s(y) = s(x+y);
X  endtype
X\end{verbatim}
X
X\begin{eqnarray}
Xs(s(s(0))) + s(s(0)) = \\
X  & s^{3}(0) + s^{2}(0) =			\\
X  & s (s^{3}(0) + s(0)) =			\\
X  & s^{2}(s^{3}(0) + 0) =			\\
X  & s^{2}(s^{3}(0)) =				\\
X  & s^{5}(0) =				\\
Xs(s(s(s(s(0)))))
X\end{eqnarray}
X\end{sld}
X
X\begin{text}
X\head{Extension}
X
XTypes may be extended with new sorts, operations, and equations.
XAllocating new sorts provides more classes of elements in our
Xuniverse.
XProviding new operations expands the range of expressions we may have.
XImposing new equations introduces new properties,
Xnew ways of rewriting.
X
XIn the example of the slide,
Xwe have enriched the type Naturals with a plus operation
X(quite conventional, isn't it?).
XIt works on a couple of nat's and provides a new nat.
XWe are providing too a couple of equations that permit
X{\em evaluating} 
Xthe new terms that we may write now that we have got a $+$ operator.
X
XThe slide shows how to apply these equations to add 3 to 2,
Xsomething that we would usually write as
X\[ 3 + 2 = 5 \]
Xwhen using arabic digits.
X\end{text}
X
X\begin{sld}
X\head{Combination}
X
X\begin{verbatim}
Xtype stack_of_nats is Naturals, Booleans
X  sorts
X    stack
X  opns
X    empty:           -> stack
X    push: nat, stack -> stack
X    top:       stack -> nat
X    pop:       stack -> stack
X    isempty:   stack -> bool
X  eqns
X    forall x: nat, s: stack
X    ofsort nat
X      top (push (x, s)) = x;
X    ofsort stack
X      pop (push (x, s)) = s;
X    ofsort bool
X      isempty (empty) = T;
X      isempty (push (x, s)) = F;
X  endtype
X\end{verbatim}
X\end{sld}
X
X\begin{text}
X\head{Combination}
X
XTypes may be combined to build more complex types.
XWe shall ``add'' the sorts, operations and equations of each component
Xto get a richer type:
Xwe have more of each.
X
XIn the example,
Xwe combine Booleans and Naturals plus new sorts, operations and
Xequations in order to get stacks of natural numbers.
X
XWe have a new sort, stack.
XWe have a {\em seed} to create stacks: the empty stack.
XPlease, notice that this is the only operation that yields an object
Xof sort stack without using another stack as input argument.
XOn the other hand,
Xnotice that the other operations
X(push, top, pop and isempty)
Xwork on an already existing object of sort stack.
X
XThe equations state the expected properties:
Xthe top of a stack is the last element pushed onto it;
Xpopping a stack is getting the stack previous to the last pushing,
Xand finding whether s stack is empty or not consists of checking
Xwhether any element has been pushed onto it.
X\end{text}
X
X\begin{sld}
X\head{Renaming}
X
X\begin{verbatim}
Xtype Mod2 is Booleans
X  sorts
X    bit
X  opns
X    0, 1:            -> bit
X    _ + _:  bit, bit -> bit
X    _ eq _: bit, bit -> bool
X  eqns  forall b: bit
X    ofsort bit
X      0 + 0 = 0;    0 + 1 = 1;
X      1 + 0 = 1;    1 + 1 = 0;
X    ofsort bool
X      b eq b = T;
X      0 eq 1 = F; 1 eq 0 = F;
X  endtype
X
Xtype Parity is Mod2 renamedby
X  sortnames
X    parity for bit
X  opnnames
X    even   for 0
X    odd    for 1
X  endtype
X\end{verbatim}
X\end{sld}
X
X\begin{text}
X\head{Renaming}
X
XIt is often the case that types are very similar.
XFor instance, the slide presents the case of naturals module 2
X(binary arithmetic)
Xand the case of parities.
XThe only differences between these two arithmetics is that we are used
Xto different names in each world,
Xand we certainly do not want to mix things up.
X
XThe renaming facility of Lotos just permits to generate a new,
Xcompletely independent,
Xtype by changing the names of its components.
XBoth sorts and operation names may be changed.
XIf a name is not changed,
Xthe same name will be used in the new type.
X
XThere is a complicated semantics associated to renaming.
XLet's start with sort names.
XIf a sort name is renamed explicitly,
Xit becames a new thing with a new name.
XIt is not only changing the name:
Xit is actually borning a new thing.
XIt is not aliasing.
XEven a sort may be renamed to the same name,
Xand then, despite being called identically,
Xthey are different things.
X
XLastly, if a sort name is not mentioned,
Xit remains undisturbed:
Xit is still denoting the very same thing.
X
XFor the example showed in the slide.
XType Booleans provides sort \verb/bool/.
XType Mod2 has both sort \verb/bool/
X(imported from Booleans)
Xand sort \verb/bit/ directly provided.
XType Parity has both sort \verb/bool/
X(brought untouched via Mod2, still the sort provided by Booleans)
Xand sort \verb/parity/ that is a new sort,
Xdespite its similarities with \verb/bit/.
X
XWith respect to operation names,
Xthe same rules apply,
Xbut there is a new complexity:
Xif any of the arguments or the result of an operation
Xbecomes a new thing,
Xthe operation becomes a new thing too,
Xboth if it is mentioned explicitly or not.
XIn the last case
X(no explicit mentioning,
Xbut either any of its arguments or its result change)
Xthe name is the same, but there is a new operation.
X
XWith respect to the slide.
XType Booleans provide the operations \verb/{T, F, not, ...}/
Xthat remain unchanged in Mod2 and in Parity.
XThe  boolean operations in type Parity are the very same ones of
XBooleans.
XType Mod2 provides \verb/{0, 1, +, eq}/.
X\verb/0/ and \verb/1/ are explicitly renamed as
X\verb/even/ and \verb/odd/, respectively,
Xand they are new operations,
Xquite similar to those in type Mod2,
Xbut incompatible.
XOperations \verb/+/ and \verb/eq/ are not explicitly renamed,
Xbut since their arguments are renamed
X(i.e. \verb/bit -> parity/),
Xthey become new operations with the same name.
XThis a typical case for operation overloading,
Xthat is permitted in Lotos.
X
XRenaming is frequently used before extending a type.
XFor instance, if we have conventional natural numbers
Xand wish to have natural numbers modulus N,
Xrather than working on Naturals and mixing everything up,
Xwe shall create a fresh copy of Naturals,
Xand we shall extend it with the new arithmetic.
XIt is a way of protecting old type against risky games.
X\end{text}
X
X\begin{sld}
X\head{Parameterization}
X
X\begin{verbatim}
Xtype Stacks is
X  formalsorts
X    element
X  sorts
X    stack
X  opns
X    empty:               -> stack
X    push: element, stack -> stack
X    top:           stack -> element
X    pop:           stack -> stack
X  eqns
X    forall e: element, s: stack
X    ofsort element
X      top (push (e, s)) = e;
X    ofsort stack
X      pop (push (e, s)) = s;
X    endtype
X\end{verbatim}
X\end{sld}
X
X\begin{text}
X\head{Parameterization}
X
XReusability is a major goal of modern software engineering.
XIn order to achieve this goal,
Xit is necessary that software be broken into components that are as
Xreusable as possible;
Xparameterization is a technique that can greatly enhance this
Xreusability of components.
X
XTypes may be incompletely specified,
Xleaving a hole or socket for further information.
XIt is a very similar situation to procedures in programming languages:
Xwe code an algorithm referring to some formal arguments to be provided
Xlater on.
XWhen the actual arguments are provided (procedure call),
Xthe algorithm is faithfully applied to those concrete values.
XThis ``trick'' may save plenty of writing,
Xdecreasing the opportunities for making mistakes,
Xand simplifying maintenance.
X
XSockets may be left open for sorts and operations.
XThe example in the slide shows a sort socket.
XThese sockets are the interface of the generic type.
XRequirements may be imposed on this interface
Xby specifying equations that must apply to the actual parameters
Xwishing to fit into these sockets;
Xbut these concepts are better understood in a semantics frame
Xand we shall leave the details for a different document.
X
XInformally,
Xthe slide shows a
X\begin{verbatim}
X    type Stacks (element: sort) ...
X\end{verbatim}
X\end{text}
X
X\begin{sld}
X\head{Actualization}
X
X\begin{verbatim}
Xtype Stack_of_Naturals is Stacks
X  actualizedby Naturals using
X  sortnames
X    nat       for element
X    nat_stack for stack
X  endtype
X
Xtype Stack_of_Booleans is Stacks
X  actualizedby Booleans using
X  sortnames
X    bool       for element
X    bool_stack for stack
X  endtype
X\end{verbatim}
X\end{sld}
X
X\begin{text}
X\head{Actualization}
X
XParameterized types may be actualized
X(instantiated, called, \ldots, as you prefer to name it).
XThe syntax is shown in the examples and should not need any further
Xexplanation.
XTwo stacks are generated by instantiating the parameterized stack with
Xdifferent actual arguments.
XInformally it may be written as
X
X\begin{quote}
X  Stack\_of\_Naturals = Stacks (Naturals)	\\
X  Stacks\_of\_Booleans = Stacks (Booleans)
X\end{quote}
X
XActualization involves a renaming of the components of the
Xparameterized data type.
XFormal sorts and operations of the parameterized type
Xare renamed into sorts and operations of the instantiation argument.
XIt differs from renaming in that now the new names are not invented,
Xbut must correspond to names in the actual argument.
XUsually, this association is explicit,
Xbut if both the parameterized type and the instantiating type have
Xsorts or operations with identical names,
Xthe renaming may be implicit.
XThis facility just helps to save paper.
X
XThe definition of actualization in Lotos allows for an on-the-fly
Xrenaming.
XIt is not theoretically required,
Xbut it uses to be very convenient.
XSorts and operations that are not formal in the parameterized type
Xmay be renamed as in a renaming construction.
XFor instance,
Xin the slide we are renaming sort \verb/stack/ of type Stacks.
XIt uses to be convenient, since sort names cannot be overloaded.
XFor sorts and operations that are not formal,
Xthe previously shown rules for {\em renaming} apply again.
X\end{text}
X
X\begin{sld}
X\head{Data vs. Behaviour}
X
XObject Oriented programming,	\\
XA dynamic vision of data:
X
X\Large
X\begin{verbatim}
Xspecification stack [push, top, pop] : noexit
X
Xtype Elements is
X  sorts
X    element
X  endtype
X
Xbehaviour
X  E_stack [push, top, pop]
X
Xwhere
X  process E_stack [push, top, pop] : noexit :=
X    push ?e: element ; D_stack [push, top, pop] (e)
X    >>
X    E_stack [push, top, pop]
X    endproc
X
X  process D_stack [push, top, pop] (e: element) : exit :=
X      top !e ; D_stack [push, top, pop] (e)
X    []
X      pop ; exit
X    []
X      ( push ?n: element ; D_stack [push, top, pop] (n)
X      >>
X        D_stack [push, top, pop] (e)   )
X    endproc
Xendspec    
X\end{verbatim}
X\end{sld}
X
X\begin{text}
X\head{Data vs. Behaviour}
X
XMost programmers are used to see their programs as collections of
Xvariables that hold different values along the execution of the
Xprogram.
XFor instance,
Xwe have a stack assigned to a variable,
Xand we push and pop things to and from this stack
Xin a dynamic manner:
Xpushing is an action, something that happens just now,
Xafter this and before that.
XThe variable holds the current state of the stack,
Xand we can act on this state step by step.
X
XLotos has a behaviour part just to specify states
Xand saying when, why and how an object transits from one state to
Xanother.
XThen a question rises,
Xcould we specify a stack as a transition machine rather than as a data
Xtype?
XAn the answer is a full yes.
X
XIn fact, this not a revolutionary idea.
XFor a long time there has existed something called ``object
Xprogramming'' supporting that idea:
Xa program is a collection of objects holding its own state.
XThese objects may be excited by sending data to them,
Xor querying,
Xand the object will keep its own history
Xto react accordingly to the past.
X
XIt is straightforward to port this idea into Lotos,
Xand write an specification that accepts pushing, topping and popping,
Xand internally holds its history about the number and order of pushes,
X\ldots
XThe example deserves detailed study that is left as an exercise to the
Xreaders: get convinced that it specifies a conventional stack!
X
XEven more,
Xwould you be able to extend the specification to support an
X``isempty'' test?
X
XThere are some pros in specifying the dynamic behaviour of a stack.
XWhile in the data type we didn't know what to do with nasty things as
X\begin{center}
X  top (empty)		\\
X  pop (empty)
X\end{center}
Xand we couldn't stop this expressions to be written;
Xnow we just don't accept these operations on empty stacks
X(\verb/E_stack/).
XIf the environment insists in popping from an empty stack,
Xit will deadlock.
X
XError treatment is never definite,
Xand there are always users and/or situations where other kinds of
Xreactions are preferred.
XThe example just shows a reaction (deadlocking) that may be useful in
Xcertain circumstances.
XFeel free to specify other behaviours!
X\end{text}
X
X\begin{sld}
X\head{Writing Equations}
X
X\begin{enumerate}
X\item
X  choose set of constructors:			\\
X  constants and argument dependent
X\item
X  write rewrite rules for non-constructors	\\
X  such that
X  \begin{itemize}
X  \item
X    non-const are applied to every combination of constructors
X  \item
X    complex $\rightarrow$ simple
X  \item
X    $[$ recursive $]$ reduction to constructors
X  \end{itemize}
X\end{enumerate}
X
XThe overall objective is to have rules to transform every possible
Xexpression into a simpler expression consisting of constructors. 
X\end{sld}
X
X\begin{text}
X\head{Writing Equations}
X
XWhen users start using Lotos,
Xthere seem to be a generalized sensation of {\em missing ground}.
X
X\begin{quote}
X``Ok, I choose a meaningful name for my type,
XI know the sorts my specification is to deal with,
XI know the operations I need.
XThat's all clear.
XI know too the syntax to write equations,
Xbut which equations shall I write?
XWhich criteria shall I use to write what?''
X\end{quote}
X
XIt is really a discouraging sensation.
X
XThe most pragmatical reaction to this should be behaving in a similar
Xway to conventional programming:
Xlet's put down a collection of procedures/functions,
Xand let's play with it.
XSurely we'll have to refine it a little bit.
X
XFor Lotos, the first rule is ``don't pretend to be the best one on the
Xearth!''
XOnce you have accepted yourself as a plain mortal,
Xjust try to write something that is understandable and works:
Xfuture readers of your text will be very grateful.
X
XThe first step is to mark apart operations that are constants.
XUsually you will not rewrite constants into any other thing,
Xbut there are some cases were you will
X(e.g. $2 = s(s(0));$).
XYou must choose those constants that you don't plan to rewrite and
Xmark them as {\em constructors}.
XThey will be used to construct canonical terms.
X
XThen you must choose a number of operations as {\em constructors} too.
XThey will be used to construct canonical terms.
X
XThe other operations,
Xthose that are not constructors,
Xmust be reducible to only constructors.
XTherefore we must write enough equations to cover all the possible
Xcases of applying non-constructors.
XThere are many ways:
Xconsidering every possible combination of constructors as arguments to
Xnon-constructors;
Xtransforming complex expressions into simpler ones;
Xrecursively reducing non-constructors by means of extracting inner
Xconstructors till we come to a simplification rules;
Xand a number of other methods well known of programming.
X\end{text}
X
X\begin{sld}
X\head{Constructors}
X
XConstructors are a subset of the operations in a type,
Xsuch that any term on the type
Xmay be expressed using only constructors and constants.
X
X\LARGE
X\begin{verbatim}
Xtype Fibonacci is Naturals
X  opns
X    _ + _: nat, nat -> nat
X    fib:        nat -> nat
X  eqns
X    forall x, y: nat
X    ofsort nat
X      x + 0 = x;
X      x + s(y) = s(x+y);
X      
X      fib (0) = 0;
X      fib (s (0)) = s (0);
X      fib (s (s (x))) = fib (x) + fib (s (x));
X  endtype
X\end{verbatim}
X
X\huge
XHere the constructors are $0, s$.
X\end{sld}
X
X\begin{text}
X\head{Constructors}
X
XThe set of constructors is arbitrary,
Xbut usually it is pretty obvious which are the constructors.
XIf not the only one,
Xit is usually straightforward to find a correct set.
X
XIn the example in the slide,
Xwe are using $0$ and $s$ as constructors.
X
XThe operation $+$ is reduced by extracting successors
Xtill we reach the simplification rule $x+0=x$.
XAn example was shown a few slides above.
X
XThe operation {\em fib} works by extracting operation $+$
Xtill we come to the simplification rules for fib.
XSince we already know how to translate $+$ into constructors,
Xthe set is sufficient.
X\end{text}
X
X\begin{sld}
X\head{Canonical Form Evaluation}
X
X\begin{verbatim}
Xtype Greatest_Common_Divisor is
X  Naturals, Booleans
X  opns
X    _ < _ : nat, nat -> bool
X    _ - _ : nat, nat -> nat
X    gcd:    nat, nat -> nat
X  eqns
X    forall x, y: nat
X    ofsort bool
X      0 < s(x) = T;
X      x < 0 = F;
X      s(x) < s(y) = x < y;
X
X    ofsort nat
X      x - 0 = x;
X      s(x) - s(y) = x - y;
X
X      gcd (x, x) = x;
X      x < y = T =>
X        gcd (x, y) = gcd (x, y - x);
X      y < x = T =>
X        gcd (x, y) = gcd (x - y, y);
X  endtype
X\end{verbatim}
X\end{sld}
X
X\begin{text}
X\head{Canonical Form Evaluation}
X
XThis example shows a few operations on Natural Numbers.
XThere is a comparision operation yielding a Boolean;
Xa subtraction operation yielding a new Natural,
Xand an operation to evaluate the greatest common divisor
Xfollowing a very classical algorithm.
X
XThe comparision operation ($<$) looks simple:
X$0$ is smaller than any successor;
Xthere is nothing smaller than $0$
X(not even $0$ itself!).
XThose are the simplification rules.
XThere is one more rule to recursively reduce any expression involving
X$<$ into an expression where one of the operands of $<$ is $0$.
XWhen this is achieved, one of the simplification rules may be applied.
X
XThe subtraction operation is a little bit trickier.
XSince we are playing with Naturals, 
Xthere is nothing below $0$.
XTherefore we only have one simplification rule
X($x-0=x;$).
XRepeated application of the reduction rule may yield a zero either for
Xthe right operand
X(then the simplification rule is applied),
Xor to the left operand.
XIn this last case ($0-x$)
Xthere is no further rule we can apply
Xand that form stands for the canonical form
X(somehow, we have invented {\em negative numbers}).
XThis kind of terms mean that there are three constructors,
Xnamely $0$, $s$ and $-$.
X
XNevertheless, there is something contradictory about {\em negative
Xnatural numbers}.
XThe specification should be further refined,
Xperhaps some kind of exception being raised when we attempt to
Xsubtract below $0$.
XBut Lotos doesn't support partial functions, nor exceptions.
XThat's most we can do.
X
XLastly,
Xthe {\sc gcd} operation {\em evaluates} the greatest common divisor of
Xtwo numbers.
XWe are using conditional equations,
Xwhich meaning should be obvious:
Xthe rule can be applied if and only if the condition holds.
XRather than explaining the rules in detail,
Xlet's present the same algorithm using the programming language C.
XIt is left as an exercise to serious readers to convince themselves of
Xthe correctness of the Lotos specification.
XGood luck!
X
XHere follow a couple of versions of {\sc gcd} in C:
X
X\begin{verbatim}
X    int gcd (x, y)                int gcd (x, y)
X      x, y: int;                    x, y: int;
X    {                             {
X      if (x == y)                   while (x != y)
X        return x;
X      if (x < y)                      if (x < y)
X        return gcd (x, y-x);            y= y-x;
X      if (y < x)                      else
X        return gcd (x-y, y);            x= x-y;
X                                    return x;
X    }                             }
X\end{verbatim}
X\end{text}
X
X\begin{sld}
X\head{Choosing Constructors}
X
XThe user may choose the constructors:
X
X\Large
X\begin{verbatim}
X(*  constructors: nil, ~  *)
Xtype Lisp_lists is
X  sorts
X    elt, list
X  opns
X    nil:               -> list
X    unit:   elt        -> list
X    _ ~ _ : elt,  list -> list
X    _ + _ : list, list -> list
X  eqns
X    forall e: elt, l1, l2: list
X    ofsort list
X      unit (e) = e ~ nil;
X      (e ~ l1) + l2 = e ~ (l1 + l2);
X      nil + l2 = l2;
X  endtype
X\end{verbatim}
X
X
X\begin{verbatim}
X(*  constructors: nil, unit, +  *)
X  ....
X  eqns
X    forall e: elt, l1, l2: list
X    ofsort list
X      nil + l2 = l2;
X      e ~ l2 = unit (e) + l2;
X      unit (e) + nil = unit (e);
X      (unit (e) + l1) + l2 = unit (e) + (l1 + l2);
X\end{verbatim}
X\end{sld}
X
X\begin{text}
X\head{Choosing Constructors}
X
XThe set of constructors is arbitrary.
XThe example shows two possible selections of constructors for Lisp
Xlists.
XThe first case is the ``natural'' one:
Xusing {\em nil} and \verb/~/ (cons for lispers).
XCanonical terms are of the form
X\begin{verbatim}
X  (e1 ~ (e2 ~ (e3 ~ nil)))
X\end{verbatim}
X
XThat is the usual representation of objects in lisp systems,
Xwhere a simplified notation is often preferred by Lisp pretty printers
X\begin{verbatim}
X  (e1 e2 e3)
X\end{verbatim}
X
XThe append function ($+$) is reduced to constructors by extracting \verb/~/
Xand applying the simplification $nil+l2=l2$.
X
XThe second set of equations uses a different set of constructors.
Xhere we have choose {\em nil}, {\em unit} and $+$
X(append for lispers)
Xas constructors.
XNow canonical terms are represented as
X\begin{verbatim}
X  unit(e1) + (unit(e2) + unit(e3))
X\end{verbatim}
X
XNotice the existence of a ``right association'' rule for $+$.
XIt is required by the symmetric nature of the append operation:
Xwe need to choose a normal form to represent chains of appends.
XTherefore, we shall rewrite
X\begin{verbatim}
X  (unit(e1) + unit(e2)) + unit(e3) -> unit(e1) + (unit(e2) + unit(e3))
X\end{verbatim}
X
XBoth constructor sets are equally good.
XIt is up to other considerations
X(probably the personal feelings of the specifier)
Xto choose one or the other.
X\end{text}
X
X\begin{sld}
X\head{How Many Equations?}
X
X\begin{itemize}
X\item
X  This is not a match!
X\item
X  Write as many as to be confident!
X\item
X  State straightforward rules!
X\item
X  There are theories		\\
X  $[$and some tools$]$		\\
X  to check whether \ldots
X  \begin{itemize}
X  \item
X    \ldots they are consistent
X  \item
X    \ldots they are redundant
X  \item
X    \ldots they are incomplete
X  \end{itemize}
X\end{itemize}
X\end{sld}
X
X\begin{text}
X\head{How Many Equations?}
X
XReal specifiers have a second reason for headaches:
Xhow many equations shall I write?
XAre there enough?
XAre there too many?
XAre consistent the ones that are?
X
XOnce again, the first rule is taking it easy:
Xdon't waste your time trying to win a price!
XNobody is paying you a dollar more for saving one equation!
X
XWriting too many equations should not be a problem,
Xnor cause any problem,
Xunless you write inconsistent properties.
XFor instance, it would be rather strange to find the following equations:
X\begin{verbatim}
X  eqns
X    x + 0 = x;
X    x + 0 = 0;
X\end{verbatim}
X
XEquations must be written in the very same terms that you are thinking
Xof the property.
XDo not contrive it unnecessarily!
XDon't write equations that you cannot even remember what you meant
Xafter a month!
X
XSure there are subtle faults that may snake into your equations and
Xcause problems.
XProgrammers are used to debugging: debug your specification!
XNever pretend that you finished when you wrote the last line:
Xfun starts now that nothing behaves as expected.
XUse of a simulator o any compiling tools is very advisable to be
Xconfident with what you wrote.
X
XExperimenting lets you be confident.
XIf you find an error, you have to correct it;
Xbut experimenting will never tell you that there are no more errors.
X
XThere are theoretical tools that help in proving completeness and
Xconsistency of the equational theory behind your naif equations.
XTry to use these tools to be more confident,
Xbut do not expect definite answres for everything:
Xthey may find some properties undecidable!
X
XReal life is hard for specifiers.
XIs it the reason for so many specifications going around the world
Xwithout even having gone through a syntax checking?
X\end{text}
X
X\begin{sld}
X\head{Operations Classification}
X
XOperations may be $[$informally$]$ classified as
X\begin{itemize}
X\item
X  constants	\\
X  eg: empty, $0$, nil
X\item
X  aggregate builders	\\
X  eg: push, s, \verb/~/, unit
X\item
X  expression builders	\\
X  eg: $+$, $+$
X\item
X  extractors	\\
X  eg: top, pop
X\item
X  testers	\\
X  eg: isempty, $<$
X\end{itemize}
X\end{sld}
X
X\begin{text}
X\head{Operations Classification}
X
XAlthough not very relevant,
Xthere is some terminology around that helps in structuring
Xspecifications
Xand in sharing information with other people.
XPlease notice that this classification is only for human convenience,
Xeven the definitions given below are rather vague,
Xand sometimes it is hard to say the role of a certain operation.
X
X{\bf Constants}	\\
Xare those operations that do not have arguments.
XSometimes they are called ``nullary operators''.
X
X{\bf Aggregate Builders}	\\
Xare those operations that take several objects of different types and
Xbuild a bigger object out of which those composing objects can be
Xextracted again.
XThese operations build aggregates.
X
X{\bf Expression Builders}	\\
XSome operations are only useful to write expressions.
XThey combine subexpressions,
Xbut recovering the history is quite impossible.
XFor instance, arithmetical operations on integers:
X\[
X  3+2 = 4+1 = 5+0 = 2+3 = 1+4 = 0+5 = \ldots
X\]
X
X{\bf Extractors}	\\
Xoperate against aggregate builders,
Xrecovering the composing objects.
X
X{\bf Testers}	\\
Xare operations yielding boolean values.
XThey can either work on a single term to reflect properties of it
X(e.g.: isempty),
Xor work on a number of terms to reflect relationships
X(e.g.: $<$).
X\end{text}
X
X\begin{sld}
X\head{Auxiliary Operations}
X
X\Large
X\begin{verbatim}
Xtype Vowels is Booleans
X  sorts
X    vowel
X  opns
X    a, e, y, o, u:      -> vowel
X    _ # _: vowel, vowel -> bool
X  eqns
X    forall v: vowel
X    ofsort bool
X    v # v = T;
X
X    a # a = T; a # e = F; a # y = F; a # o = F; a # u = F;
X    e # a = F; e # e = T; e # y = F; e # o = F; e # u = F;
X    y # a = F; y # e = F; y # y = T; y # o = F; y # u = F;
X    o # a = F; o # e = F; o # y = F; o # o = T; o # u = F;
X    u # a = F; u # e = F; u # y = F; u # o = F; u # u = T;
X  endtype
X
X  
X  opns
X    map: vowel -> nat
X  eqns
X    forall v1, v2: vowel
X    ofsort nat
X      map (a) = 0;
X      map (e) = s (map (a));
X      map (y) = s (map (e));
X      map (o) = s (map (y));
X      map (u) = s (map (o));
X    ofsort bool
X      v1 # v2 = map (v1) nat_eq map (v2);
X\end{verbatim}
X\end{sld}
X
X\begin{text}
X\head{Auxiliary Operations}
X
XDespite the previous classification,
Xthere are still unclassifiable operations that users happen to write.
X
XA very typical wish of theoretic people,
Xgreenhorns,
Xand price winners,
Xis to minimize the number of objects.
XIt may be a nice entertainment,
Xbut sometimes there are properties that cannot be stated in a finite
Xpiece of paper.
X
XThe slide shows a typical situation where we have a collection of
Xobjects and we want to define an equality relation between them.
XIt is rather easy to express that everything is equal to itself
X\[
X  v \# v = T;
X\]
Xbut it is harder to express that everything is unequal of any other
Xthing.
XIn this case, the piece of paper is not so big,
Xbut imagine the whole alphabet.
XYou need $n^{2}$ equations.
XAnd there are worse cases where the amount of required paper is
Xinfinite.
X
XThere are paper saving solutions if you accept to introduce auxiliary
Xfunctions, functions that do not mean anything for the type,
Xbut that help in stating properties.
X
XThe example shows a mapping function.
XIt associates a different natural number to each vowel,
Xand then uses the equality for natural numbers 
X(that is usually defined)
Xto check the equality of vowels.
X
XSince these kind of operations are very usual,
Xsome languages support {\em hidden operations}.
XA hidden operation is something that exists only within the type,
Xand can therefore be used to write equations in a confortable manner;
Xbut is not provided to users of the type.
XWith this facility you can simplify the specification of the type
Xwithout introducing garbage into the rest of the specification.
X
XIt is a pity, but Lotos cannot hide any operation.
XAuxiliary functions may exist, and they are visible everywhere.
X\end{text}
X
X\begin{sld}
X\head{Equality and Metaequality}
X
XPredefined equality inferred from equations: $=$
X\[
X  exp = exp =>
X\]
X
XUser specified equalities without interference.
X
X\Large
X\begin{verbatim}
Xtype Nats_Mod2 is Booleans
X  sorts
X    nat
X  opns
X    0:                -> bool
X    s:            nat -> bool
X    _ eq  _: nat, nat -> bool
X    _ eq2 _: nat, nat -> bool
X  eqns
X    forall x, y: nat
X    ofsort bool
X      x eq x = T;
X      s(x) eq 0 = F;
X      0 eq s(x) = F;
X      s(x) eq s(y) = x eq y;
X
X      x eq2 x = T;
X      x eq2 s(s(y)) = x eq2 y;
X      s(s(x)) eq2 y = x eq2 y;
X      0 eq2 s(0) = F;
X      s(0) eq2 0 = F;
X  endtype
X
X
Xa eq b = true =>    a eq b =>       not (a eq b) =>
Xa eq2 b = true =>   a eq2 b =>      not (a eq2 b) =>
X\end{verbatim}
X\end{sld}
X
X\begin{text}
X\head{Equality and Metaequality}
X
XFor every sort,
Xthere is a predefined equality
X(denoted by the reserved symbol $=$)
Xthat says whether two terms can be proved equal according to the
Xequations.
XThis equality may be used in guards and predicates
X
X\begin{verbatim}
X  term1 = term2 => ...
X\end{verbatim}
X
XSurprisingly,
Xthere is no way to check for unequality
X(in other words, there is no predefined $\not=$).
XThis is a reminiscent of the theoretic background of the language.
XEquational reasoning may yield a positive result when it succeeds in
Xproving two things equal.
XBut we can spend years trying to find two things equal,
Xand still be looking for a demonstration.
XSometimes we may come out with a proof of unequality.
XBut there are cases were nothing can be said.
XTherefore Lotos is very conservative and declines deciding.
X
XApart from that implicit equality,
Xusers may define their own equalities.
XThese are nothing more that user operations that yield a boolean
Xvalue.
XThe specifier will provide enough equations to get a T or a F.
XThe example shows a type with a couple of such equalities:
Xnormal equality for naturals, and modulus 2 equality.
XNotice there are different properties for each of them.
X
XLotos permits the use of these user defined equalities in guards
X\begin{verbatim}
X  term1 eq term2 = true => ...
X  term1 eq term2        => ...
X\end{verbatim}
Xwhere both guards having the same meaning,
Xthat is, the reference to ``true'' may be left implicit.
X
XObviously, we can here apply all the power of Booleans,
Xand check for equality, negate it, compose predicates, and so on.
X\end{text}
X
X\begin{sld}
X\head{Partial Functions and Errors}
X
XLotos ADTs are total.
X
XThere are no facilities to handle errors.
X
X\Large
X\begin{verbatim}
Xtype stack_of_nats is Naturals
X  sorts
X    stack
X  opns
X    empty:           -> stack
X    push: nat, stack -> stack
X    top:       stack -> nat
X    pop:       stack -> stack
X    error:           -> nat
X    error:           -> stack
X  eqns
X    forall x: nat, s: stack
X    ofsort nat
X      top (push (x, s)) = x;
X    ofsort stack
X      pop (push (x, s)) = s;
X    ofsort nat
X      top (empty) = error;
X      top (error) = error;
X    ofsort stack
X      pop (empty) = error;
X      pop (error) = error;
X      push (x, error) = error;
X  endtype
X\end{verbatim}
X\end{sld}
X
X\begin{text}
X\head{Partial Functions and Errors}
X
XLotos doesn't support partial functions.
XPartial functions are functions whose arguments are restricted.
XThere are many cases where partial functions model accurately the
Xreality.
XWe found an example while specifying stacks, where expressions as
X\begin{center}
X{\em top (empty)}
X\end{center}
Xare not expected.
XThe bahavioural specification of stacks was a way of modelling a
Xpartial function: some arguments are not accepted.
XOther languages permit to associate predicates on the actual
Xarguments,
Xand raise exceptions when these predicates are violated.
X
XAs far as Lotos operations are concerned,
Xthere is no way of restricting the arguments to operations.
XTherefore we'll get nice $[$pseudo$]$natural numbers as 
X\begin{center}
X{\em top (empty)}
X\end{center}
Xand nice $[$pseudo$]$stacks as
X\begin{center}
X{\em pop (empty)}
X\end{center}
Xand plenty of derivatives as
X\begin{center}
X{\em push (top (empty), pop (empty))}.
X\end{center}
XA big pile of garbage!
X
XSome users make attempts to include errors in the specification of the
Xtype. The slide shows a rather typical approach,
Xalthough there are as many solutions as specifiers.
XThe example defines an error for naturals and an error for Stacks;
Xgenerates this error upon unexpected operations,
Xand tries to collapse any term involving an error into a plain error.
XOne never knows where to end writing cases.
XFor instance,
Xwould you add an equation as the following?
X\begin{verbatim}
X  ofsort stack
X    push (error, s) = error;
X\end{verbatim}
X
XEven harder,
Xnotice that we have added an error term to Naturals.
XWhat shall we do with the operations already defined for naturals?
XFor instance, what does it mean ({\em x + error})?
X\end{text}
X
X\begin{sld}
X\head{Review}
X
X\begin{itemize}
X\item
X  basic types
X\item
X  extension
X\item
X  composition
X\item
X  parameterization/actualization
X\item
X  data vs. behaviour
X\item
X  hints to write equations
X\item
X  the roles of operations
X\item
X  auxiliary operations
X\item
X  equalities and equalities
X\item
X  partial functions and errors
X\end{itemize}
X\end{sld}
X
X\begin{text}
X\head{Phrases}
X
XReal programmers don't write specifications
X-- users should consider themselves lucky to get any programs at all
Xand take what they're given.
X
XReal programmers don't comment their code.
XIt was hard to write,
Xit should be hard to understand.
X
XReal programmers don't document.
XDocumentation is for wimps who can't read the listings of the object
Xcode.
X
XReal programmers don't worry about type checking.
XStrong type checking is for people with weak memories.
X
XReal programmers explain their work (if ever)
Xto their managers in baby-talk so they will understand it.
X
XReal programmers know what the users need better than the users do.
X
XReal programmers know that user friendly designs require only the
Xapplication of common sense.
XBesides, no one cares about users.
XPrograms are written for aesthetic beauty.
X
XReal software engineers don't comment their code.
XThe identifiers are so mnemonic that they don't need to.
X
XReal software engineers don't debug programs;
Xthey verify correctness.
XThis process need not necessarily involve executing anything on a
Xcomputer,
Xexcept perhaps a Correctness Verification Aid Program.
X
XReal software engineers like C's structured constants,
Xbut they are suspicious of it because they have heard it lets you get
X``close to the machine''.
X
XReal software engineers write in languages that have not actually been
Ximplemented for any machine,
Xand for which only the formal spec (in BNF) is available.
XThis keeps them from having to take any machine dependencies into
Xaccount.
XMachine dependencies make real software engineers very uneasy.
X
XReal computer scientists don't write the user interface;
Xthery merely argue over what they should look like.
X
XReal computer scientists don't program in assembler.
XThey don't write in anything less portable than an HB pencil.
X
XReal computer scientists admire Ada for its overwhelming aesthetic
Xvalue,
Xbut they find it difficult to actually program in,
Xas it is much too large to implement.
XMost real computer scientists don't notice this because they are still
Xarguing over what else to add to Ada.
X
XReal computer scientists only write specs for languages that might run
Xon future hardware.
XNobody trusts them to write specs for anything Homo Sapiens will ever
Xbe able to fit on a single planet.
X
XReal computer scientists love the concept of users.
XUsers are always real impressed by the stuff real computer scientists
Xare talking about;
Xit sure sounds better than the stuff they are being forced to use now.
X\end{text}
X\end{document}
X
X\begin{sld}
X\head{}
X\end{sld}
X
X\begin{text}
X\head{}
X\end{text}
X
X\begin{center}
X\end{center}
X
X\begin{verbatim}
X\end{verbatim}
X
X\begin{itemize}
X\item
X\end{itemize}
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){\vector(0, -1){10}}
X  \end{picture}
X\end{center}
X
X%% Local Variables:
X%% mode:indented-text
X%% 
END_OF_intro.tex
if test 43895 -ne `wc -c <intro.tex`; then
    echo shar: \"intro.tex\" unpacked with wrong size!
fi
# end of overwriting check
fi
if test -f sld.tex -a "${1}" != "-c" ; then 
  echo shar: Will not over-write existing file \"sld.tex\"
else
echo shar: Extracting \"sld.tex\" \(1377 characters\)
sed "s/^X//" >sld.tex <<'END_OF_sld.tex'
X%	sld
X%	to generate slides
X
X%	\def\today{10 de mayo, 1988}
X%	\def\package{sld package}
X%	\setcounter{sldn}{7}		% next - 1
X
X%	Jose A. Manas
X%	Dpt. Ingenieria Telematica
X%	ETSIT Telecomunicacion
X%	Ciudad Universitaria
X%	E-28040  Madrid
X
X%	pepe@dit.upm.es
X
X\pagestyle{empty}
X\oddsidemargin 1cm
X\evensidemargin 1cm
X\topmargin -1cm			% 1.5cm
X\headheight 0cm
X\headsep 0cm
X\textheight 25cm
X\textwidth 16.5cm
X\footheight 0cm
X\footskip 0cm
X
X\parindent 0cm
X\parskip 1em
X\itemsep 1em
X
X\newcounter{sldn}
X\setcounter{sldn}{0}
X\newcounter{sldnt}
X
X\newcommand{\head}[1]{
X  \begin{center}
X    \Huge
X    #1
X  \end{center}
X  }
X
X\newenvironment{sld} {
X  \addtocounter{sldn}{1}
X  \setcounter{sldnt}{0}
X  \setlength{\unitlength}{1mm}
X  \begin{picture}(0, 20)
X    \put (160, 15) {\makebox (0, 0) [r] {{\small \today}}}
X    \put (160, 11) {\makebox (0, 0) [r] {{\small \package}}}
X    \put (160,  7) {\makebox (0, 0) [r] {{\small pg. \arabic{sldn}}}}
X    \special{psfile=dit-.ps}
X    \end{picture}
X  \huge
X  }{\newpage}
X
X\newenvironment{text} {
X  \addtocounter{sldnt}{1}
X  \setlength{\unitlength}{1mm}
X  \begin{picture}(0, 20)
X    \put (160, 15) {\makebox (0, 0) [r] {{\small \today}}}
X    \put (160, 11) {\makebox (0, 0) [r] {{\small \package}}}
X    \put (160,  7) {\makebox (0, 0) [r]
X		    {{\small pg. \arabic{sldn}.\arabic{sldnt}}}}
X    \special{psfile=dit-.ps}
X    \end{picture}
X   }{\newpage}
END_OF_sld.tex
if test 1377 -ne `wc -c <sld.tex`; then
    echo shar: \"sld.tex\" unpacked with wrong size!
fi
# end of overwriting check
fi
if test -f dit-.ps -a "${1}" != "-c" ; then 
  echo shar: Will not over-write existing file \"dit-.ps\"
else
echo shar: Extracting \"dit-.ps\" \(376 characters\)
sed "s/^X//" >dit-.ps <<'END_OF_dit-.ps'
X%	sld	.ps
X%	DIT --------------------------------------------------------
X%	frame for slides
X%	10 may, 1988
X
X%	Jose A. Manas
X%	Dpt. Ingenieria Telematica
X%	ETSIT Telecomunicacion
X%	Ciudad Universitaria
X%	E-28040  Madrid
X
X%	pepe@goya.uucp
X
Xnewpath
X0 10 moveto
X.8 setlinewidth
X/Times-BoldItalic findfont 50 scalefont setfont
X(dit) true charpath
X65 10 moveto
X480 10 lineto
Xstroke
END_OF_dit-.ps
if test 376 -ne `wc -c <dit-.ps`; then
    echo shar: \"dit-.ps\" unpacked with wrong size!
fi
# end of overwriting check
fi
echo shar: End of shell archive.
exit 0
