packages/assert/assert.tex

\documentclass{article}

\usepackage[latin1]{inputenc}

\begin{document}

\title{ASSERT: Dynamic Verification of Assertions on Function Types}
\author{Thomas Sturm\\
Dpto.~de Matem�ticas Estad�stica y Computaci�n\\
Universidad de Cantabria\\
39071 Santander, Spain\\
Email: \texttt{sturm@redlog.eu}}
\date{July 18, 2010}
\maketitle

\begin{abstract}
  ASSERT admits to add to symbolic mode RLISP code assertions (partly)
  specifying \emph{types} of the arguments and results of RLISP expr
  procedures. These types can be associated with functions testing the
  validity of the respective arguments during runtime.
\end{abstract}

\section{Loading and Using}
The package is loaded using \texttt{load\_package} or
\texttt{load!-package} in algebraic or symbolic mode, resp. There is a
central switch \texttt{assertcheck}, which is off by default. With
\texttt{assertcheck} off, all type definitions and assertions described
in the sequel are ignored and have the status of comments. For
verification of the assertions it most be turned on (dynamically) before
the first relevant type definition or assertion.

ASSERT aims at the dynamic analysis of RLISP expr procedure in symbolic
mode. All uses of \texttt{typedef} and \texttt{assert} discussed in the
following have to take place in symbolic mode. There is, in contrast, a
final print routine \texttt{assert\_analyze} that is available in both
symbolic and algebraic mode.

\section{Type Definitions}
Here are some examples for definitions of types:
\begin{verbatim}
typedef any;
typedef number checked by numberp;
typedef sf checked by sfpx;
typedef sq checked by sqp;
\end{verbatim}
The first one defines a type \texttt{any}, which is not possibly checked
by any function. This is useful, e.g., for functions which admit any
argument at one position but at others rely on certain types or
guarantee certain result types, e.g.,
\begin{verbatim}
procedure cellcnt(a);
   % a is any, returns a number.
   if not pairp a then 0 else cellcnt car a + cellcnt cdr a + 1;
\end{verbatim}

The other ones define a type \texttt{number}, which can be checked by
the RLISP function \texttt{numberp}, a type \texttt{sf} for standard
forms, which can be checked by the function \texttt{sfpx} provided by
ASSERT, and similarly a type for standard quotients.

All type checking functions take one argument and return extended
Boolean, i.e., non-nil iff their argument is of the corresponding type.

\section{Assertions}
Having defined types, we can formulate assertions on expr procedures in
terms of these types:
\begin{verbatim}
assert cellcnt: (any) -> number;
assert addsq: (sq,sq) -> sq;
\end{verbatim}
Note that on the argument side parenthesis are mandatory also with only
one argument. This notation is inspired by Haskell but avoids the
intuition of currying.\footnote{This notation has benn suggested by C. Zengler}

Assertions can be dynamically checked only for expr procedures. When
making assertions for other types of procedures, a warning is issued and
the assertion has the status of a comment.

It is important that assertions via assert come after the definitions of
the used types via \texttt{typedef} and also after the definition of the
procedures they make assertions on.

A natural order for adding type definitions and assertions to the source
code files would be to have all typedefs at the beginning of a module
and assertions immediately after the respective functions.
Fig.~\ref{FIG:assMod} illustrates this. Note that for dynamic checking
of the assertions the switch \texttt{assertcheck} has to be on during
the translation of the module; i.e., either when reading it with
\texttt{in} or during compilation. For compilation this can be achieved
by commenting in the \texttt{on assertcheck} at the beginning or by
parameterizing the Lisp-specific compilation scripts in a suitable way.

An alternative option is to have type definitions and assertions for
specific packages right after \texttt{load\_package} in batch files as
illustrated in Fig.~\ref{FIG:assBat}.
\begin{figure}
  \begin{small}
\begin{verbatim}
module sizetools;

load!-package 'assert;

% on assertcheck;

typedef any;
typedef number checked by number;

procedure cellcnt(a);
   % a is any, returns a number.
   if not pairp a then 0 else cellcnt car a + cellcnt cdr a + 1;

assert cellcnt: (any) -> number;

% ...

endmodule;

end;  % of file
\end{verbatim}
  \end{small}
  \caption{Assertions in the source code.\label{FIG:assMod}}
\end{figure}

\begin{figure}
  \begin{small}
\begin{verbatim}
load_package sizetools;
load_package assert;

on assertcheck;

lisp <<
   typedef any;
   typedef number checked by numberp;

   assert cellcnt: (any) -> number
>>;

% ... computations ...

assert_analyze();

end;  % of file
\end{verbatim}
  \end{small}
  \caption{Assertions in a batch file.\label{FIG:assBat}}
\end{figure}

