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

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

\documentstyle[12pt]{article}
\input{psfig.tex}

\title	{rdtts: Real Data Types Test Specification}
\author	{Jos\'e A. Ma\~nas}
\date{19 September, 1992}

\begin{document}

\maketitle

\begin{abstract}
  This paper focuses on the problem of getting correct data type
  specifications,
  where correctness is considered with respect to user intentions.
  The procedure used to achieve this objective is to exercise the
  data specification,
  either symbolically or as a result of compiling it.

  A language to specify test cases in a compact manner is presented.
  Although the semantics after this language are straightforward,
  and its handling can be done by hand;
  its existence as a tool will promote the existence of a data testing
  phase during specification development.

  The document mostly deals with the data part.
  Data part is expected to be submitted to testing before the complete
  behaviour is tested.
  This order will permit the specifier to focus on one problem at a
  time during testing of the specification.

  The paper walks towards a testing tool,
  where the methodological considerations will be applied to the
  test sequences selection,
  test run,
  and interpretation of the results.
\end{abstract}

\tableofcontents

\section{Introduction}
A LOTOS specification is produced by humans,
and is therefore subject to errors.
In fact,
any human specification contains a number of errors,
and it is always necessary to go through an in-house testing phase to
debug it.

\begin{quote}
\em\large\raggedleft
  Testing is the process of executing a program	\\
  with the intent of finding errors.	\\
  {\em\normalsize G. Myers, The Art of Software Testing}
\end{quote}

The case of LOTOS presents two clearly distinguished parts:
data and behaviour.
Data specification is rather autonomous:
its specification is independent of any behavioral consideration.
On the other hand,
behaviour specification is clearly dependent on data that are used for
guards and predicates.
Therefore,
it is natural to divide the debugging phase into two subphases:
the first one devoted to get the data right,
the second one to get the behaviour right.

Of course,
the ending of a subphase does not mean it will be never entered again.
Testing just discloses bugs,
and after a large number of test cases have been successfully passed,
the confidence on the correctness of the specification is higher,
but it cannot be absolute.
Therefore,
it may happen that during behaviour debugging,
new bugs are discovered in the data part,
and that subphase has to be entered again.

Last, but not least,
LOTOS equations are usually understood as left to right rewrite rules.
The correctness of this interpretation relies on the property of the
rewrite system to be confluent and terminating.
That is, it assumes that any expression may be rewritten a finite
number of times,
and that whichever possible rewriting we apply to an expression,
it yields that very same result.

In other words,
most available tools assume that language expressions may be rewritten
into a canonical form,
and that any two terms that are equal according to the equational
reasoning on the language axioms,
will yield the very same canonical form,
where equality may be decided syntactically.

Unfortunately,
this property cannot be guaranteed in general.
Although there are tools to check it,
they are not usually able to handle big specifications,
and they are just too prone to regard the issue as undecidable.

Therefore,
there is a risk of an incorrect interpretation of equations that
results quite often in the following situation:
two different tools show different behaviour of the same
specification.
This is unpleasant result is becoming more and more familiar to
specifiers,
as more and more tools are available to deal with LOTOS specs.
It is usually due to the fact that user equations are not confluent,
and since two different tools are very likely to apply two different
heuristics to decide which rewrite rule to apply,
they come to different terminal forms,
that are not canonical any longer.

Thus,
it sounds interesting to use those tools interpretation of the
equations to drive the test cases.
So,
we will discover both proper bugs in the data specification,
and bugs induced by the interpretation of equations as rewrite rules.

\section{Objectives}
Some definitions (related to testing) may clarify our intentions:
\begin{description}
\item[verification.-]
  Are we specifying the system right?
\item[validation.-]
  Are we specifying the right system?
\item[test case.-]
  A set of input data used to test a particular piece of code or
  function,
  with its accompanying expected output(s).
\item[testing vs. debugging.-]
  Testing is the act of finding errors;
  debugging is re--designing or re--specifying
  all or part of the formal model of the system,
  to get the errors out.
\end{description}

The objective of ADT testing is to show out inconsistencies between
the equations and the user desires {(\em validation)},
as well as defects in the equation set that preclude its correct
interpretation as a rewrite system {(\em verification)}.

Our test cases encompass both the data to test,
and the expected output by means of assertions,
rendering extremely compact specifications of test suites.

The objective of this document is to identify tools that may support
ADT testing.

\section{Opportunities to Fail}

\begin{figure}
  \centerline{\fbox{\psfig{figure=eqdefects.id,width=15cm}}}
  \caption{Defects in an equational model}
\end{figure}

\begin{figure}
  \centerline{\fbox{\psfig{figure=rwdefects.id,width=15cm}}}
  \caption{Defects in a rewrite system}
\end{figure}

There are several reasons for an ADT specification not to agree to
user expectations.

ADT specifications in LOTOS get their meaning from the initial model
of the collection of algebras that satisfy the equations put forth
by the user.
This initial model has the property that any two terms on the algebra
are different unless there are equations enough to prove that they are
equal.
It tries to make different as many terms as possible.
With this criterion,
the set of terms of a sort are classified into equivalence classes:
two terms belong to the same equivalence class iff they are equal.

With respect to the user,
if it regards two terms as being equal,
they must belong to the same equivalence class.
It the user wishes to terms to be distinct,
they must belong to different equivalence classes.

The model of equivalence classes allows for an easy mental model of
countries and borders.
Two terms in the same country are equal,
and two terms in different countries are different.

In this image,
an equational system fails to specify user desires both if there are
too many borders
(and people of the same intended country are put apart);
or if there are too few borders
(people of different countries are mixed together.

Too many equations may result into too few borders,
and the other way round too few equations may result into too many
borders.
So the objective of testing is to check that there are enough
equations;
and, if there are more than enough,
that these ``redundant'' equations do not collapse the system.

When tools come into the scene,
it becomes more complicated.
Most tools on LOTOS
(at least all those that the authors are aware of)
work on the assumption that it is possible to identify a singular term
of each class that may be used as the representative of the class for
every practical purpose.
This term is usually known as the ``canonical form'' of the terms of an
equivalence class.

Under this assumption,
two terms are equal if and only if both share a canonical form.
Different canonical forms imply belongship to different equivalence
classes.

This method used by tools is very effective computationally.
It is able to give an answer in any case,
and turns the semi-decidability of equational reasoning,
into a decidable problem.
But a price is paid for it.

Tools depend on the existence and computability of the singular
canonical form for every term in the algebra.

Then tools use to make further assumptions,
and opt to hand the equational system as a rewrite system.
That is,
every term the user writes down is scanned to check whether it fits
into the pattern of the left hand side of some equation.
If so,
the term is rewritten into the right hand side of the same equation.
The procedure is repeated once and again,
until no left hand side of any equation applies.

This procedure is computationally effective provided that
\begin{itemize}
\item
  It terminates
\item
  It finds THE canonical form
\end{itemize}
and, conversely,
it may fail either in terminating,
or in finding the canonical form.

Termination is easy to detect: it is very noticeable.
No more comments are devoted to it.

Finding the canonical form is more obscure,
and it may easily happen that there are several different results
after applying the previous procedure to terms that belong to the same
equivalence class.
The effect is that they are regarded as different by the tool.

To summarize,
there are errors emerging from incorrect specification of the
equations,
and there are errors emerging from unjustified assumptions of the
tools.

Errors in the equations may result in different terms that become
equal,
or in equal terms that become different.
Errors in the tool may result in livelock (non terminating procedure),
or in equal terms that become different.

All of them will violate user intentions,
and are object of testing.

An error detected in the equational system must be repaired.

An error detected in the tool does not strictly need to be repaired
(you may always blame the authors of the tool);
but for any practical purpose, it uses to be very convenient to modify
the equational system in order to get into the scope of correct
behaviour of the tool.

\section{A Language to specify test cases}
\input{lang.tex}

\section{Verdict Assignment}
Test run consist of exercising each assertion with the variable in it
properly replaced by the corresponding ground terms.
There are three possible verdicts for each test case:
\begin{description}
\item[pass.-]
  the assertion is satisfied.
\item[fail.-]
  the assertion is not satisfied.
\item[inconclusive.-]
  the premiss(es) do(es) not hold.
\end{description}

Verdicts are assigned to observations after taking into consideration
the intention of the test.
The following table summarizes the criteria:

\begin{tabbing}
mm \= mm \= mm \=				\kill
if any premiss fails then			\\
\> return {\bf inconclusive}			\\
else $(*$ all premisses hold $*)$		\\
\>  if the assertion must hold then		\\
\> \>   if the assertion does hold then		\\
\> \> \>    return {\bf pass}			\\
\> \>   else					\\
\> \> \>    return {\bf fail}			\\
\> \>   endif					\\
\>  else $(*$ the assertion must not hold $*)$	\\
\> \>   if the assertion holds then		\\
\> \> \>    return {\bf fail}			\\
\> \>   else					\\
\> \> \>    return {\bf pass}			\\
\> \>   endif					\\
\>  endif					\\
endif
\end{tabbing}

% Let $T$ be an assertion that must hold,
% the following piece of LOTOS associates a verdict assignment to its
% evaluation:

% \begin{verbatim}
%     [ T ]-> pass ; ...
%   []
%     (*| priority -1 |*) fail ; ...
% \end{verbatim}

% where the annotation \verb/priority/ implies that the branch it guards
% will only be selected if the other one yields \verb/stop/.

% Let $T$ be an assertion that must not hold,

% \begin{verbatim}
%     [ T ]-> fail ; ...
%   []
%     (*| priority -1 |*) pass ; ...
% \end{verbatim}
% where a test assertion as \verb/(a != b)/ is translated into a LOTOS
% equation as \verb/(a = b)/.
% This last is $T$ in the LOTOS text.

% Let $P=>T$ be an assertion that must hold if the premiss holds,

% \begin{verbatim}
%     [ P ]->[ T ]-> pass ; ...
%   []
%     [ P ]-> (*| priority -1 |*) fail ; ...
%   []
%     (*| priority -2 |*) inconclusive ; ...
% \end{verbatim}

% Let $P=>T$ be an assertion that must not hold if the premiss holds,

% \begin{verbatim}
%     [ P ]->[ T ]-> fail ; ...
%   []
%     [ P ]-> (*| priority -1 |*) pass ; ...
%   []
%     (*| priority -2 |*) inconclusive ; ...
% \end{verbatim}

\section{Which equations?}
Test cases are,
in the end,
equations involving user operations.
When the debugger starts considering cases to exercise,
the first question is
{\em ``which equations shall I exercise?''}

There are basically three groups to consider:
\begin{enumerate}
\item
  White box testing:
  equations written by the user in the ADT specification.
\item
  White box testing:
  guards and predicates showing up in the behaviour part of the
  specification.
\item
  Black box testing.
  Alternative points of view on the data:
  \begin{enumerate}
  \item
    terms that must be different,
  \item
    properties expected from operations,
  \item
    theorems that are known to hold (or not),
  \item
    \ldots
  \end{enumerate}
\end{enumerate}

The first group addresses the check of whether the interpretation
provided by the tool satisfies or not the equations stated by the
user. 
This directly addresses to discover by testing whether the rewrite
system induced from the equations is convergent or not
(if there is a risk for the tool to behave incorrectly,
we are as well checking it,
thus getting confidence on its quality).

The second group addresses the expected use of equations.
Many specifiers do not worry to perfectly and completely specify a
nice theory for a type,
but use to minimize the specification effort by only providing enough
knowledge as to resolve those cases that do show up in the use of the
data in the behavioral part.
This usually means that many of the operations are only partially
specified,
and only the specified part is to be tested.

The third group of assertions addresses the most general goal of
getting the right type.
Typical examples of it are to check that an operation is commutative,
or to check that a well known theorem (difficult to prove after
equations) does hold for a selected number of cases.

The two first groups fall into what is usually known as white box
testing:
the actual specification structure is inspected to create the test
cases.
The third group correspond to back box testing:
the intentions of the system are tested,
without looking at the actual specification of it.

A limitation of white box testing is that it will not tell you if the
code is ``completely wrong'';
i.e. the wrong type is being specified.

A limitation of black box testing is that it will not tell you if there
is a ``missing function'';
i.e. how can you test it if you do not know it is there?

The first group tests that the system interpretation is right;
the second one that the system specification is enough;
the third one that the specified system is the desired one.

\section{Which data?}
For each assertion we wish to test,
ground terms are to be provided.
The question rises about which data values are convenient.

It is obvious that every constant
(nullary operation) in a sort must be used systematically in every
test involving values of that sort.

If the sort under consideration is finite,
exercising one representative of each class sounds as a solid approach.
It is possible, for instance, in the case of booleans, where there are
supposed to be just two representatives, namely true and false.
It is true as well for those many types that are enumerative,
that is, they define a finite list of constants.

But most interesting data types have an infinite number of classes,
and therefore an infinite number of ground terms would be needed to
exercise the equations thoroughly.
Then, a finite number of data values has to chosen,
which ones?

Software testing theory has a clean answer to this issue.
For each sort,
we must divide its existence space around singular points,
that is values that imply some break of smoothness in equations
definition.
For instance, when speficying arithmetic modulus 4,
4 and its multiples become singular.

The rule is to choose for testing every singular case,
its neighbors,
and ``normal'' representatives in between those.
For instance,
for arithmetic modulus 4,
we should exercise 4, 3, and 5 as neighbors,
and 2 as a normal case.
Even in this case, the number of singular values is infinite
\((0, 4, 8, 12, \ldots)\),
and only a limited number of them is needed.

A warning must be given to data test specifiers with respect to
thorough testing of sorts with a finite number of term classes.
For a thorough testing of the specification,
it must be proved that the terms considered are really covering every
class.
It may be simple for very simple terms where only constants are
defined,
but when operations on them are considered too,
it must be proved that no new term is generated.
That is,
the operations must be proved to be complete.
Unfortunately,
this is, in general, undecidable.

\section{Implementation}
\input{impl.tex}

\section{Other tools}
A tool to run test cases must be put together with tools that help in
preparing the test suite.
This subject needs further study,
but some early opportunities are reported below.

\subsection{Extraction of guards, predicates, and premisses}
In order to have positive assertions to test,
it might be convenient a tool that given an specification,
prints out the guards used in the behaviour,
or the predicates.

It should be easy to provide this tool based on an AST of the
specification.
A very flexible user interface is needed for convenience.

\subsection{Extraction of equations}
Another tool,
or a new functionality of the previous one,
would print out user equations of each sort.

\subsection{Extraction of data values}
Data values are needed to exercise the assertions with free variables.
Since all the data values are usually too many to try
(in fact, there use to be infinite),
tools might support the election of values.

A starting tool would print out the constants (nullary operations in a
sort.
A smarter tool would try to identify constructors of a sort by
inspecting equations
(a similar functionality is currently implemented as part of the
narrowing engine in SMILE).

Another class of tools
could traverse the specification and extract all the
values used along it.
That is, to print out value expressions without free variables.

As before,
it sounds simple to get this tool working on an AST representation of
the user specification.

A more elaborated tool would perform some kind of data-flow analysis,
and would be able to replace some variables from some free terms,
and provide more ground terms for experimentation.

\subsection{Ground term generation}
A stronger approach would be to synthetise ground terms.
Given a sort,
it is easy to determine all the nullary operations of it:
those without arguments.
Then,
it is possible to start applying the other operations in a recursive
manner.
Means are needed to stop unbounded generation of values.

An identification of constructors would severely limit the generation,
restricting it to terms build up of constructors.
Another interesting limit could be based on complexity analysis:
as more and more operations are used to build a ground term, its
complexity grows; an upper limit is imposed to stop further growing.
A wise weighting of operations would help to generate terms out of a
preferred set of components.

\subsection{Coverage}
{\bf Coverage} tells us how many distinct {\em paths} through the code
or set of functions has been covered,
out of the total possible.

Indirectly,
coverage provides a quantitative figure on how good a test suite is.
That is,
how much confidence is achieved after a test suite has been
successfully passed?

These definitions apply nicely to deterministic languages,
where the path followed by a concrete execution is univoquely
determined, and may be deduced from the source text.

This ideas seem to be completely useless for equational reasoning,
although we could attempt some kind of ``dynamic evaluation of
coverage'' by means of checking how many equations have been applied.

Even in a rewrite system,
as soon as two left hand sides overlap,
the execution path is not determined by the source text,
but different tools may choose different alternatives.

On the other hand,
evaluating coverage of a sequential program presents its most serious
difficulty if the chaining of conditionals.
That is,
it is difficult to get data to exercise every branch of code,
since late conditions are only reached after many other conditions,
and after plenty of calculations.
In usual software testing,
85\% of source code coverage is an excellent figure that,
nevertheless may be prohibitive expense to improve.
Testing is seldom finished:
it is usually ``quitted''.

In equational specifications,
all the equations are at the ``top level``
(perhaps with a few premisses to protect them).
If every user equation is exercised in the test suite,
coverage seems to be of 100\%.

When a user equation is used as a test by feeding it with actual
values, and checking that it holds,
\begin{itemize}
\item
  either the tool uses that equation as a rewrite tool,
  and therefore the ``path'' is covered, or
\item
  other equations are used as rewrite rules,
  yielding a result coherent with the statement of this one;
  somehow this equation is redundant.
\end{itemize}
Thus,
every useful equation is covered,
and redundant equations are indirectly proved to hold.
So, full coverage is obtained.

Of course,
coverage is a ``white box testing'' concept.
The core problem of testing that the right system is being specified
is extremely reluctant to quantitative measuring.

\section{Other Testing Means}
During the elaboration of this paper,
several other alternatives have been considered to get the ADTs right.
Most of them went, as usual, to \verb/dev/null'.
But eventually some ideas seem worth further thinking.
Please, regard this as a true working paper,
and allow us to sketch something more.

\subsection{Constructors Checks}
In actual implementations,
rewrite systems are very usual,
if not the only mean to implement ADTs.
In rewrite systems,
the canonical form plays a central role.
After observation of the canonical forms in a sort,
operations may be classified as
\begin{description}
\item[constructors.-]
  operations that may be part of canonical forms.
\item[non--constructors.-]
  operations that never show up in canonical forms.
\end{description}

It occurs that most specifiers do use these concepts to design their
equations.
For instance, in usual arithmetic, most people think of digits as
constructors, and of $+, -, *, \ldots$ as non--constructors.
That is, most people do not expect to see any $+, \ldots$ in a number,
but only to use them to combine numbers.

Then an idea is born:
{\em``is it worth checking that canonical forms are built only after
constructors?''}

The answer seems to be positive in two directions:
user intentions are checked,
and if we may rely on that assumption,
the test suite has to deal only with terms built out of constructors.

There are two approaches to get this kind of testing.
\begin{enumerate}
\item
  TOPO has an annotation to mark an operation as non--constructor.
  If at run-time  such an operation is needed to build a canonical
  form,
  an exception is raised.

  Since the language proposed in this document is intended to go into
  TOPO for execution,
  these kind of checks may be performed ``on the fly'' embedded with
  assertion testing.
\item
  A specific language could be devised where constructors for a sort
  are stated,
  and a large collection of terms are proposed to check whether any
  other operation is ever needed to generate the canonical form.

  \begin{verbatim}
  ofsort nat
  constructors 0, succ;
    0; 1; 2; 3; 4; 5; ...
    1+2; 2+2; 5+7; 9-4; ...
  \end{verbatim}
\end{enumerate}

\section{Limitations}
The approach presented in this document has a noticeable limitation in
the fact that it works on the canonical data type.
It limits the possibilities even to run some tests cases,
if the operations involved may not be identified in a single context.
It is different from the case of running the test cases in a given
scope.

This limitation uniquely applies to the capacity of the overloading
resolution algorithm to univoquely identify an operation when put in a
wider scope.
This limitation does not induce errors in test execution,
since the ambiguity is detected at compile time of the tester
specification,
and the test suite is rejected.

Testing, as usual, does not prove correctness;
it is only useful to pop out bugs.
It is only an enhancement of confidence that comes out from test run.

\section{Conclusions}
A language has been proposed to specify test suites to debug ADTs.
A method has been proposed to execute those tests,
and to get verdicts,
by means of generating a tester written in LOTOS.

Some guidelines are provided as to which test cases to select,
and on which data values to apply to them.
But this is open to further study.
Quality of the test suite needs also more elaboration.

Once the test suite has been successfully passed by the specification,
both of them are ``validated by testing''.
The test suite may be latter used to test the implementation of ADTs,
when the wonderful world of formal specification is left,
and hand coded data come into the scene.

\clearpage
\appendix
\section{Language grammar}
\input{grammar.tex}

\end{document}
