Go to the first, previous, next, last section, table of contents.

Permission is granted to make and distribute verbatim copies of this manual provided the copyright notice and this permission notice are preserved on all copies.

Introduction

Nana is a library that provides support for assertion checking and logging in a space and time efficient manner. The aim is to put common good practise(1) into a library that can be reused rather than writing this stuff every time you begin a new project.

In addition assertion checking and logging code can be implemented using a debugger rather than as inline code with a large saving in code space.

Nana aims to solve the following problems:

Avoid the two executables problem (one with asserts in and another without any). The code space and time costs of having assertion checking and detailed logging code in a program can be high. Normally people construct two versions of the program, one with checking code for testing and one without checking code for production use. With nana one version of the executable can be built for both testing and release since debugger based checking has negligible space and time impact.
Configurable: the nana library is designed to be reconfigured by the user according to their needs. For example we can:
- Modify the behaviour on assertion failure, e.g. to attempt a system restart rather than just shutting down.
- Selectively enable and disable assertion checking and logging both at compile and run time.
- Send the logging information off to various locations, e.g.
  - Users terminal
  - A file for later checking.
  - Another process, e.g. a plotting program or a program that verifies that the system is behaving itself.
  - A circular buffer in memory. This is an old embedded systems trick and is very useful for production systems. The time cost of logging into memory is not large and when your production system in the field has problems you can then see what was happening in the minutes before its unfortunate demise rather than asking some user what was happening before it died.
Time and space efficient. For example the GNU `assert.h' implementation uses 53 bytes for `assert(i>=0)' on a i386. The nana version using the i386 `stp' instruction on assert fail uses 10 bytes. If your willing to accept the time penalty this can be reduced to 0 or 1 byte by using debugger based assertions.
Support for formal methods.
- Before and after state (e.g. x,x' in the Z notation). Specifications are often written in terms of the state of variables before and after an operation. For example the `isempty' operation on a stack should leave the stack unchanged. To verify this in nana we could use:
```
bool isempty(){ /* true iff stack is empty */
  DS($s = s); /* copy s into $s in the debugger */
  ...; /* code to do the operation */
  DI($s == s); /* verify that s hasn't been changed */
}
```
  These `$..' variables are called convenience variables and are implemented by gdb. They have a global scope and are dynamically typed and initialised automatically to 0. In addition a C only version of before and after state is provided. For example:
```
bool isempty() { /* true iff stack is empty */
  ID(int olds); /* declare variable to hold old value */
  IS(olds = s); /* copy s into $s in the debugger */
  ...; /* code to do the operation */
  I(olds == s); /* verify that s hasn't been changed */
}
```
- Support for Predicate Calculus. Nana provides some support for universal (forall) and existential (exists one or more) quantification. For example to specify that the string v contains only lower case letters we could use:
```
  I(A(char *p = v, *p != '\0', p++, islower(*p)));
```
  These macros can be nested and used as normal boolean values in control constructs as well as assertions. Unfortunately they depend on the GNU CC statement value extensions and so are not portable. The following macros are defined in `Q.h':
  
  A
  For all values the expression must be true.
  E
  There exists one or more values for which the expression is true.
  E1
  There exists a single value for which the expression is true.
  C
  Returns the number of times the expression is true.
  S
  Returns the sum of the expressions.
  P
  Returns the product of the expressions.
- Verifying timing. As well as using nana to verify timings with assertions using a hardware supported timer you can also a simulator (e.g. the PSIM power pc simulator by Cagney) with gdb. These simulators can model time and provide a register called `$cycles' which represents the current cycle count of the program. This can be used to check that timing constraints are being meet.
```
void process_events() {
  for(;;){ 
    DS($start = $cycles); 
    switch(get_event()){
      case TOO_HOT:
        ...;
        DI($start - $cycles <= 120);
        break;
      case TOO_COLD:
        ...;
        DI($start - $cycles <= 240);
        break;
    }
  }
}
```

The intended audience for Nana includes:

Software Engineers.
Formal methods community.
Real time programmers.
System testers.
People teaching programming.

Related work

The Nana project was inspired by some other projects, in particular:

Anna - Anna stands for "Annotated Ada" where the programmer inserts various assertions into the code which can be automatically validated. To quote from the WWW Virtual Library entry on Anna:
Anna is a language for formally specifying the intended behaviour of Ada programs. It extends Ada with various different kinds of specification constructs from ones as simple as assertions, to as complex as algebraic specifications. A tool set has been implemented at Stanford for Anna, including:
1. standard DIANA extension packages, parsers, pretty-printers;
2. a semantic checker;
3. a specification analyser;
4. an annotation transformer; and
5. a special debugger that allows program debugging based on formal specifications
All tools have been developed in Ada and are therefore extremely portable. Anna has thus been ported to many platforms. For more information send e-mail to "[email protected]". Before down loading the huge Anna release, you may wish to copy and read some Anna LaTeX reports.
Anna is available from: ftp://anna.stanford.edu/pub/anna
Eiffel - the Eiffel programming language provides support in the language flexible assertion checking. To quote from the Eiffel page in WWW Virtual library:

Eiffel is a pure object-oriented language featuring multiple inheritance, polymorphism, static typing and dynamic binding, genericity (constrained and unconstrained), a disciplined exception mechanism, systematic use of assertions to promote programming by contract, and deferred classes for high-level design and analysis.
APP - Annotation PreProcessor. The APP was written by David S. Rosenblum and provides assertion checking functions for C and C++. It is implemented using a preprocessor wrapper around the C preprocessor and supports quantifiers and before/after state. See "A Practical Approach to Programming with Assertions" in Vol 21, No. 1, January 1995 of IEEE Transactions on Software Engineering for an interesting paper describing APP. Unfortunately the APP tool doesn't seem to be freely available (I'm willing to be corrected on this). Note that any similarity between my examples and David's are due to morphic resonance.

Nana is essentially a poor mans implementation of some of these ideas which works for C and C++. Ideally in the best of all possible worlds you might want to look at Eiffel or in the military world Ada and Anna. If you use TCL/TK you might also be interested in Jon Cook's `AsserTCL' package.

Assert.h considered harmful

Most C programmers become familiar with assertions from the the assert.h header. As such its a very good thing and has a nice simple implementation. However it is also inefficient and leads some people to the conclusion that assertion checking is an expensive luxury.

The implementation of assert.h as distributed with gcc looks like the following (after a bit of editing):

# ifndef NDEBUG
# define _assert(ex)	{if (!(ex)) \
                         {(void)fprintf(stderr, \
                           "Assertion failed: file \"%s\", line %d\n", \
                           __FILE__, __LINE__);exit(1);}}
# define assert(ex)	_assert(ex)
# else
# define _assert(ex)
# define assert(ex)
# endif

There are are two main problems with this:

Code space overhead: each call to `assert' generates 2 function calls with 4 and 1 arguments plus strings for error messages. If assert.h had library code support we could make the implementation much more space efficient, e.g. by calling a single function on error detection.
The default behaviour simply prints a message and dies, ideally you like to be able to use a debugger to determine why the assertion failed. Even if you run this under the debugger you can't observe the failures of variables are an assert failure because the process exits rather than aborting back to the debugger.

Of course everyone merely rewrites their own `assert' macro so these are not significant objections. The only problem is if the author uses the libraries without modification.

Scope of this document

This document aims to both describe the library and provide a tutorial in its use. Further work is required, particularly on the tutorial sections. If anyone has any suggestions please send them to me.

Go to the first, previous, next, last section, table of contents.