%\section{Implementation}

\begin{figure}
  \centerline{\fbox{\psfig{figure=testsystem.id,height=12cm}}}
  \caption{Organization of the test system}
\end{figure}

After specifying the test suite,
we have two objects:
a LOTOS specification,
and a test suite specification.
In order to mix them together,
it seems necessary to get a new LOTOS specification that puts
together:
\begin{itemize}
\item
  the canonical data type in the user specification
\item
  the test cases proposed by the debugger,
  after expanding groups of assertions on collections of data values
\item
  the verdict assignment criteria
\end{itemize}

The all--within--LOTOS approach seems very promising,
since more complex behaviour of the tester may be specified using
LOTOS operators.
Furthermore,
operation overloading,
and the complexities derived from renaming and actualizing types may
be handled in a semantically consistent environment.

The LOTOS specification may organize test linking in many ways,
and here we shall propose one based on the use of annotations,
and clearly oriented towards using TOPO to run the tests.
Other approaches look interesting to study,
but are only sketched below \ldots for the time being.

\subsection{Sequential execution}
The test suite may be transformed into a LOTOS specification of
behaviour.
The behaviour of the tester is modeled by sequential probe of each
test case, and each premiss of each test case.
The basic problem of assertion failure,
that is the fundamental issue of negation,
is dealt with by means of annotations.

It is assumed below that an interpretation of a LOTOS specification is
able to decide completely equality.
That is, there is no room for undecidability.
Be aware that from an equational point of view,
equality is only semi--decidable.
So, a stronger criterion is expected from tools,
a criterion that is usually based on rewrite semantics.

Very often we are in a situation where
some predicate $P$ may hold or not.
It would be great to have full decision in LOTOS:
\begin{verbatim}
    [ P ]-> ... (* P holds *)
  []
    [ ! P ]-> ... (* P does not hold *)
\end{verbatim}
where \verb/!/ stands for negation.
But unfortunately
there is in LOTOS no \verb/!/.

So, we shall organize such decisions as
\begin{verbatim}
    [ P ]-> ... (* P holds *)
  []
    (*| priority -1 |*) ... (* P does not hold *)
\end{verbatim}
that is, the undecidable behaviour is given a lower priority,
and will only be selected if the other branch
(the ``it holds'' alternative)
is not selectable;
that is, if P does not hold.

Thus,
the basic code generated for a positive assertion (\verb/=/) is
\begin{verbatim}
Code (P) ::=
    [ P ]-> i (*| C printf ("pass N\n"); |*) ; exit
  []
    (*| priority -1 |*) i (*| C printf ("fail N\n"); |*) ; exit
\end{verbatim}

and for a negative assertion (\verb/!=/):
\begin{verbatim}
Code (F) ::=
    [ F ]-> i (*| C printf ("fail N\n"); |*) ; exit
  []
    (*| priority -1 |*) i (*| C printf ("pass N\n"); |*) ; exit
\end{verbatim}
where $N$ is the number of the test case in the test suite.

When there are premisses (\verb/P => A/),
a previous step is introduced to check the premiss:
\begin{verbatim}
Code (P, A) ::=
    [ P ]-> i (*| C printf ("premiss N.p\n"); |*) ; Code (A)
  []
    (*| priority -1 |*) i (*| C printf ("inconclusive N.p\n"); |*) ; exit
\end{verbatim}
where $N$ is the test case number,
and $p$ is the premiss number.
When there is a series of premisses,
the generated code is a sequence of probes.

The existence of local definitions is handled by means of expansion.
For instance,
\begin{verbatim}
  for m: s in [m1, m2] [[ A ]]
\end{verbatim}
generates the following code:
\begin{verbatim}
  ( let m: s = m1 in Code (A) )
  >>
  ( let m: s = m2 in Code (A) )
  >>
\end{verbatim}
If there were several local definitions,
\begin{verbatim}
  for m: s in [m1, m2],
  for n: s in [n1, n2, n3] [[ A ]]
