-
Notifications
You must be signed in to change notification settings - Fork 1
/
ANNOUNCE
executable file
·96 lines (67 loc) · 3.22 KB
/
ANNOUNCE
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
GNU Nana -- improved support for assertions and logging.
GNU Nana is a freely available library providing improved support for
assertions and logging GNU C/C++. In particular:
* Space/time efficient assertion checking.
* Space/time efficent program logging.
* Code to HTML converter giving only details
of your interface and pre/postconditions
(similar to Eiffel short form).
* Statement and function level tracing under GDB.
It was written by the author because he has written too many of these
systems in the past for individual projects and has finally gotten
tired of it. In particular it provides:
0. Assertion and logging code can be implemented as inline C code (as
in <assert.h>) or by extracting a set of commands for the GNU gdb
debugger which then does the actual checking. The use of gdb avoids
the need to create two executables (one with assertions in, and one
which does not contain assertions and is the production system) since
the cost for assertion checking only occurs if you run the application
under the debugger.
1. Configurable:
a) Compile and run-time selection of assertions and logging.
b) The action on assertion failure can be redefined.
c) Modify the destination for logging messages. For example:
i) To a file.
ii) To a circular buffer in core.
iii) To a UNIX process (for program visualisation)
2. Space and time efficient (particularly compared to <assert.h>).
For example:
a) Simply replacing assert(i >= 0) with nana's I(i >= 0)
reduces the code space from 53 bytes to 32 bytes.
If your willing to accept a illegal instruction as the
signal for assertion failure you can reduce this to only
10 bytes from the original 53.
b) By using nana's debugger based assertions and log messages
you can reduce the code space to 0 or 1 bytes and so leave
support for these things in your production code.
3. Some support for formal methods in particular Quantifiers and
before and after state (as in Z, VDM etc). For example:
if(A(int i = 0, i < MAX, i++,
A(int j = 0, j < MAX, j++,
a[i][j] == 0))) { /* a[..][..] is all 0's */
... ;
}
DS($x = x);
..; /* code that modifies x */
DI(x * x == $x); /* check the previous state of x */
If you have an instruction level simulator you can also add in
timing constraints into your system as well as various simple
forms of instrumentation.
4. Ability to produce a short form of your program in HTML which
describes the interfaces and assumptions of your code.
5. Portability.
Ideally you should be using GNU CC/C++ and/or GDB.
The library should also be useful to people using other compilers.
Unfortunately parts of the library use two GNU CC extensions
which makes them non-portable. These are:
1. Variable number of arguments to macros which is used in the
message logging components (L.h,DL.h).
2. Statement Expressions which are used to implement
the support for Forall, Exists, etc (Q.h)
The rest of the library is written in at least partially portable ANSI C.
6. For further information see:
<ftp://ftp.cs.ntu.edu.au/pub/nana/>
or
<http://www.cs.ntu.edu.au/homepages/pjm/nana-home>
Phil Maker <pjm@gnu.org>
Quoll Systems <http://www.quoll.com.au/>