From Wikipedia, the free encyclopedia
GNU Nana provides support for Design by Contract in C and C++. Nana is implemented using both the C Preprocessor and GDB debugger. Features include:
- Time and space efficient. 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 you're willing to accept the time penalty this can be reduced to 0 or 1 byte by using debugger based assertions.
- Limited support for formal methods.
- Before and after state support (e.g. x,x' in the Z notation).
- Support for the predicate calculus operators support for universal (forall) and existential (exists) quantification.
- Verification of timing behaviour.
- Selective logging of messages to memory, syslog or files.
[edit] External links
|
GNU Project |
|
| History |
|
 |
|
| Licences |
|
|
| Software |
|
|
| Public speakers |
|
|
| Other topics |
|
|