\section{Dynamic Checking of Assertions}
Recall that with the switch \texttt{assertcheck} off at translation
time, all type definitions and assertions have the status of comments.
We are now going to discuss how these statements are processed with
\texttt{assertcheck} on.

\texttt{typedef} marks the type identifier as a valid type and possibly
associates the given typechecking function with it. Technically, the
property list of the type identifier is used for both purposes.

\texttt{assert} encapsulates the procedure that it asserts on into
another one, which checks the types of the arguments and of the result
to the extent that there are typechecking functions given. Whenever some
argument does not pass the test by the typechecking function, there is a
warning message issued. Furthermore, the following numbers are counted
for each asserted function:
\begin{enumerate}
\item The number of overall calls,
\item the number of calls with at least one assertion violation,
\item the number of assertion violations.
\end{enumerate}
These numbers can be printed anytime in either symbolic or algebraic
mode using the command \texttt{assert\_analyze()}. This command at the
same time resets all the counters.

Fig.~\ref{FIG:sample} shows an interactive sample session.
%
\begin{figure}
  \begin{small}
\begin{verbatim}
1: symbolic$

2* load_package assert$

3* on assertcheck$

4* typedef sq checked by sqp;
sqp

5* assert negsq: (sq) -> sq;
+++ negsq compiled, 13 + 20 bytes

(negsq)

6* assert addsq: (sq,sq) -> sq;
+++ addsq compiled, 14 + 20 bytes

(addsq)

7* addsq(simp 'x,negsq simp 'y);

((((x . 1) . 1) ((y . 1) . -1)) . 1)

8* addsq(simp 'x,negsq numr simp 'y);

*** assertion negsq: (sq) -> sq violated by arg1 (((y . 1) . 1))

*** assertion negsq: (sq) -> sq violated by result (((y . -1) . -1))

*** assertion addsq: (sq,sq) -> sq violated by arg2 (((y . -1) . -1))

*** assertion addsq: (sq,sq) -> sq violated by result (((y . -1) . -1))

(((y . -1) . -1))

9* assert_analyze()$
------------------------------------------------------------------------
function          #calls              #bad calls   #assertion violations
------------------------------------------------------------------------
addsq                  2                       1                       2
negsq                  2                       1                       2
------------------------------------------------------------------------
sum                    4                       2                       4
------------------------------------------------------------------------
\end{verbatim}
  \end{small}
  \caption{An interactive sample session.\label{FIG:sample}}
\end{figure}

\section{Switches}
As discussed above, the switch \texttt{assertcheck} controls at
translation time whether or not assertions are dynamically checked.

There is a switch \texttt{assertbreak}, which is off by default. When
on, there are not only warnings issued for assertion violations but the
computations is interrupted with a corresponding error.

The statistical counting of procedure calls and assertion violations is
toggled by the switch \texttt{assertstatistics}, which is on by default.

\section{Efficiency}
The encapsulating functions introduced with assertions are automatically
compiled.

% sturm@lennier[~/Desktop] time redpsl < taylor.tst > /dev/null

% real	0m0.798s
% user	0m0.584s
% sys	0m0.166s
% sturm@lennier[~/Desktop] time redcsl < taylor.tst > /dev/null

% real	0m1.975s
% user	0m1.808s
% sys	0m0.143s
% sturm@lennier[~/Desktop] time redpsl < taylor.tst > /dev/null

% real	0m0.442s
% user	0m0.316s
% sys	0m0.122s
% sturm@lennier[~/Desktop] time redcsl < taylor.tst > /dev/null

% real	0m0.610s
% user	0m0.491s
% sys	0m0.115s

We have experimentally checked assertions on the standard quotient
arithmetic \texttt{addsq}, \texttt{multsq}, \texttt{quotsq},
\texttt{invsq}, \texttt{negsq} for the test file \texttt{taylor.tst} of
the TAYLOR package. For CSL we observe a slowdown of factor 3.2, and for
PSL we observe a slowdown of factor 1.8 in this particular example,
where there are 323\,750 function calls checked altogether.

The ASSERT package is considered an analysis and debugging tool.
Production system should as a rule not run with dynamic assertion
checking. For critical applications, however, the slowdown might be
even acceptable.

\section{Possible Extensions}
Our assertions could be used also for a static type analysis of source
code. In that case, the type checking functions become irrelevant. On
the other hand, the introduction of variouse unchecked types becomes
meaningful.

In a model, where the source code is systematically annotated with
assertions, it is technically no problem to generalize the specification
of procedure definitions such that assertions become implicit. For
instance, one could \emph{optionally} admit procedure definitions like
the following:
\begin{verbatim}
procedure cellcnt(a:any):number;
   if not pairp a then 0 else cellcnt car a + cellcnt cdr a + 1;
\end{verbatim}
\end{document}