%> do tex %F -l -l -d"-t a4"

\documentstyle[12pt]{article}

\textwidth=16cm
\oddsidemargin=1cm
\evensidemargin=1cm
\textheight=22cm
\topmargin=0cm
\parindent=0mm
\parskip=4mm

\title{How to Use LOTOS Data Types from C Code	\\
       and How to Implement them by Hand	\\
       Using TOPO --- version 3R6
      }

\author{Marcelino Veiga			\\
	Jos{\'e} A. Ma{\~n}as			\\
					\\
	Dpt. Ingenier{\'\i}a Telem{\'a}tica	\\
	E.T.S.I. de Telecomunicaci{\'o}n	\\
	Univ. Polit{\'e}cnica de Madrid	\\
	E-28040 Madrid, SPAIN		\\
					\\
	{\tt <topo@dit.upm.es>}
       }

\date{10 October, 1994}

\pagestyle{myheadings}
\markright{Data Interface Manual}

\begin{document}

\maketitle

\begin{abstract}
This document deals with the data compiler of {\em topo}:
a compiler for the specification language LOTOS.
{\em Topo} generates separate C code to implement the behaviour and the
data.
There is a predefined interface between them,
that is covered in this paper.
As far as this interface is preserved,
the automatically generated data type implementation
may be replaced by efficient hand coded versions.
\end{abstract}

\newpage
\tableofcontents

\newpage

\section{Introduction}
{\em Topo} is a package for compiling system specifications written in
LOTOS\cite{kn:iso88} into executable programs that run on actual computers
\cite{kn:manas89}.
It has two separate parts: behaviour and data.
Both parts share a number of preliminary stages as syntax and
semantics checking.
Once the specification is accepted as correct,
and the specification objects are properly identified and associated
(definitions to usage occurrences),
the specification splits apart the behaviour and the data.

The behaviour compiler just cares after LOTOS {\em procedures}.
It takes a large list of procedures and generates a C
coroutine for each.
Each coroutine is a reentrant piece of code that implements an
automaton that behaves according to the LOTOS specification.
It has to call the data part for
\begin{itemize}
\item
  evaluating data expressions
\item
  testing for equality of two data values
\item
  copying and freeing data values.
\item
  printing values for debugging purposes or output data.
\item
  parsing strings for input data.
\end{itemize}

The data compiler handles a large (flat) collection of equations.
It treats the equations as rewrite rules that are repeatedly applied
to data value expressions till no other one applies.
This last stage of rewriting is regarded as the {\em canonical form}
of the data value.
Only canonical forms are handed around the compiled code.
Any other form is eagerly reduced down.
When testing for equality is required,
it is just needed to check for identical canonical forms.

It is up to the user to guarantee that the equational system may be
safely treated as a terminating and confluent (i.e. convergent)
rewrite system where the canonical form can be trusted as reachable
and unique.
But there are specific software tools out of {\em topo} to prove
that. See \cite{kn:knuth}, \cite{kn:reve} and \cite{kn:obj}.

The generated code is passive with respect to that generated by the
behaviour compiler:
it stays there waiting for being called.
Somehow, the code produced by the data compiler acts as a library that
is there to serve the behaviour part.
This fact allows to think of user implemented libraries that override
the code generated by the compiler.

Great improvements in efficiency may be achieved by this means.
Take for instance the case of integers.
This may be correctly handled by means of a rewrite system,
but it is much more efficient to use the operations provided either by
the hardware or in some system library.
These are directly addressable from most programming languages.
Even when system implementations do not exist,
great improvements may be achieved by direct hand coding of most used
operations.

In this paper we show how to use the output of the data compiler,
and how to add hand coded implementations of data types.
First, the interface of the data is shown.
Then there are described the data structures used to represent LOTOS
data types in a conventional compiler.
The C programming language is used all the time.
Finally it is presented how to write hand coded alternatives.

\section{Data Interface}
Let's start by presenting a typical (and useful) case of naturals
and booleans. It is fully detailed in an appendix with several variants.
Here follows its interface, i.e., sort and operation declarations.

\begin{quote}
\begin{verbatim}
type Boolean is
sorts
  bool
opns
  true  : -> bool  (* constructor *)
  false : -> bool  (* constructor *)
endtype

type Natural is Boolean
sorts
  nat
opns
  0    :          -> nat  (* constructor *)
  1    :          -> nat
  succ : nat      -> nat  (* constructor *)
  pred : nat      -> nat
  _+_  : nat, nat -> nat
  _<_  : nat, nat -> bool
  _==_ : nat, nat -> bool
  _/=_ : nat, nat -> bool
eqns
  ...
endtype
\end{verbatim}
\end{quote}

The behaviour compiler will assume a number of C functions to be
provided at link time,
either by the data compiler, or any other means.
There is one function per operation plus a function to check for
{\em meta-equality}.

Before proceeding, a word of warning.
In this example (and in many many others)
there are two equalities.
One is the specifier defined
(\verb/==/, in this example).
And there is a much more fundamental one,
the equality derived from the equational system.
The user may specify whatever he likes for \verb/==/
(for instance, equality modulus N),
and therefore there may be simultaneously a number of user defined
equalities,
each one being defined by a few equations.
But there is a single {\em meta-equality}, represented by \verb/=/,
and derived from the complete set of equations.

Back to the expected interface,
a number of functions is expected by the behaviour compiler, namely
\begin{quote}
\begin{verbatim}
bool true ()
bool false ()

nat  0 ()
nat  1 ()
nat  succ (nat)
nat  pred (nat)
nat  + (nat, nat)
bool < (nat, nat)
bool == (nat, nat)
bool /= (nat, nat)

bool  copy (bool)
void  free (bool)
int   equal (bool, bool)
char *draw (bool)
bool  parse (char *)

nat   copy (nat)
void  free (nat)
int   equal (nat, nat)
char *draw (nat)
nat   parse (char *)
\end{verbatim}
\end{quote}

There are a number of C functions associated to LOTOS operations,
plus five standard functions per sort to copy values, to free memory,
to check equality, to draw a node and to parse a string.
Let's start with the first group.

There are as many C functions as LOTOS operations and
as many C types as LOTOS sorts,
each one is named like in LOTOS.
This naive translation, obviously presents a number of problems
\begin{enumerate}
\item
  some operation names are not valid C identifiers,
  and will be rejected by the C compiler.
\item
  some sort names are not valid C predefined types,
  and there isn't either any mean to predefine them in a convenient
  manner.
\item
  in large specifications, identifiers may be overloaded, thus having
  equal lexical value but different meanings.
  Unfortunately, C does not support any overloading, but a flat
  name space.
\end{enumerate}

To sort out the first problem, let's instruct to the data compiler to
generate lexical names, and then let's annotate the LOTOS specification
associating a valid C identifier to those unacceptable LOTOS
identifiers.
Here follows the annotations for the example.
\begin{quote}
\begin{verbatim}
true  :      -> bool
false :      -> bool

0    (*| name zero |*) :          -> nat
1    (*| name one |*)  :          -> nat
succ                   : nat      -> nat
pred                   : nat      -> nat
_+_  (*| name plus |*) : nat, nat -> nat
_<_  (*| name lt   |*) : nat, nat -> bool
_==_ (*| name eq   |*) : nat, nat -> bool
_/=_ (*| name ne   |*) : nat, nat -> bool
\end{verbatim}
\end{quote}

Another possibility is to instruct to the data compiler to generate
internal names for operations, adding \verb/name/ annotations to those
ones we plan to use from C code.

The second nuisance needs a more drastic repair.
Let's assume there is two types defined in C that are used to store
values of LOTOS sorts.
They are called \verb/kdatum/ and \verb/udatum/ and its structure is
described in the next section.
\verb/kdatum/ stands for {\em Kaos datum}, because that is the name of
the run time support of the data compiler, and it is for sorts generated
by the data compiler.
\verb/udatum/ stands for {\em User datum}, because it is for hand coded
sorts, i.e. written by the user.

As you can see,
the whole set of sorts collapse in a set of only two C data types,
so we need some means to discriminate between different sorts.
This is simple: assign a unique integer to each one,
and provide a function for mapping names to numbers.

If we assume that in our example the sort \verb/bool/ is automatically
generated, and the sort \verb/nat/ is hand coded,
the corresponding C functions will be as follows:
\begin{quote}
\begin{verbatim}
kdatum true ()
kdatum false ()

udatum zero ()
udatum one ()
udatum succ (v1) udatum v1;
udatum pred (v1) udatum v1;
udatum plus (v1, v2) udatum v1, v2;
kdatum lt (v1, v2) udatum v1, v2;
kdatum eq (v1, v2) udatum v1, v2;
kdatum ne (v1, v2) udatum v1, v2;
\end{verbatim}
\end{quote}

Lastly, the problem of overloading must be resolved. So, we have to add
\verb/name/ annotations to some identifiers.

As already mentioned, there are also functions associated to sorts.
In fact, only some interface functions are provided for handling all the
sorts. There is a common initialization function, and a few more ones
divided in two groups: one for automatically generated
sorts, and another one for hand coded sorts.
So, the first group is for \verb/kdatum/,
and they use the mnemonic prefix \verb/kd_/.
And the second groups is for \verb/udatum/,
using the mnemonic prefix \verb/ud_/.
Functions of both groups
have an analogue interface, but \verb/ud_/ group have always
the \verb/sort/ parameter, because the data compiler does not know the
internal representation of hand coded sorts. Apart from this, they have
the same functionality and they look like:
\begin{itemize}
\item
  \verb/void ldcinit ()/        \\
  It initializes {\em kaos}, the run time support of the data compiler.
  So, it must be called before using any data type,
  both automatically generated ones and hand coded ones.
\item
  \verb/kdatum kd_copy (v) kdatum v;/	\\
  \verb/udatum ud_copy (sort, v) int sort; udatum v;/	\\
  These functions make a copy of a value.
\item
  \verb/void kd_free (v) kdatum v;/	\\
  \verb/void ud_free (sort, v) int sort; udatum v;/	\\
  These functions are just to release memory when a value is no longer
  needed.
\item
  \verb/int kd_equal (v1, v2) kdatum v1, v2;/	\\
  \verb/int ud_equal (sort, v1, v2) int sort; udatum v1, v2;/	\\
  \verb/int kd_gequal (v1, v2, mask) kdatum v1, v2; int mask;/	\\
  \verb/int ud_gequal (sort, v1, v2, mask) int sort; udatum v1, v2; int mask;/	\\
  These functions implement the {\em meta-equality},
  the equality derived from the equations.
  The difference among them is that the first pair does not free its
  arguments, and the second pair does it depending on the value of the binary
  \verb/mask/, i.e., if first bit is $ 1 $, the first argument must be
  freed, if the second one is $ 1 $ the second argument is freed, an if
  both ones are $ 1 $ both arguments are freed.
\item
  \verb/char *kd_draw (v) kdatum v;/	\\
  \verb/char *ud_draw (sort, v) int sort; udatum v;/	\\
  \verb/char *kd_gdraw (v, mask) kdatum v; int mask;/	\\
  \verb/char *ud_gdraw (sort, v, mask) int sort; udatum v; int mask;/	\\
  These functions return a string that is a textual representation of
  the value (or NULL if cannot), using always LOTOS prefix notation.
  They are useful for debugging purposes or for output data.
  The difference among them is the same as for equal functions.
\item
  \verb/int kd_parse (sort, ptr, r) int sort; char **ptr; kdatum *r/	\\
  \verb/int ud_parse (sort, ptr, r) int sort; char **ptr; udatum *r/	\\
  \verb/int kd_eval (sort, str, r) int sort; char *str; kdatum *r/	\\
  \verb/int ud_eval (sort, str, r) int sort; char *str; udatum *r/	\\
  These functions parse a string until it matches a {\em printed} value,
  then store it in \verb/r/ and return true (i.e. $\not= 0$).
  If matching fails (because of wrong syntax, ambiguity, ...),
  they left \verb/r/ unchanged and return false (i.e. $0$).
  The \verb/sort/ argument is mainly for ambiguity resolution
  between values of different sorts.
  There is also a difference among these functions:
  {\em x}\verb/d_eval()/ parses the whole string;
  and {\em x}\verb/d_parse()/ stops when it recognizes a value
  (or error), updating the pointer to the remainder substring.
  So, {\em x}\verb/d_eval()/ is useful for strings automatically
  generated by drawing functions (no errors expected),
  and {\em x}\verb/d_parse()/ for strings elaborated by hand (possible
  errors expected).
\item
  \verb/int kd_sort (snm) char *snm;/	\\
  \verb/int ud_sort (snm) char *snm;/	\\
  These functions return the unique identifier of a sort
  (or a negative number if not found or ambiguous).
\end{itemize}

At this moment, we have all functions we need for using both
automatically generated sorts and hand coded ones, with their
operations, of course. But, how must they be used?

The philosophy is simple:
when invoking a function representing an operation,
the caller must provide several arguments,
and the callee elaborates a result for the caller.
Besides, the arguments cannot be variables, but a copy of them,
because the callee suppose that all the arguments are owned by it.
In our example, a lotos expression like
\begin{quote}
\begin{verbatim}
succ(0) + pred(x)
\end{verbatim}
\end{quote}

In C must be written like
\begin{quote}
\begin{verbatim}
plus(succ(zero()), pred(kd_copy(x)))
\end{verbatim}
\end{quote}

where \verb/x/ is the C variable equivalent to the LOTOS one.
As you can see, it is slightly different:
\begin{enumerate}
\item
  It uses prefix notation and \verb/name/ annotations.
\item
  All operations are functions.
\item
  The variables must be \verb/kd_copy/ed (or \verb/ud_copy/ed).
\end{enumerate}

Simple enough? But how can be created and handled LOTOS variables in C?
You only need to declare the variable and assign a value, then you can
use copies of it to expressions, and finally you must remove it.
For example, suppose the LOTOS expression
\begin{quote}
\begin{verbatim}
let x: nat= succ(succ(0)) in (...)
\end{verbatim}
\end{quote}

As expected, the C equivalent is
\begin{quote}
\begin{verbatim}
{
  kdatum x;

  x= succ(succ(zero()));
  {...}
  kd_free(x);
}
\end{verbatim}
\end{quote}

And that's all. Only one remark, both \verb/kdatum/ and \verb/udatum/
are shared structures, so there is no real copy, and memory is only
deallocated when it become unused, i.e., there is no reference to it.
This mechanism saves space and time.
Besides, it allows to have values that will never be deallocated,
and there are functions to do it			\\
\verb/kdatum kd_const (n) kdatum n;/			\\
\verb/udatum ud_const (sort, n) int sort; udatum n;/

As a side effect of sharing datum, values cannot be modified.

\section{Data Structure}
As already seen, data values of automatically generated sorts are
represented by means of a type called \verb/kdatum/. Its structure only
concerns to the compiler, and the user must use it like an opaque
object.

For data values of hand coded sorts, the representation schema is left
to the user, and the data compiler only provides a structure for
encapsulating the user representation. The definitions is as follows:
\begin{quote}
\begin{verbatim}
typedef struct Udatum
{ int ino;              /* integer number */
  void *ptr;            /* any pointer */
} *udatum;
\end{verbatim}
\end{quote}

In this structure there are two fields for user data: \verb/ino/ and
\verb/ptr/. The first one for storing an integer number, and the second
one for any kind of pointer. This way the user can use from simple
representations to very complex ones.

There is also a function for allocating \verb/udatum/, and it is 
\verb/udatum ud_alloc ()/. It provides a newly created \verb/udatum/,
and it warranties that the field \verb/ino/ is set to $ 0 $, and the
field \verb/ptr/ is set to \verb/NULL/. The modification of these fields
is left to the user. Remember that an \verb/udatum/ is a shared
structure. So, you can only modify it at this moment, i.e., when you
create it.

\section{Hand Coding}
It is often the case that great benefit may derive from writing the
implementation of data types by hand.
There are some reasons for it:
\begin{itemize}
\item
  The sort strictly corresponds to some type directly accessible in C
  language.
  E.g. integers.
\item
  It is a burden to write equations for operations already available
  in C.
  E.g. integer division.
\item
  It is easier to code in C.
  E.g. sets.
\end{itemize}

In these cases,
the implementer needs to coordinate its C code with the interface
expected by the behavioural part.

The compilers are instructed of the intentions of the specifier by
means of annotations associated to sorts and/or operations.

\subsection{Automatically Generated Sorts}
If you just plan to remake the code to evaluate an operation,
but you do not really intend to change the data structure of the data
type, then it is only required that the operation is external.
The data compiler will refrain itself from generating its corresponding
function, but will expect it from the specifier at link time.
The drawback of this approach is that the specifier must be aware of
the data structures handled by the compiler and agree carefully with
them.

\subsubsection{Operation Implementation}
Let's go to our example. We are going to implement by hand a few
operations:
\begin{quote}
\begin{verbatim}
true  : -> bool
false : -> bool

0    (*| name zero |*) :          -> nat
1    (*| extern |*)
     (*| name one |*)  :          -> nat
succ                   : nat      -> nat
pred                   : nat      -> nat
_+_  (*| extern |*)
     (*| name plus |*) : nat, nat -> nat
_<_  (*| extern |*)
     (*| name lt   |*) : nat, nat -> bool
_==_ (*| name eq   |*) : nat, nat -> bool
_/=_ (*| name ne   |*) : nat, nat -> bool
\end{verbatim}
\end{quote}

First operation is \verb/1/. It is a constant, so we should write a
function that evaluates the constant once forever.
\begin{quote}
\begin{verbatim}
kdatum one ()
{
  static kdatum v= NULL;

  if (v == NULL)
  { v= succ(zero());
    (void) kd_const(v);
  }
  return v;
}
\end{verbatim}
\end{quote}

As you can see, the first time \verb/one()/ is called it initializes the
constant, and marks it as permanent.
From then on, it only returns its value.

The second operation is \verb/+/. It has arguments, so it needs to
make copies of them when it uses them in expressions, and it must free
them before returning.
\begin{quote}
\begin{verbatim}
kdatum plus (p1, p2)
  kdatum p1, p2;
{
  kdatum v;

  if (kd_gequal(p1, zero(), 0x2))
    v= kd_copy(p2);
  else if (kd_gequal(zero(), p2, 0x1))
    v= kd_copy(p1);
  else
    v= succ(succ(plus(pred(kd_copy(p1)), pred(kd_copy(p2)))));
  kd_free(p1);
  kd_free(p2);
  return v;
}
\end{verbatim}
\end{quote}

And the third operation is \verb/</. It is similar to last one,
but its result belongs to a different sort, \verb/bool/.
\begin{quote}
\begin{verbatim}
kdatum lt (p1, p2)
  kdatum p1, p2;
{
  kdatum v;

  if (kd_equal(p1, p2))
    v= false();
  else if (kd_gequal(p1, zero(), 0x2))
    v= true();
  else if (kd_gequal(zero(), p2, 0x1))
    v= false();
  else
    v= lt(pred(kd_copy(p1)), pred(kd_copy(p2)));
  kd_free(p1);
  kd_free(p2);
  return v;
}
\end{verbatim}
\end{quote}

\subsection{Hand Coded Sorts}
A more drastic approach is to declare the whole sort as external.
In this case, the data compiler needs information, via annotations,
for instantiating standard interface functions, because the data
structure of the sort is unknown by it.

Because of sharing data, there is no real copy, so it is not needed a
copying function. In other words, the standard copying functions do not
have to be instantiated.
However, it is necessary a freeing function, but only
for complex data, that put things in the pointer valued field. This way,
the standard freeing functions will call this function when the data is
not referenced.
\begin{quote}
\begin{verbatim}
void free_SORT (v)
  udatum v;
\end{verbatim}
\end{quote}

For checking equality is also needed a function. But in this case, it is
mandatory.
\begin{quote}
\begin{verbatim}
int equal_SORT (v1, v2)
  udatum v1, v2;
\end{verbatim}
\end{quote}

Both drawing and parsing values is not always necessary, so functions for
it are optional. For security, there is one restriction: if a parsing
function is provided, a drawing function must be provided too.
The drawing function must return a string with the pretty-printed value,
or NULL if cannot.
\begin{quote}
\begin{verbatim}
char *draw_SORT (v)
  udatum v;
\end{verbatim}
\end{quote}

The parsing function is a bit more complicated, because it must treat
possible errors. So, it must inspect the pointed string until it
recognizes a value of the sort or error, updating the pointer to the
remainder substring. If the parsing was successful, it stores the value
in \verb/r/ and returns true (i.e. $\not= 0$), or else returns false
(i.e. $0$).
\begin{quote}
\begin{verbatim}
int parse_SORT (p, r)
  char **p;
  udatum *r;
\end{verbatim}
\end{quote}

About operations, some restrictions are applied.
You must declare all the {\em constructor}s of that sort
as external too, otherwise a run time exception will be raised.
By the other hand, equations with an operation of a not \verb/extern/
sort as outermost of left member,
cannot contain non-constant \verb/extern/ expressions
in such left member.
The reason for such requirements is that the compiler does not know what
the user put in the \verb/udatum/.

\subsubsection{Sort Implementation}
In our example, we are going to implement by hand the sort \verb/nat/.
In this case, we only need to use the integer valued field of the
\verb/udatum/. So we do not have to provide any \verb/free/ annotation,
only the following ones:
\begin{quote}
\begin{verbatim}
nat (*| extern |*)
    (*| equal eqnat |*)
    (*| draw  dnat  |*)
    (*| parse pnat  |*)
\end{verbatim}
\end{quote}

The equality checker is simple, as you can see.
\begin{quote}
\begin{verbatim}
int eqnat (p1, p2)
  udatum p1, p2;
{
  return p1->ino == p2->ino;
}
\end{verbatim}
\end{quote}

For drawing values, we only need to print a decimal number.
\begin{quote}
\begin{verbatim}
char *dnat (n)
  udatum n;
{
  static char buf[10];
  extern char *sprintf();

  return sprintf(buf, "%d", n->ino);
}
\end{verbatim}
\end{quote}

So, the parser must be able to recognize any decimal number.
\begin{quote}
\begin{verbatim}
int pnat (p, r)
  char **p;
  udatum *r;
{
  int d, l;

  if (sscanf(*p, "%d%n", &d, &l) == 1)
  { *p+= l;                 /* update pointer */
    (*r)= ud_alloc();       /* build result */
    (*r)->ino= d;
    return TRUE;
  }
  else
    return FALSE;
}
\end{verbatim}
\end{quote}

Apart from those functions, it is useful to have a variable to store the
unique identifier of the sort, for using when calling standard interface
functions. Typically named like the sort (if possible):
\begin{quote}
\begin{verbatim}
int nat;
\end{verbatim}
\end{quote}

That variable must be initialized, and the better place to do it is in
\verb/ldcinit/ annotation.
\begin{quote}
\begin{verbatim}
(*| ldcinit
nat= ud_sort("nat");
|*)
\end{verbatim}
\end{quote}

\subsubsection{Operation Implementation}
As mentioned, the constructors are mandatory to implement them by hand,
and the other ones are optional or not depending on the equations.
Taking into account these restrictions, we are going to select a few
operations to implement by hand:
\begin{quote}
\begin{verbatim}
true  : -> bool
false : -> bool

0    (*| extern |*)
     (*| name zero |*) :          -> nat
1    (*| extern |*)
     (*| name one |*)  :          -> nat
succ (*| extern |*)    : nat      -> nat
pred (*| extern |*)    : nat      -> nat
_+_  (*| extern |*)
     (*| name plus |*) : nat, nat -> nat
_<_  (*| extern |*)
     (*| name lt   |*) : nat, nat -> bool
_==_ (*| name eq   |*) : nat, nat -> bool
_/=_ (*| name ne   |*) : nat, nat -> bool
\end{verbatim}
\end{quote}

Now we are going to show the implementation of some operations. The
whole example is in an appendix.

We can start with a constant like \verb/1/. As already mentioned, we
should write a function that evaluates it once forever and returns its
value.
\begin{quote}
\begin{verbatim}
udatum one ()
{
  static udatum v= NULL;

  if (v == NULL)
  { v= ud_alloc();
    v->ino= 1;
    (void) ud_const(nat, v);
  }
  return v;
}
\end{verbatim}
\end{quote}

We can follow with operation \verb/+/, a typical example of operation
with arguments. So, we must remember that the arguments must be copied
when used in expressions, and must be freed before
returning.
\begin{quote}
\begin{verbatim}
udatum plus (p1, p2)
  udatum p1, p2;
{
  udatum v;

  v= ud_alloc();
  v->ino= p1->ino + p2->ino;
  ud_free(nat, p1);
  ud_free(nat, p2);
  return v;
}
\end{verbatim}
\end{quote}

And to finish, the operation \verb/</. It also has arguments, but it
show how to interact with automatically generated sorts, in this case
with \verb/bool/.
\begin{quote}
\begin{verbatim}
kdatum lt (p1, p2)
  udatum p1, p2;
{
  kdatum v;

  if (p1->ino < p2->ino)
    v= true();
  else
    v= false();
  ud_free(nat, p1);
  ud_free(nat, p2);
  return v;
}
\end{verbatim}
\end{quote}

\section{Debugging Facilities}
The implementer must be very carefully with memory handling because
of memory sharing. There are two kind of problems:
\begin{itemize}
\item
  The specification running looses memory, and eventually crashes
  because of memory exhausted.
\item
  Too much memory is freed, so the specification crashes when it try to
  use memory already deallocated or reused.
\end{itemize}

Usually, the first problem arises when there is some missing
{\em x}\verb/d_free()/ or an extra {\em x}\verb/d_copy()/.
But, if the memory consumption of the specification is low and/or it is
not running for a long time, this problem never produces a crash.

The second problem much more important and generally is owed to some
extra {\em x}\verb/d_free()/ or a missing {\em x}\verb/d_copy()/.
In this situation it is highly probable (almost sure) that the
specification will crash. This problem is hard to track, because
normally the crash is produced too much far from the bug. For this
reason, \verb/topo/ provides a mechanism for detecting such errors
early, and it can be activated by means of the variable
\verb/kaos.debug/ ({\em kaos} is the kernel of the data compiler of {\em
topo}). By default its value is false (i.e. $0$), but if you set it to
true (i.e. $\not= 0$), all {\em kaos} functions check their parameters
looking for data corrupted, badly built, ..., raising an exception when
found.

This feature slows down the execution of the specification, but the
implementer can activate and disactivate it dynamically, so he/she only
needs to activate it in the part where he/she suspect there is (or is
near to) a problem.

\section{Conclusions}
This paper has presented the interface of
the code automatically generated by the data compiler of {\em topo} and
some examples of user generated code.

{\em Topo} is able to compile data as far as appropriate equations are
provided.
This may be cumbersome and not very efficient,
and there rises a need to hand code certain parts.
It is possible to remake some types,
and still allow the compiler to provide code for the rest.

The most risky business is to handle memory allocation, since errors
in this part are hard to detect and may drive into erratic behaviour
depending on exact scheduling of processes, and interaction with the
environment.
The compiler provides a number of library functions to handle memory
management,
plus mechanisms to adapt to peculiarities of user implemented types.
Besides, there is a debugging facility for early detection of memory
handling problems.

In a real environment, where big specifications are being implemented,
{\em topo} may support a methodology based on a number of precompiled
libraries of the most usual data types.
These libraries may be easily coordinated with the generated code,
thus allowing for reusability of software.

\newpage
\begin{thebibliography}{[Puymbroeck84]}

\bibitem[Goguen79]{kn:obj}
Goguen, J.A. and Tardo, J.J.,
An Introduction to OBJ: A Language for Writing and Testing Formal
Algebraic Program Specifications.
Proceeding Specifications of Reliable Software Conference, 1979.

\bibitem[ISO88]{kn:iso88}
ISO IS 8807,
``Information Processing Systems,
Open Systems Interconnection,
{\sc lotos},
A Formal Description Technique Based on the Temporal Ordering
of Observational Behavior'',
ISO, July, 1988.

\bibitem[Knuth69]{kn:knuth}
Knuth, D.E. and Bendix, P.B.,
``Simple Word Problems in Universal Algebras'',
Computational Problems in Abstract Algebra,
J. Leech (ed.),
Pergamon Press, 1969.

\bibitem[Lescanne83]{kn:reve}
Lescanne, P.,
``Computer Experiments with the REVE term Rewriting System Generator'',
10th POPL Conf. Austin, Texas, 1983.

\bibitem[Manas89]{kn:manas89}
Manas, J.A. and Miguel, T. de,
``FROM LOTOS to C'',
Formal Description Techniques,
K.J.Turner (editor), 1989.

\bibitem[Puymbroeck84]{kn:puym}
Puymbroeck, W. van, and Goovaerts, V.,
``A Translator for Algebraic Specifications''
Advances in Microprocessing and Microprogramming. 1984.
\end{thebibliography}

%\twocolumn
\newpage
\appendix
\section{Examples}
\subsection{AutoNat}

\subsubsection*{File autonat.lot}
\begin{verbatim}
specification AutoNat: noexit

type Boolean is
sorts
  bool
opns
  true  : -> bool
  false : -> bool
endtype

type Natural is Boolean
sorts
  nat
opns
  0    :          -> nat
  1    :          -> nat
  succ : nat      -> nat
  pred : nat      -> nat
  _+_  : nat, nat -> nat
  _<_  : nat, nat -> bool
  _==_ : nat, nat -> bool
  _/=_ : nat, nat -> bool
eqns
  forall x, y: nat
  ofsort nat
    1 = succ(0);
    pred(succ(x)) = x;
    x + 0 = x;
    x + succ(y) = succ(x + y);
  ofsort bool
    0 < succ(x) = true;
    x < 0 = false;
    succ(x) < succ(y) = x < y;
  ofsort bool
    x < y => x == y = false;
    x < y => x /= y = true;
    x = y => x == y = true;
    x = y => x /= y = false;
    y < x => x == y = false;
    y < x => x /= y = true;
endtype

behaviour
  stop
endspec
\end{verbatim}

\subsubsection*{File autonat.gld}
\begin{verbatim}
opns any: forall -> any => (*| nonconstructor |*) (*| lexicalifpossible |*);

specification (* Boolean *) ;
sorts
  bool ;
opns
  true : -> bool => (*| constructor |*) ;
  false: -> bool => (*| constructor |*) ;
endspec (* Boolean *) ;

specification (* Natural *) =>
  (*| ldc #include "nat.h" |*) ;
sorts
  nat ;
opns
  0   :          -> nat  => (*| constructor |*) (*| name zero |*) ;
  1   :          -> nat  => (*| extern |*) (*| name one |*) ;
  succ: nat      -> nat  => (*| constructor |*) ;
  pred: nat      -> nat  => (*| partial !kd_gequal($1, zero(), 0x2) |*) ;
  _+_ : nat, nat -> nat  => (*| extern |*) (*| name plus |*) ;
  _<_ : nat, nat -> bool => (*| extern |*) (*| name lt |*) ;
  _==_: nat, nat -> bool => (*| name eq |*) ;
  _/=_: nat, nat -> bool => (*| name ne |*) ;
endspec (* Natural *) ;
\end{verbatim}

\newpage
\subsubsection*{File nat.h}
\begin{verbatim}
#include <kaos.hh>

kdatum one ();
kdatum plus ();
kdatum lt ();
\end{verbatim}

\subsubsection*{File nat.c}
\begin{verbatim}
#include "nat.h"

extern kdatum true ();
extern kdatum false ();

extern kdatum zero ();
extern kdatum succ ();
extern kdatum pred ();

kdatum one ()
{
  static kdatum v= NULL;

  if (v == NULL)
  { v= succ(zero());
    (void) kd_const(v);
  }
  return v;
}

kdatum plus (p1, p2)
  kdatum p1, p2;
{
  kdatum v;

  if (kd_gequal(p1, zero(), 0x2))
    v= kd_copy(p2);
  else if (kd_gequal(zero(), p2, 0x1))
    v= kd_copy(p1);
  else
    v= succ(succ(plus(pred(kd_copy(p1)), pred(kd_copy(p2)))));
  kd_free(p1);
  kd_free(p2);
  return v;
}

kdatum lt (p1, p2)
  kdatum p1, p2;
{
  kdatum v;

  if (kd_equal(p1, p2))
    v= false();
  else if (kd_gequal(p1, zero(), 0x2))
    v= true();
  else if (kd_gequal(zero(), p2, 0x1))
    v= false();
  else
    v= lt(pred(kd_copy(p1)), pred(kd_copy(p2)));
  kd_free(p1);
  kd_free(p2);
  return v;
}
\end{verbatim}

\newpage
\subsubsection*{File test.h}
\begin{verbatim}
void test ();
\end{verbatim}

\subsubsection*{File test.c}
\begin{verbatim}
#include "autonat.ldc.hh"
#include "test.h"

static void test_bool ()
{
  kdatum t, f;

  (void) printf("t <- true\n");
  t= true();
  (void) printf("t := %s\n", kd_draw(t));

  (void) printf("f <- false\n");
  f= false();
  (void) printf("f := %s\n", kd_draw(f));

  kd_free(t);
  kd_free(f);
}

static void test_nat ()
{
  kdatum m, n;

  (void) printf("m <- 0\n");
  m= zero();
  (void) printf("m := %s\n", kd_draw(m));
  kd_free(m);

  (void) printf("m <- 1\n");
  m= one();
  (void) printf("m := %s\n", kd_draw(m));
  kd_free(m);

  (void) printf("m <- succ(succ(0))\n");
  m= succ(succ(zero()));
  (void) printf("m := %s\n", kd_draw(m));

  (void) printf("n <- succ(succ(succ(m)))\n");
  n= succ(succ(succ(kd_copy(m))));
  (void) printf("n := %s\n", kd_draw(n));

  (void) printf("succ(m) := %s\n", kd_gdraw(succ(kd_copy(m)), 0x1));
  (void) printf("pred(m) := %s\n", kd_gdraw(pred(kd_copy(m)), 0x1));
  (void) printf("m + n := %s\n", kd_gdraw(plus(kd_copy(m),
                                               kd_copy(n)), 0x1));
  (void) printf("m < n := %s\n", kd_gdraw(lt(kd_copy(m),
                                             kd_copy(n)), 0x1));
  (void) printf("m == n := %s\n", kd_gdraw(eq(kd_copy(m),
                                              kd_copy(n)), 0x1));
  (void) printf("m /= n := %s\n", kd_gdraw(ne(kd_copy(m),
                                              kd_copy(n)), 0x1));

  kd_free(m);
  kd_free(n);
}

void test ()
{
  kaos.debug= TRUE;
  (void) printf("*** testing bool sort ***\n");
  test_bool();
  (void) printf("\n");
  (void) printf("*** testing nat sort ***\n");
  test_nat();
  kaos.debug= FALSE;
}
\end{verbatim}

\subsubsection*{File autonat.c}
\begin{verbatim}
#include <lotos.hh>
#include "test.h"

main()
{
  ldcinit ();
  test();
  lbcinit (0, NULL);
  exit(sch());
}
\end{verbatim}

\newpage
\subsubsection*{File makefile}
\begin{verbatim}
SPEC=   autonat
DNAME=  $(SPEC).ldc
TNAME=  $(SPEC).lbc
GLAD=   $(SPEC).gld

CFLAGS=-g -I$(TOPOINC)
LDFLAGS=-L$(TOPOLIB) -lotos -lkaos

TRGT=   $(SPEC)
OBJS=   nat.o $(DNAME).o $(TNAME).o test.o $(SPEC).o

$(TRGT):        $(OBJS)
        $(CC) $(CFLAGS) -o $@ $(OBJS) $(LDFLAGS)

DNAME_HH=       nat.h $(DNAME).hh
TNAME_HH=       $(DNAME_HH) $(TNAME).hh

nat.c:  nat.h
$(DNAME).o:     $(DNAME_HH)
$(TNAME).o:     $(TNAME_HH)
test.c: $(DNAME_HH) test.h
$(SPEC).c:      test.h

$(DNAME).c $(DNAME).hh: $(SPEC).lot $(GLAD) $(SPEC).ctx
        $(TOPOBIN)/topo $(SPEC) -verbose -d
$(TNAME).c $(TNAME).hh: $(SPEC).lot $(GLAD) $(SPEC).ctx
        $(TOPOBIN)/topo $(SPEC) -verbose -t

$(SPEC).ctx:
        $(TOPOBIN)/toposet $(SPEC) -dname $(DNAME) -tname $(TNAME)
        $(TOPOBIN)/toposet $(SPEC) -glad $(GLAD)

clean tidy::
        rm -f *~ core topocore
        rm -f $(OBJS)
        rm -f $(SPEC).com

clean::
        $(TOPOBIN)/topo $(SPEC) -clean

tidy::
        rm -f $(TRGT)
        $(TOPOBIN)/topo $(SPEC) -tidy
        rm -f $(SPEC).ctx
\end{verbatim}

\newpage
\subsection{HandNat}

\subsubsection*{File handnat.lot}
\begin{verbatim}
specification HandNat: noexit

type Boolean is
sorts
  bool
opns
  true  : -> bool
  false : -> bool
endtype

type Natural is Boolean
sorts
  nat
opns
  0    :          -> nat
  1    :          -> nat
  succ : nat      -> nat
  pred : nat      -> nat
  _+_  : nat, nat -> nat
  _<_  : nat, nat -> bool
  _==_ : nat, nat -> bool
  _/=_ : nat, nat -> bool
eqns
  forall x, y: nat
  ofsort nat
    1 = succ(0);
    pred(succ(x)) = x;
    x + 0 = x;
    x + succ(y) = succ(x + y);
  ofsort bool
    0 < succ(x) = true;
    x < 0 = false;
    succ(x) < succ(y) = x < y;
  ofsort bool
    x < y => x == y = false;
    x < y => x /= y = true;
    x = y => x == y = true;
    x = y => x /= y = false;
    y < x => x == y = false;
    y < x => x /= y = true;
endtype

behaviour
  stop
endspec
\end{verbatim}

\subsubsection*{File handnat.gld}
\begin{verbatim}
opns any: forall -> any => (*| nonconstructor |*) (*| lexicalifpossible |*);

specification (* Boolean *) ;
sorts
  bool ;
opns
  true : -> bool => (*| constructor |*) ;
  false: -> bool => (*| constructor |*) ;
endspec (* Boolean *) ;

specification (* Natural *) =>
  (*| ldc #include "nat.h" |*)
  (*| ldcinit nat= ud_sort("nat"); |*) ;

sorts
  nat => (*| extern |*) (*| nofree |*)
                        (*| equal eqnat |*)
                        (*| draw  dnat |*)
                        (*| parse pnat |*) ;
opns
  0   :          -> nat  => (*| constructor |*)
                            (*| extern |*) (*| name zero |*) ;
  1   :          -> nat  => (*| extern |*) (*| name one |*) ;
  succ: nat      -> nat  => (*| constructor |*)
                            (*| extern |*) ;
  pred: nat      -> nat  => (*| extern |*) ;
  _+_ : nat, nat -> nat  => (*| extern |*) (*| name plus |*) ;
  _<_ : nat, nat -> bool => (*| extern |*) (*| name lt   |*) ;
  _==_: nat, nat -> bool => (*| name eq |*) ;
  _/=_: nat, nat -> bool => (*| name ne |*) ;
endspec (* Natural *) ;
\end{verbatim}

\newpage
\subsubsection*{File nat.h}
\begin{verbatim}
#include <kaos.hh>

extern int nat;

int eqnat ();
char *dnat ();
int pnat ();

udatum zero ();
udatum one ();
udatum succ ();
udatum pred ();
udatum plus ();
kdatum lt ();
\end{verbatim}

\subsubsection*{File nat.c}
\begin{verbatim}
#include <stdio.h>
#include <assert.h>
#include "nat.h"

extern kdatum true ();
extern kdatum false ();

int nat= -1;

int eqnat (p1, p2)
  udatum p1, p2;
{
  return p1->ino == p2->ino;
}

char *dnat (n)
  udatum n;
{
  static char buf[10];
  extern char *sprintf();

  return sprintf(buf, "%d", n->ino);
}

int pnat (p, r)
  char **p;
  udatum *r;
{
  int d, l;

  if (sscanf(*p, "%d%n", &d, &l) == 1)
  { *p+= l;                 /* update pointer */
    (*r)= ud_alloc();       /* build result */
    (*r)->ino= d;
    return TRUE;
  }
  else
    return FALSE;
}

udatum zero ()
{
  static udatum v= NULL;

  if (v == NULL)
  { v= ud_alloc();
    v->ino= 0;
    (void) ud_const(nat, v);
  }
  return v;
}

udatum one ()
{
  static udatum v= NULL;

  if (v == NULL)
  { v= ud_alloc();
    v->ino= 1;
    (void) ud_const(nat, v);
  }
  return v;
}

udatum succ (p1)
  udatum p1;
{
  udatum v;

  v= ud_alloc();
  v->ino= p1->ino + 1;
  ud_free(nat, p1);
  return v;
}

udatum pred (p1)
  udatum p1;
{
  udatum v;

  assert(p1->ino > 0);
  v= ud_alloc();
  v->ino= p1->ino - 1;
  ud_free(nat, p1);
  return v;
}

udatum plus (p1, p2)
  udatum p1, p2;
{
  udatum v;

  v= ud_alloc();
  v->ino= p1->ino + p2->ino;
  ud_free(nat, p1);
  ud_free(nat, p2);
  return v;
}

kdatum lt (p1, p2)
  udatum p1, p2;
{
  kdatum v;

  if (p1->ino < p2->ino)
    v= true();
  else
    v= false();
  ud_free(nat, p1);
  ud_free(nat, p2);
  return v;
}
\end{verbatim}

\newpage
\subsubsection*{File test.h}
\begin{verbatim}
void test ();
\end{verbatim}

\subsubsection*{File test.c}
\begin{verbatim}
#include "handnat.ldc.hh"
#include "test.h"

static void test_bool ()
{
  kdatum t, f;

  (void) printf("t <- true\n");
  t= true();
  (void) printf("t := %s\n", kd_draw(t));

  (void) printf("f <- false\n");
  f= false();
  (void) printf("f := %s\n", kd_draw(f));

  kd_free(t);
  kd_free(f);
}

static void test_nat ()
{
  udatum m, n;

  (void) printf("m <- 0\n");
  m= zero();
  (void) printf("m := %s\n", ud_draw(nat, m));
  ud_free(nat, m);

  (void) printf("m <- 1\n");
  m= one();
  (void) printf("m := %s\n", ud_draw(nat, m));
  ud_free(nat, m);

  (void) printf("m <- succ(succ(0))\n");
  m= succ(succ(zero()));
  (void) printf("m := %s\n", ud_draw(nat, m));

  (void) printf("n <- succ(succ(succ(m)))\n");
  n= succ(succ(succ(ud_copy(nat, m))));
  (void) printf("n := %s\n", ud_draw(nat, n));

  (void) printf("succ(m) := %s\n", ud_gdraw(nat, succ(ud_copy(nat, m)), 0x1));
  (void) printf("pred(m) := %s\n", ud_gdraw(nat, pred(ud_copy(nat, m)), 0x1));
  (void) printf("m + n := %s\n", ud_gdraw(nat, plus(ud_copy(nat, m),
                                                    ud_copy(nat, n)), 0x1));
  (void) printf("m < n := %s\n", kd_gdraw(lt(ud_copy(nat, m),
                                             ud_copy(nat, n)), 0x1));
  (void) printf("m == n := %s\n", kd_gdraw(eq(ud_copy(nat, m),
                                              ud_copy(nat, n)), 0x1));
  (void) printf("m /= n := %s\n", kd_gdraw(ne(ud_copy(nat, m),
                                              ud_copy(nat, n)), 0x1));

  ud_free(nat, m);
  ud_free(nat, n);
}

void test ()
{
  kaos.debug= TRUE;
  (void) printf("*** testing bool sort ***\n");
  test_bool();
  (void) printf("\n");
  (void) printf("*** testing nat sort ***\n");
  test_nat();
  kaos.debug= FALSE;
}
\end{verbatim}

\subsubsection*{File handnat.c}
\begin{verbatim}
#include <lotos.hh>
#include "test.h"

main()
{
  ldcinit ();
  test();
  lbcinit (0, NULL);
  exit(sch());
}
\end{verbatim}

\newpage
\subsubsection*{File makefile}
\begin{verbatim}
SPEC=   handnat
DNAME=  $(SPEC).ldc
TNAME=  $(SPEC).lbc
GLAD=   $(SPEC).gld

CFLAGS=-g -I$(TOPOINC)
LDFLAGS=-L$(TOPOLIB) -lotos -lkaos

TRGT=   $(SPEC)
OBJS=   nat.o $(DNAME).o $(TNAME).o test.o $(SPEC).o

$(TRGT):        $(OBJS)
        $(CC) $(CFLAGS) -o $@ $(OBJS) $(LDFLAGS)

DNAME_HH=       nat.h $(DNAME).hh
TNAME_HH=       $(DNAME_HH) $(TNAME).hh

nat.c:  nat.h
$(DNAME).o:     $(DNAME_HH)
$(TNAME).o:     $(TNAME_HH)
test.c: $(DNAME_HH) test.h
$(SPEC).c:      test.h

$(DNAME).c $(DNAME).hh: $(SPEC).lot $(GLAD) $(SPEC).ctx
        $(TOPOBIN)/topo $(SPEC) -verbose -d
$(TNAME).c $(TNAME).hh: $(SPEC).lot $(GLAD) $(SPEC).ctx
        $(TOPOBIN)/topo $(SPEC) -verbose -t

$(SPEC).ctx:
        $(TOPOBIN)/toposet $(SPEC) -dname $(DNAME) -tname $(TNAME)
        $(TOPOBIN)/toposet $(SPEC) -glad $(GLAD)

clean tidy::
        rm -f *~ core topocore
        rm -f $(OBJS)
        rm -f $(SPEC).com

clean::
        $(TOPOBIN)/topo $(SPEC) -clean

tidy::
        rm -f $(TRGT)
        $(TOPOBIN)/topo $(SPEC) -tidy
        rm -f $(SPEC).ctx
\end{verbatim}

\end{document}