\end{verbatim}
the cartesian product of choices is used:
\begin{verbatim}
  ( let m: s= m1, n: s= n1 in Code (A) )
  >>
  ( let m: s= m1, n: s= n2 in Code (A) )
  >>
  ( let m: s= m1, n: s= n3 in Code (A) )
  >>
  ( let m: s= m2, n: s= n1 in Code (A) )
  >>
  ( let m: s= m2, n: s= n2 in Code (A) )
  >>
  ( let m: s= m2, n: s= n3 in Code (A) )
  >>
\end{verbatim}
Each expanded test case receives a consecutive number $N$ for trace
reference.

Given a user specification \verb/spec.lot/,
its canonical data type is extracted by exercising the semantics
analysis on the specification,
and asking the pretty printer just to print the canonical data type.
Then,
the tester is built as
\begin{verbatim}
specification Tester : noexit 
    << the canonical data type comes here verbatim >>
  behaviour
    Code (Test_Suite)
    >>
    stop
  endspec
\end{verbatim}
This specification may go through the compiler,
and generate a program that, when executed,
provides a verdict for each case in the test suite.

\subsection{Symbolic execution}
The approach above is strongly based on the use of annotations,
both to avoid deadlock when predicates do not hold,
and to emit reports on testing progress.

If rather than TOPO,
a symbolic tool is to be used,
alternative means must be found.

First, to emit reports on test progress,
rather than internal actions,
we would use external gates that allow to observe the system.
For instance:
\begin{verbatim}
Code (P) ::=
    [ P ]-> pass ; exit
  []
    (*| priority -1 |*) fail ; exit
\end{verbatim}
The gates may be enriched with a natural number $N$ that informs of the
test case under consideration:	\\
\centerline{\verb/pass !N ; exit/}	\\
This requires to introduce in the tester a notion of natural numbers,
both to have the sort, and to have operations for arabic numbers.
But this on one hand pollutes the original specification introducing
extra data types,
and on the other hand, may be very cumbersome.
For instance, think of defining 1000 operations for a test suite with
1000 test cases.
Or, do we prefer Peano arithmetic?

An alternative could be to have as many gates as test cases,
and so have a clear indication of test run,
completely based on gate identifiers.
Unfortunately,
this approach also implies an explosion of identifiers.

Priority annotations should be removed too.
One possibility is to remove the alternative branch completely.
Then the tester runs until a failure is detected
(what about must not assertions?).
Another possibility is to keep the alternate branch,
and carefully observe whether both branches are possible
(denoting the test is passed),
or only the unguarded one (denoting failure).

It is unclear how to deal with must not assertions,
and how to report on tests cases where the premiss(es) fails.

A symbolic tool would provide some benefits.
For instance,
assertions on {\em any value} could be eventually proved.
LOLA or SMILE are able to rewrite terms with free variables.
A syntactic check may be performed on the outcome of the rewriting
process.
Of course,
this is a semi--decidable method:
if two free terms are rewritten into the same canonical form
(modules variable names),
they are proved to hold for any value;
but if the result of rewriting is not identical,
we may not conclude anything.

SMILE could still apply narrowing to try to find solutions for an
assertion on free terms.
Under some circumstance,
narrowing may yield a definite result:
there is no value for which this assertion holds.
But narrowing may not give a definite answer.

However, this option to use symbolic tools looks worth further study
to try to overcome some of the drawbacks reported above.

\subsection{Parallel execution}
Symbolic tools supporting the expansion theorems,
might be used to run all the tests in parallel:
\begin{verbatim}
    [ A1 ]-> pass ; ...
  []
    [ A2 ]-> pass ; ...
  ...
  []
    [ An ]-> pass ; ...
\end{verbatim}
Passed test cases show up as offers of gate \verb/pass/;
while failures are denoted by \verb/stop/.
This is an alternative to the \verb/priority/ annotations to provide
escape paths.

The same problems reported above for symbolic execution occur again.
This approach looks nice for short test suites,
but it is doubtful how useful it may be for test suites composed of
hundreds of cases.




