%\section{A Language to specify test cases}
In order to test the data part,
we need to exercise it under a large number of situations.
A language that permits to express concisely and clearly the cases we
wish to test,
will surely help specifiers to produce solid test suites,
and keep them documented.

\subsection{Assertions that must hold}
A first class of assertions that are needed to exercise are those that
need to hold.
For instance (in most usual specifications of integers),
the following assertion is expected to hold	\\
\centerline{\verb/2 + 2 = 4 ;/}			\\
despite the fact that integer arithmetic may be specified via the
convoluted concepts of Peano.

These tests check that equal terms are classified into the same
equivalence class.
That is,
that there are not too many borders.

\subsection{Assertions that must not hold}
A second class of assertions that are need to exercise
are somehow negative:
they must not hold.
For instance,
it is usually be very convenient that	\\
\centerline{\verb/true != false/}	\\
at least in most usual specifications of booleans.

The notation \verb/!=/ is chosen to avoid conflicts with the very rich
set of symbols that are allowed to specify operations in LOTOS.
Both \verb/!/ and \verb/=/ have specific meaning individually,
and it is not possible to mix them up with user operations.

These tests check that different terms do not fall into the same
equivalence class.
That is,
that there are not too few borders.

\subsection{Partial functions}
Despite the fact that LOTOS provides complete semantics for any
operation,
the users use to underspecify partial operations,
just by no providing complete equations for them.
In terms of rewrite systems,
it is usually the case that a partial operation gets a status of
semi-constructor:
it is not a constructor for acceptable entries,
but is unable to rewrite on unexpected arguments.

For instance,
when division is specified,
no rule is given to handle	\\
\centerline{\verb:10 / 0:}

Each specification has its own approach to this business of partial
operations.
The one exposed above is only a simple one,
that is close to usual practice in programming languages:
let it be undefined, but raise an exception if it would ever occur.
LOTOS reproduces the first part,
but since there is no opportunity to raise any exception,
there are a number of new ground terms that
may stealthily creep into the specification.

Anyway,
in terms of testing,
partial operations may not be exercised on incorrect arguments.
So,
it is often convenient to sort out this possibilities explicitly: \\
\centerline{\verb|n ne 0 => (m / n) lt m ;|}

\subsection{Grouping}
Usually,
most of the assertions will be exercised on sets of of ground terms
\begin{verbatim}
  for b: bool in [true, false] [[
    not (not (b)) = b ;
  ]]
\end{verbatim}
\begin{verbatim}
  for p, q: bool in [true, false] [[
    p xor q = (p and not (q)) or (not (p) and q) ;
  ]]
\end{verbatim}
\begin{verbatim}
  for m: nat in [1, 2, 3],
      n: nat in [1, 2, 3] [[
    m > n => m/n <> 0 ;
  ]]
\end{verbatim}
Notice the syntax is systematically chosen to use the same lexical
constructs as LOTOS.
This permits to reuse lexical analyzers,
and avoid potential errors in identifying LOTOS operations.

\subsection{Definitions of Lists}
Some lists of data values to exercise assertions are used quite a lot
of times in a data test specification.
They may be given a name
\begin{verbatim}
  let m4: nat = [0, 4, 8, 12];
  for m, n in m4 [[
    n > 0 , m > n => m mod n = 0 ;
  ]]
\end{verbatim}




